Critical code, Ada, Eiffel, Ariane etc.

Critical code, Ada, Eiffel, Ariane etc.

[Peter Amey]

Recent, interesting, threads on programming safety-critical systems,
language subsets, assertions, DBC etc. were kicked off by some kind
remarks by Tucker Taft about SPARK, our secure, Ada subset.  Now that the
dust has settled a bit I thought I would return to the original themes and
explain why we believe SPARK addresses some of the issues raised. 

I think two main themes emerged: 

(1) Languages: special versus general, benefit of subsets, how are subsets
constructed? 

(2) Assertions versus exceptions, DBC etc. 

(there was also the usual sub-topic of whether each writer's preferred
method would have prevented the Ariane 5 failure - I will briefly return
to that later). 

Languages
---------

The decision to subset Ada rather than invent a new "perfect" language is
a pragmatic one.  A special-purpose language cannot hope to get the volume
of support needed to gain wide use.  By using a standard language as a
base we gain access to a range of compiler vendors, a range of target
processors, books, training material and a pool of staff.  All of these
have to be created from scratch if a completely new language is chosen. 
In the design of SPARK we chose to maximise the amount we could exploit
these resources whilst still producing a language with the qualities
essential for critical work: complete predictability coupled with
sufficient expressive power to do a properly-engineered job.  To this end
SPARK is compiler-independent: a SPARK program is guaranteed to have the
same meaning when compiled with any validated compiler.  Put another way,
a SPARK program cannot be "erroneous" in the Ada 83 LRM sense. 

There is a widespread misconception, reflected in this thread, that
producing a safe language subset is simply a matter of deciding what to
leave out; this is not true.  In many cases what is needed is a way of
providing more information so that rules can be properly checked (there is
no point inventing language rules that cannot be enforced).  For example,
SPARK has rules that ensure that a program is free from evaluation-order
dependencies.  One of these rules requires that functions cannot have
side-effects.  It is quite difficult to show that a function has no
side-effects (at least in computationally efficient ways) without some
extra information.  SPARK provides this by means of annotations, or formal
comments, one of which - the global annotation - provides the information
needed for the tools to confirm that a function is free from side-effects. 
There are many cases like this. 

Another misconception is that any language can be rendered "safe" by
subsetting and that all such subsets tend to look the same.  Neither is
true.  A subset must be based on reasonably firm foundation - something
that Ada provides.  Furthermore, we want the subset to retain language
properties that enable things such as abstraction to be properly handled. 
Thus SPARK includes packages, private types, functions returning
structured objects etc.  A subset of C, for example, would not have
SPARK's properties in this respect. 

Assertions etc.
---------------

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.  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.  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. 

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.  Also the issue concerning the effective difference
between executable assertions and execptions is not applicable to SPARK:
using SPARK we can show the code to be exception-free prior to execution. 
This proof can also show the absence of Ada-defined run-time errors such
as constraint errors. 

The use of secure subsets and static analysis makes it harder to put bugs
in the code; furthermore, it makes their early detection easier which
offers dramatic savings in the integration test phase of a project (80%
reduction in integration test costs has been quoted).  Furthermore, SPARK
is not a toy, prototype or even partially completed piece of academic
research - it is a real industrial strength tool usable, and used, on real
projects. 

Peter

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! 

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

[Ken Garlington]

Peter Amey wrote:
> 
> Recent, interesting, threads on programming safety-critical systems,
> language subsets, assertions, DBC etc. were kicked off by some kind
> remarks by Tucker Taft about SPARK, our secure, Ada subset.  Now that the
> dust has settled a bit I thought I would return to the original themes and
> explain why we believe SPARK addresses some of the issues raised.
> 
[much good discussion snipped]
> 
> The use of secure subsets and static analysis makes it harder to put bugs
> in the code; furthermore, it makes their early detection easier which
> offers dramatic savings in the integration test phase of a project (80%
> reduction in integration test costs has been quoted).  Furthermore, SPARK
> is not a toy, prototype or even partially completed piece of academic
> research - it is a real industrial strength tool usable, and used, on real
> projects.

As I recall, SPARK was used in the development of the C-130 airlifter
real-time mission-critical avionics, so I believe that it is quite
accurate
to say that SPARK has been used on "real" projects in an environment
very
similar to the Ariane 5.

I also think SPARK addresses many of my concerns with Eiffel-style
assertions
(and Ada-style exceptions), although there are still issues about the
number
and types of proofs generated. 

> Peter
> 
> 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!

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

[Brian Rogoff]

Peter,
	I looked at the Praxis web page, and noticed that generic units are 
excluded from the Spark subset. What are the reasons for this choice? 

-- Brian

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

[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

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

[Gavin Finnie]

In article <Pine.SGI.3.95.970813191536.1634A-100000@shellx.best.com>,
Brian Rogoff  <bpr@shellx.best.com> wrote:

>	I looked at the Praxis web page, and noticed that generic units are 
>excluded from the Spark subset. What are the reasons for this choice? 

SPARK has so far totally excluded generics on the grounds of complexity, in
terms of defining a formal model of generics, the additional static analysis
and proof work required, and the effect on human understanding of the source
code (and hence the potential for errors) when generics are used.

However, we recognise that the controlled use of simple generics can assist in
creating re-usable abstractions that can make code easier to structure,
understand and reason about. Also, certain flaws in Ada 83's contract
model have been fixed in Ada 95. We are therefore considering providing limited
support for generics in a future version of SPARK.

Gavin Finnie

Praxis Critical Systems Ltd                Tel (+44) 01225-466991
20 Manvers Street                          Fax (+44) 01225-469006
Bath BA1 1PX
UK

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

[Robert Dewar]

Gavin says

<<SPARK has so far totally excluded generics on the grounds of complexity, in
terms of defining a formal model of generics, the additional static analysis
and proof work required, and the effect on human understanding of the source
code (and hence the potential for errors) when generics are used.>>

Another issue here is complexity in the SPARK examiner itself. Certainly
the SPARK examiner can handle any language construct, since it can certainly
become equivalent to an Ada 95 compiler (indeed we are looking at the issue
of implementing a pragma Restrictions (SPARK) or somesuch in GNAT).

But the examiner is much more than a syntax checker, and part of the 
integrity of the SPARK approach involves keeping the examiner small
and much simpler than a full compiler. So an issue like the addition of
generics has to be considered from this point of view as well.