Loading ...
Sorry, an error occurred while loading the content.
 

RE: [eiffel_software] Re: void safety and dbc

Expand Messages
  • Peter Horan
    ... Well, not quite. In the absence of an explicit postcondition, the postcondition is True. In any case, it can only be strengthened by a descendent toward
    Message 1 of 13 , Sep 1, 2012
      colin_paul_adams wrote:
      > `is_my_attribute_attached, has no postcondition. ...
      > A desecendant might redefine `is_my_attribute_attached'
      > to return exactly the opposite result (or always False,
      > or always True).

      Well, not quite. In the absence of an explicit postcondition, the postcondition is True. In any case, it can only be strengthened by a descendent toward False. So, the postcondition can be used and it should be made as strong as possible.

      So, does the code compile if the code is:

      ___is_my_attribute_attached: BOOLEAN
      ______do
      __________Result := attached my_attribute
      ______ensure
      __________attached: Result = attached my_attribute
      ______end

      --
      Peter Horan             Faculty of Science and Technology
      peter@...     Deakin University
      +61-3-5221 1234 (Voice) Geelong, Victoria 3217, AUSTRALIA
      +61-4-0831 2116 (Mobile)

      -- The Eiffel guarantee: From specification to implementation
      -- (http://www.cetus-links.org/oo_eiffel.html)


      Important Notice: The contents of this email are intended solely for the named addressee and are confidential; any unauthorised use, reproduction or storage of the contents is expressly prohibited. If you have received this email in error, please delete it and any attachments immediately and advise the sender by return email or telephone.

      Deakin University does not warrant that this email and any attachments are error or virus free.
    • rfo@amalasoft.com
      Hi Peter Yes, in the case I had the first feature was detachable and that is a source of confusion because it s a bad example. Recent posts by others have
      Message 2 of 13 , Sep 1, 2012
        Hi Peter

        Yes, in the case I had the first feature was detachable and that is a
        source of confusion because it's a bad example. Recent posts by others
        have actually done a better job of illustration. Neal's post of Aug 30
        had a couple of good ones.

        In reality, there are many cases where a feature's job is to assure the
        programmer that a value is non-void and valid. Such features, it seems
        to me have diminished importance if we then have to check voidness at
        every turn. If we have checked validity, and it includes non-voidness,
        and asserts that via postconditions, then _that_ check should suffice
        instead of having to perform an explicit void check.

        Even something as simple as

        if is_valid_something (foo) then
        foo.do_something
        end

        Is no longer usable. Losing this kind of mechanism makes code less
        readable and ultimately less good, defeating the goals of void safety
        and DbC - and of Eiffel.


        R

        ==================================================
        Roger F. Osmond



        -------- Original Message --------
        Subject: Re: [eiffel_software] void safety and dbc
        From: Peter Gummer <p-gummer@...>
        Date: Sat, September 01, 2012 3:32 am
        To: eiffel_software@yahoogroups.com

        <rfo@...> wrote:

        > is_empty: BOOLEAN ...
        > ensure
        > void-safe-implication: not Result implies attached first ...
        > ...
        > The intent, regardless of the eventual syntax, is to exploit the
        > specification aspects of contracts and make them partners with the more
        > explict mechanisms of void safety. The result I think would be
        > better-contracted and less defensive code.

        Hi Roger,

        I have a question, because I'm no closer to understanding what problem
        you're trying to solve with your "implied non-voidness" proposal.

        The postcondition above asserts that 'first' is attached when the
        container is not empty. The fact that you need to assert this would
        suggest that 'first' is declared detachable, right?

        first: detachable FOO ... etc.

        - Peter Gummer
      • larry_rix
        Hi Neal! I just tried this in a junk project and the compiler does in fact now see this CAP and reports no compile-time issues with the query feature:
        Message 3 of 13 , Sep 1, 2012
          Hi Neal!
          I just tried this in a junk project and the compiler does in fact now
          see this CAP and reports no compile-time issues with the query feature:
          `is_my_attribute_attached'.
          > Unfortunately, (the last time I checked) the compiler does not (yet)
          realize that> > is_my_attribute_attached: BOOLEAN> do> Result :=
          attached my_attribute> end



          [Non-text portions of this message have been removed]
        • Neal
          ... One problem I see is that Void safety, as part of the type system, is currently designed to be thread safe while contracts, as run time checks, are not
          Message 4 of 13 , Sep 1, 2012
            --- In eiffel_software@yahoogroups.com, <rfo@...> wrote:
            > Even something as simple as
            >
            > if is_valid_something (foo) then
            > foo.do_something
            > end
            >
            > Is no longer usable. Losing this kind of mechanism makes code less
            > readable and ultimately less good, defeating the goals of void safety
            > and DbC - and of Eiffel.

            One problem I see is that Void safety, as part of the type system, is currently designed to be thread safe while contracts, as run time checks, are not necessarily thread safe. Perhaps SCOOP will alleviate this mismatch.

            Colin, good point about the post condition.

            Neal
          Your message has been successfully submitted and would be delivered to recipients shortly.