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:
> I suspect it to see Result - 1, standing for the value of Result in the  
> Assert clause (and thus as the actual expression standing for Result),  
> as a monolithic subexpression. If this is really what happens, then it  
> would not see (Result + 1 + 1) as (Result - 1 + 1 + 1), and instead as  
> ((Result - 1) + 1 + 1), then see 1 + 1 as an expression, which is  
> simplifies to 2, getting ((Result - 1) + 2), which it could not simplify  
> any more, as it could not see -1 + 2 as a simplifiable expression,  
> because -1 belongs to a subexpression.

Note for readers : if you are not aware of how SPARK and Simplifier works,  
reading “see (Result + 1 + 1) as (Result - 1 + 1 + 1)”, you may believe  
I'm crazy ;) So here is how you should understand it : in the first  
expression, Result stands for its actual value, in the line starting with  
“--# check”. If you read carefully, you may notice between the line  
starting with “--# assert” and the one starting with “--# check”, the is a  
line “Result := Result + 1”. So, the previous value of Result, in terms of  
its actual one, is “Result - 1”. In the proofs, SPARK sees Result as an  
expression which is equivalent to its actual value. This expression is  
relative the value of Result in the line starting with “--# assert”. So  
(Result + 1 + 1) is an expression in the terms of the actual value of  
Result, as the program see it would see, and (Result - 1 + 1 + 1) is the  
same expression as SPARK see it. You may also, for better understanding,  
read it as (previous-value-of-Result - 1 + 1 + 1).

Hope this note helped readers to understand the likely strange things they  
may feel to have read here ;)

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