From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=0.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.228.227 with SMTP id sl3mr5367571pbc.5.1341060847062; Sat, 30 Jun 2012 05:54:07 -0700 (PDT) Path: l9ni2271pbj.0!nntp.google.com!news2.google.com!news3.google.com!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Sat, 30 Jun 2012 15:54:03 +0300 Organization: Tidorum Ltd Message-ID: References: <4fe59ea0$0$9502$9b4e6d93@newsspool1.arcor-online.net> <1mkp7fzlk1b0y.1ueinfjn48fcy$.dlg@40tude.net> <4fe72b6b$0$9504$9b4e6d93@newsspool1.arcor-online.net> <1bbvp3ghpjb5s.1go1s1qvcmagh$.dlg@40tude.net> <4fe76fad$0$9507$9b4e6d93@newsspool1.arcor-online.net> <1jt8vhzxfrv2i.eohce4d3rwx1$.dlg@40tude.net> <4fe83aaa$0$6624$9b4e6d93@newsspool2.arcor-online.net> <1pkfv0tiod3rn$.onx6dmaa3if9$.dlg@40tude.net> <1i1mp8xs3vtl2.1oc4m66qtfgzq.dlg@40tude.net>

<4fe9bde5$0$6566$9b4e6d93@newsspool4.arcor-online.net>

<1otknesgpcisl$.112pd12on3vsb$.dlg@40tude.net> Mime-Version: 1.0 X-Trace: individual.net 6nhFgPA7scW4RpOKHrQ7JALXdfnM5tsGaW/zx+Kyaw5nDI0jNh/OZ9KAmpAY0m/wiq Cancel-Lock: sha1:awE1CEy5WdS3jyI57v7FiFR6Jso= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:12.0) Gecko/20120428 Thunderbird/12.0.1 In-Reply-To: <1otknesgpcisl$.112pd12on3vsb$.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Date: 2012-06-30T15:54:03+03:00 List-Id: On 12-06-30 11:26 , Dmitry A. Kazakov wrote: > On Fri, 29 Jun 2012 14:03:27 -0700 (PDT), Shark8 wrote: > >>>> What do pre/post implement, if so, in your view? >>> >>> if Pre(...) then >>> >>> if Post(...) then >>> null; >>> else >>> raise Constraint_Error; >>> end if; >>> else >>> raise Constraint_Error; >>> end if; >> >> Ok, but this is just what preconditions [and post] are supposed to do. > > [That is POV #1] > > No they are not. True pre-/post-conditions are not supposed to implement > anything. > > Formally speaking, pre-/post-conditions are statements of another language > L. The language Ada is what you use to program some P. P operates bits and > bytes. The language L is used to operate P itself. In L you can say Correct > (P) or Incorrect (P). Perhaps the Ada 2012 "Pre" and "Post" constructs should be called "precheck" and "postcheck" instead of "precondition" and "postcondition". Then it would be clearer that they are not the same as the logical, side-effect-free pre/postconditions used in program proofs. An Ada compiler or prover can include (as a conjunct) the "precheck" condition in the precondition of a call to the subprogram, and include the "postcheck" condition in the postcondition of the call (with alternative paths to exception handling). But the pre/post-checks are not the *whole* pre/post-conditions in the compiler's analysis or proof. -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .