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!news.glorb.com!peer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!Xl.tags.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Mon, 11 May 2015 17:49:39 -0500
Newsgroups: comp.lang.ada
Date: Mon, 11 May 2015 18:49:37 -0400
From: Peter Chapin <PChapin@vtc.vsc.edu>
X-X-Sender: pcc09070@WIL414CHAPIN.vtc.vsc.edu
Subject: Re: {Pre,Post}conditions and side effects
In-Reply-To: <c6a5c672-9e37-4d2b-b313-1f2139fffc66@googlegroups.com>
Message-ID: <alpine.CYG.2.11.1505111846520.5124@WIL414CHAPIN.vtc.vsc.edu>
References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com>
 <AnYlw.957256$Rp.242412@fx23.iad>
 <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com>
 <wccoaqucn51.fsf@shell01.TheWorld.com>
 <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com>
 <alpine.CYG.2.11.1412231747100.4196@WIL414CHAPIN.vtc.vsc.edu>
 <wccegrpq2om.fsf@shell01.TheWorld.com>
 <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com>
 <ce4af31e-d491-479f-a5b3-0b3eedea2a68@googlegroups.com>
 <midvq5$2u3$1@loke.gir.dk>
 <alpine.DEB.2.11.1505071103310.14859@debian> <migc9a$jp8$1@loke.gir.dk>
 <alpine.DEB.2.11.1505072052570.16448@debian> <mijen0$1hj$1@loke.gir.dk>
 <alpine.DEB.2.11.1505111113020.12062@debian>
 <c6a5c672-9e37-4d2b-b313-1f2139fffc66@googlegroups.com>
User-Agent: Alpine 2.11 (CYG 23 2013-08-11)
Organization: Vermont Technical College
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-TUFu3dfxC4cOr71gqbnptGczBbUgUZkt0Ckp39dAoz91x2/3wQCn6l6DnYTNP5Y162Tuh0/Rh23smg7!7bPbtzktTd4iwkqF7fqJliCEX5g212nG83EabJk5TTMwKGPdzndE2ZCaxqAxFoRuXLHWkKyaIrD+!wyExajKNzeSR2P7a6g==
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: 2934
X-Received-Bytes: 3046
X-Received-Body-CRC: 3412362206
Xref: news.eternal-september.org comp.lang.ada:25819
Date: 2015-05-11T18:49:37-04:00
List-Id: <comp.lang.ada>

On Mon, 11 May 2015, vincent.diemunsch@gmail.com wrote:

> It was easy in Spark 2005 :
>
> --# function Perm (A, B : Array_Type) return Boolean;
> --# assume Perm ( T~ [ I => T~(J); J => T~(I) ],  T~);
>
> Then you can prove that A is a permutation of B by proving that A 
> results from a sequence of permutations of two elements, starting with 
> B. It is the case in all sorting algorithm that I know (QuickSort, 
> HeapSort, etc.).
>
> Maybe you can also do that using "Ghost functions" in Spark 2014.

It is possible.

In the book on SPARK 2014 John McCormick and I recently wrote (available 
later this summer) we show an example of proving a sorting 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. The proofs can be processed with the 
upcoming SPARK GPL 2015 release, but I'm not sure if they will go through 
with SPARK GPL 2014.

Peter