Re: Silly and stupid post-condition or not ?

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

On Feb 3, 3:13 am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:

> .... Something like SPARC, that requires an
> all-or-nothing approach, very often ends up with nothing.

I think this misrepresents the range of options available with SPARK.
Proofs can be anywhere in the range from fully formal from first
principles, through less formal proofs with user supplied rules (which
can themselves be supported by more or less formal justifications) to
the fully informal (proof by review).

I have always adopted "as formal as is reasonably practicable" and it
hasn't failed me yet.

> I think that things like SPARC can actually be harmful, as they focus
> attention on the wrong things. There is a lot that can be proved about
> dynamic constructs in Ada (far more than in other most languages), and it is
> unfortunate that instead of taking advantage of this (and making widely
> usable results), most of effort has been on proving the Fortran 66 subset of
> Ada. (I do see signs that this is changing, finally, but I think a lot of
> the work should have been done years ago.)
>

It would be nice to have some examples of what you have in mind here.

Cheers,

Phil