Re: Lost in translation (with SPARK user rules)

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 27 May, 13:36, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> Le Thu, 27 May 2010 13:57:58 +0200, Phil Thornley  
> <phil.jpthorn...@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).

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

Cheers,

Phil