Re: Lost in translation (with SPARK user rules)

[Mark Lorenzen <mark.lorenzen@gmail.com>]

On 27 Maj, 00:01, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
>
> 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 would like to suggest that you always use the mandatory annotations
(of course)
*and also* the #pre annotation. The use of preconditions can
drastically improve
the Simplifier's ability to discharge VCs. You already discovered that
effect when
you introduced constrained subtypes. Furthermore you don't have to
think about
ways to make your subprograms total by using "nil" values or error
flags, which
also relieves the calling subprogram from checking for such "nil"
values and
error flags.

Then, if you are bold, you can start to think about writing
postconditions.
*However*, if the criticality of your program *requires* the use of
postconditions,
I suggest that you introduce them from the beginning on as their
introduction they
may require some reworking (often simplification) of your code.

- Mark L