Re: Issue with SPARK 2014

["Phil Thornley" <phil.jpthornley@gmail.com>]

On Tuesday, 15 October 2015 18:28:39 UTC+1, Serge Robyns  wrote:
[snip]
> When trying to build a small standalone body I gets proved successfully 
> with the below code. However the call is using constant values.
> I'm wondering if the fact that here the prover has constants in the 
> procedure call makes it possible for him to prove it.

No, the use of constants in the procedure call is irrelevant.

> Now in essence the moves are either given by a player or selected by an 
> algorithm.  I was expecting that SPARK could prove the procedure by using 
> the procedure signature, in worst case pre/post conditions.

That's exactly what is done - the Evaluate_Board procedure is proved for all 
possible (valid) calls.

> The essence I'm trying to state in the loop invariant (which I've put to 
> shut up other SPARK messages) is that the count will never exceed a 
> certain range.  You can't have more "tiles" than there is space to put 
> them.

Every loop has a loop invariant (it's needed to cut the code as Stuart 
explained). If you don't supply one the SPARK tools create a default one.

The messages that you get without an explicit loop invariant are because the 
default loop invariant isn't strong enough for this code.

> Now I play with this code from time to time when I've an urge to make it 
> proven or when I read about how nice spark is.

[code snipped]

I don't think that you need more than one Loop_Variant in any loop, this is 
only needed to prove termination of the loop and just one valid loop variant 
should be enough.

Cheers,

Phil


---
This email has been checked for viruses by Avast antivirus software.
https://www.avast.com/antivirus


--- news://freenews.netfront.net/ - complaints: news@netfront.net ---