Re: {Pre,Post}conditions and side effects

[vincent.diemunsch@gmail.com]

Le mardi 12 mai 2015 00:49:40 UTC+2, Peter Chapin a écrit :

> 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. 

Tell us more ! Do you use the same basic idea : assuming that the swap function is
an elementary permutation of arrays ? Do you use an assume statement ?

> 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.

What is new with the SPARK GPL 2015 prover ?

Regards,

Vincent