Re: Lost in translation (with SPARK user rules)

["Peter C. Chapin" <pcc482719@gmail.com>]

Dmitry A. Kazakov wrote:

> Rather by refining the contracts. When you feel that the implementation is
> mature, you can add more promises to the contract of and see if they hold
> (=provable). If they don't you could try to re-implement some parts of it.
> When you feel that it takes too much time, is impossible to prove, you can
> drop the idea to do it formally. You will sill have a gain of deeper
> understanding how the thing works and could document why do you think it is
> correct, even if that is not formally provable.

I think this is a good way to work with SPARK. I'm developing a SPARK program
now. I started with the specifications, working with them until I felt
comfortable with the overall structure of the program. Refactoring at that
stage was very cheap and I did it several times.

I just finished coding the body of the one of the critical packages. The SPARK
Examiner was very helpful at catching silly errors that I might have missed.
In one case I forget to condition a flag at the end of a procedure and was
told that my code did not agree with my annotations. Nice.

Next I was able to prove the code free of runtime errors. This worked out
quite easily in this case. After changing two declarations to use properly
constrainted subtypes (rather than just Natural as I had originally... my
bad), the SPARK simplifier was able to discharge 96% of the VCs "out of the
box." The remaining ones were not hard to fix. I felt lucky!

Now I hope to encode some useful and interesting information about the
intended functionality of the subprograms in SPARK annotations (#pre, #post,
etc), and see if I can still get the proofs to go through. Somewhere around
now I will also start building my test program. One thing that I like about
SPARK is that you can do a lot of useful things with it without worrying
about stubbing out a zillion supporting packages for purposes of creating a
test program.

I do agree certainly that SPARK is not for everything. The code I'm working on
is (potentially) security sensitive so the extra effort of working with SPARK
seems worthwhile. My test harness, on the other hand, is likely to be in full
Ada.

Peter