Re: Lost in translation (with SPARK user rules)

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

Le Thu, 27 May 2010 15:38:27 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> I very much agree with this approach - adding a sequence of check
> annotations so that the rules required are easy to validate. However
> you have to balance this against the size of the annotations required.
>
> For example, a few years ago I was trying to prove the correctness of
> code for a red-black tree, the single rotation procedure was four
> lines of code, but it took about 60 lines of check annotations plus a
> bunch of quite complex rules, to prove that the tree stayed a valid
> binary tree (and I never got round to proving the colour invariants).
At least, I've noticed that while user rules can have an impact on speed  
of Simplifier, this is not the most important. Check (and so assert also)  
seems to have the most significant impact. What is worth to note : a long  
and explicit proof does not implies it is a slower one (the Simplifier is  
mostly slow when it fails to prove something, and is faster when it  
success).

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