Re: Lost in translation (with SPARK user rules)

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

Le Thu, 27 May 2010 13:57:58 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> So my approach is now to create user rules so that the Simplfier
> proves 100% of the VCs.  However this sometimes requires quite complex
> user rules that are difficult validate manually, so I use the Proof
> Checker to validate those rules by creating VCs that correspond to the
> rule and proving those.
This is close to my personal wish too, except I see a slight difference :  
I prefer to write very simple user rules, easily proved (like as easy to  
prove as using a truth table) and write Check based demonstrations relying  
on these rules. This is because I feel it is more safe (enforce soundness)  
and because it left more in the source in less in external documents (does  
not brake source navigability and layout logic).

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