Re: Lost in translation (with SPARK user rules)

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

Le Thu, 27 May 2010 14:22:26 +0200, <stefan-lucks@see-the.signature> a  
écrit:
> Wouldn't it be much simpler to use the proof checker, instead of the
> simplifier?
>
> Stefan
>
I don't like the checker, this is an external tool (... and not an handy  
one), to me, SPARK is a language, not a tool. And further more, I really  
prefer to write proofs in source, because this is what I am expecting of  
such a thing as program proof is (I don't bother about adding a user rules  
file, although I would like a way to not need to copy it every where it is  
needed and have it to be loaded all time automatically).

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