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

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

Yes, and yes. We do use Assume to describe the necessary mathematical 
properties involved. In particular we Assume the array after swapping two 
elements is a permutation of the original. Similarly we use Assume to 
embody the idea that permutations are transitive: if B is a permutation of 
A and C is a permtuation of B, then C is a permutation of A. This is 
necessary to support a loop invariant asserting that the partially 
processed array is always a permutation of the original.

In our example we leave the ghost functions unimplemented so the tools 
can't learn anything about them other than what we describe in the 
assertions associated with them. This also means the program won't link 
unless it's compiled with an Assertion_Policy of Ignore.

The ghost functions could potentially be implemented with actual code and 
then one might hope the tools could learn enough from them to do without 
some of the Assumes, for example via contextual analysis. However, some 
caution is needed. You don't want to use the sorting procedure to 
implement the permutation checker that you are using to prove the sorting 
procedure!

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

Well, SPARK GPL 2015 ships with two theorem provers that it uses together: 
alt-ergo and cvc4 (you can also add others, such as z3). So, by default, 
anything that either prover can prove is seen as handled from the user's 
point of view. Since the provers have different strengths the combination 
gives you better coverage than either one alone. However, it also 
increases the amount of code you have to trust.

There are various other improvements. For example it handles bit 
manipulation operators a lot better than SPARK GPL 2014. Just consider 
this simple case:

     type Octet is mod 2**8;
     type Double_Octet is mod 2**16;

     X : Octet;
     Y : Double_Octet;

...

     X := Octet(Y and 16#00FF);

As I recall SPARK GPL 2014 didn't understand that the masking operation 
chopped the size of the result into an acceptable range for type Octet and 
thus it complained that it couldn't prove there wasn't a range violation. 
SPARK GPL 2015 has no problem with the example above, and other similar 
examples.

Also my experience with using the 2015 version as opposed to the 2014 
version is that it requires a lot less fussing around with "obvious" 
things. Loop invariants, for example, can often be significantly 
simplified or even eliminated. The user experience with it is much better 
overall.

Non-linear floating point computations are still not handled that 
fantastically (I understand it's a hard problem). Thus if you are doing a 
lot of floating point work you may need to wait for more evolutionary 
improvements beyond even SPARK GPL 2015.

Peter