Re: Critical code, Ada, Eiffel, Ariane etc.

[jsa@alexandria.organon.com (Jon S Anthony)]

In article <Pine.SUN.3.91.970812160036.17653A-100000@erlang.praxis-cs.co.uk> Peter Amey <pna@erlang.praxis-cs.co.uk> writes:

[... lot's of good stuff ...]

> The gains from simply using a predictable, secure language subset together
> with data and information flow analysis are quite significant.  It is
> possible to go further than this with SPARK and perform the sorts of DBC
> approach discussed in the Eiffel part of this thread.

Ah, but there is a _significant_ difference as you note below.

>  SPARK subprogams can have annotation in the form of pre and post
> condition expressions.  These, however, are not executable but can
> be mechanically checked by proof techniques.  Also of note is that
> these assertions may make statements about things which are not even
> visible according to the rules of Ada.

This is key.  The annotations are not _in the language_ and thus allow
for descriptions, invariants, etc. which can't be expressed _within_
the code for the <whatever> to be expressed outside of it.  This sort
of "meta" assertion can be checked by an extra language tool against
constraints specified for the context of use which the "component"
(and any assertions in the code) can't possibly have knowledge of.


> For example, we may want to assert that a stack is not full
> before allowing a push operation; however, we don't want to make the
> internal details of the stack visible to callers and might not even want
> to export a "NotFull" function.  SPARK annotations can handle cases like
> this by defining a proof function, which is invisible to the compiler,
> which can be used to express the precondition. 

Bingo.


> The issues that kept coming up about whether the presence of assertions
> can affect the behaviour of code simply do not apply to SPARK: the
> assertions are comments, but comments that can be checked against the code
> with tool support.

Absolutely.


> P.S. As for Ariane: yes it is quite clear that a proof of absence of
> run-time errors using the SPARK Examiner would have revealed the
> circumstances under which the Ariane code would fail; however, given
> the real problem -- the decision that off-the-shelf code did not
> require re-test -- it is almost certain that no re-proof would have
> been required either!

Completely agreed.  Excellent post.

/Jon
-- 
Jon Anthony
OMI, Belmont, MA 02178, 617.484.3383 
"Nightmares - Ha!  The way my life's been going lately,
 Who'd notice?"  -- Londo Mollari