Re: Lost in translation (with SPARK user rules)

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

On 27 May, 13:22, stefan-lu...@see-the.signature wrote:
[..]
> Wouldn't it be much simpler to use the proof checker, instead of the
> simplifier?

The main reason that I have for avoiding the Proof Checker for VCs
left after simplfication is that the proofs need to be repeated every
time the VCs are generated - which is OK except that small and
irrelevant changes to the code often break the proof scripts that you
have to keep to do the reproofs each time.
(And the Proof Checker provides no support for the maintenance of
existing scripts.)

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.

There are a couple of small examples of this in the Tokeneer code
distributed with SPARK GPL 8.1.1 - see code/core/tismain.rlu and code/
core/tismain/mainloopbody.rlu.

Cheers,

Phil