Re: SPARK : surprising failure with implication

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Thu, 03 Jun 2010 10:54:51 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> The original context in Ada/SPARK source is of the form (the above C1  
> stands for the Check clause):
>
>     --# assert ..... U'Pos (Result + 1) .....
>     .....
>     Result := Result + 1;
>     .....
>     --# check .... U'Pos (Result + 1 + 1) ....

If you meet a similar case as the above message, the only workable  
workaround seems to use an intermediate variable like in:

     --# assert ..... U'Pos (Result + 1) .....
     .....
     Previous_Result := Result;
     Result := Previous_Result - 1;
     .....
     --# check .... U'Pos (Previous_Result + 1) ....

I suppose some of you guessed this in an extract of a loop (the Check  
clause is the start of the proof of a loop invariant).

BTW, I've made a mistake in the previous transcription, this was “Result  
:= Result - 1;” (sorry for that)

I will not give other examples, I will just say using intermediate  
variables oftenly help with SPARK. But take care: while doing so, avoid to  
introduce additional RTC VC which will turn your proof into a more  
complicated story, and to avoid this misadventure, you should only use  
this technique to backup previous values of a variable which is modified  
since a previous Assert clause (a copy between two variables of the same  
type does not introduce RTC VC, so it's OK).

Have a nice day all.

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.