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=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!newsfeed1.swip.net!newspeer1.nac.net!Xl.tags.giganews.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail NNTP-Posting-Date: Tue, 12 May 2015 18:26:00 -0500 Newsgroups: comp.lang.ada Date: Tue, 12 May 2015 19:25:58 -0400 From: Peter Chapin X-X-Sender: pcc09070@WIL414CHAPIN.vtc.vsc.edu Subject: Re: {Pre,Post}conditions and side effects In-Reply-To: Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com> User-Agent: Alpine 2.11 (CYG 23 2013-08-11) Organization: Vermont Technical College MIME-Version: 1.0 Content-Type: MULTIPART/MIXED; BOUNDARY="3735943886-1464782853-1431473160=:4652" X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-a7bGcd6G6Nvpj3DvioGDiFlBN2YMnksPFtWeI9dktP6yCSPm9FYnzPGXSakaPPkngRyiqN85gJpBl4m!HeMMwRDYpcwPAOvohmS4R9WRG/MBC+H+/vVOzsGfZVLjy0ZY/6Ww7APVEkjSNEIorzdF5QzyHF/J!ZcwaAV45KzaQ7/07lA== X-Complaints-To: abuse@giganews.com X-DMCA-Notifications: http://www.giganews.com/info/dmca.html X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.40 X-Original-Bytes: 6143 Xref: news.eternal-september.org comp.lang.ada:25858 Date: 2015-05-12T19:25:58-04:00 List-Id: This message is in MIME format. The first part should be readable text, while the remaining parts are likely unreadable without MIME-aware tools. --3735943886-1464782853-1431473160=:4652 Content-Type: TEXT/PLAIN; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE On Mon, 11 May 2015, vincent.diemunsch@gmail.com wrote: > Le mardi 12 mai 2015 00:49:40 UTC+2, Peter Chapin a =E9crit=A0: > >> In the book on SPARK 2014 John McCormick and I recently wrote=20 >> (available later this summer) we show an example of proving a sorting=20 >> procedure where the tools prove both >> >> a) The resulting array is sorted and >> b) The resulting array is a permutation of the original array. >> >> We use ghost functions to do this. > > Tell us more ! Do you use the same basic idea :=A0assuming that the swap= =20 > function is an elementary permutation of arrays ? Do you use an assume=20 > statement ? Yes, and yes. We do use Assume to describe the necessary mathematical=20 properties involved. In particular we Assume the array after swapping two= =20 elements is a permutation of the original. Similarly we use Assume to=20 embody the idea that permutations are transitive: if B is a permutation of= =20 A and C is a permtuation of B, then C is a permutation of A. This is=20 necessary to support a loop invariant asserting that the partially=20 processed array is always a permutation of the original. In our example we leave the ghost functions unimplemented so the tools=20 can't learn anything about them other than what we describe in the=20 assertions associated with them. This also means the program won't link=20 unless it's compiled with an Assertion_Policy of Ignore. The ghost functions could potentially be implemented with actual code and= =20 then one might hope the tools could learn enough from them to do without=20 some of the Assumes, for example via contextual analysis. However, some=20 caution is needed. You don't want to use the sorting procedure to=20 implement the permutation checker that you are using to prove the sorting= =20 procedure! >> The proofs can be processed with the upcoming SPARK GPL 2015 release,=20 >> but I'm not sure if they will go through with SPARK GPL 2014. > > What is new with the SPARK GPL=A02015 prover ? Well, SPARK GPL 2015 ships with two theorem provers that it uses together:= =20 alt-ergo and cvc4 (you can also add others, such as z3). So, by default,=20 anything that either prover can prove is seen as handled from the user's=20 point of view. Since the provers have different strengths the combination= =20 gives you better coverage than either one alone. However, it also=20 increases the amount of code you have to trust. There are various other improvements. For example it handles bit=20 manipulation operators a lot better than SPARK GPL 2014. Just consider=20 this simple case: type Octet is mod 2**8; type Double_Octet is mod 2**16; X : Octet; Y : Double_Octet; =2E.. X :=3D Octet(Y and 16#00FF); As I recall SPARK GPL 2014 didn't understand that the masking operation=20 chopped the size of the result into an acceptable range for type Octet and= =20 thus it complained that it couldn't prove there wasn't a range violation.= =20 SPARK GPL 2015 has no problem with the example above, and other similar=20 examples. Also my experience with using the 2015 version as opposed to the 2014=20 version is that it requires a lot less fussing around with "obvious"=20 things. Loop invariants, for example, can often be significantly=20 simplified or even eliminated. The user experience with it is much better= =20 overall. Non-linear floating point computations are still not handled that=20 fantastically (I understand it's a hard problem). Thus if you are doing a= =20 lot of floating point work you may need to wait for more evolutionary=20 improvements beyond even SPARK GPL 2015. Peter --3735943886-1464782853-1431473160=:4652--