Vendor introduces "safe" Ada subset

Vendor introduces "safe" Ada subset

[Jon Jacky]

The following article appeared in ELECTRONIC ENGINEERING TIMES,
Sept. 26, 1988, p. 25:

ADA SUBSET ADDRESSES SOFTWARE SAFETY

Southampton, England - (A subset of Ada called Spark) is reported to 
overcome the drawbacks of (Ada) in applications where software integrity
is critical. ...

Spark was developed at the University of Southampton with the sponsorhip of
the British Ministry of Defence.  It is now being marketed by Program 
Validation Ltd.  

(A representative of Program Validation) said that 
the use of Ada for safety critical programming poses some
serious problems.  There is no formal definition of the language and the
precise meaning of some its constructions is unclear.  According to Program
Validation, the resulting uncertainties make formal verification of Ada 
programs impossible and cast doubts on the integrity of the compiled code.
A further complication is that the richness of Ada allows programs to be
constructed that are apparently simple, but hide great underlying complexity.

... To achieve Ada integrity, Spark has introduced several restrictions.  It
does not allow the use of tasks, exceptions or generic units.  Access types 
are also omitted, as these are considered unacceptable in real-time safety
critical applications.  ... Certain features - such as "go to" statements
and "declare" statements - are totally barred.

- Jonathan Jacky, University of Washington

Re: Vendor introduces "safe" Ada subset

[Jacob Gore]

/ comp.lang.ada / jon@june.cs.washington.edu (Jon Jacky) / Oct 14, 1988 /
>... To achieve Ada integrity, Spark has introduced several restrictions.  It
>does not allow the use of tasks, exceptions or generic units.  Access types 
>are also omitted, as these are considered unacceptable in real-time safety
>critical applications.  ... Certain features - such as "go to" statements
>and "declare" statements - are totally barred.

Interesting.  Removing EXCEPTIONS to achieve safe programming?

Sounds like what's left is Modula-2 with overloading (or is that "barred"
also?).

Jacob Gore				Gore@EECS.NWU.Edu
Northwestern Univ., EECS Dept.		{oddjob,gargoyle,att}!nucsrl!gore

Re: Vendor introduces "safe" Ada subset

[ryer]

Regarding:

>... To achieve Ada integrity, Spark has introduced several restrictions.  It
>does not allow the use of tasks, exceptions or generic units.  Access types 
>are also omitted, as these are considered unacceptable in real-time safety
>critical applications.  ... Certain features - such as "go to" statements
>and "declare" statements - are totally barred.

From a compiler writer's viewpoint, generics, exceptions, and even tasks are
just compile-time notions:  We know *exactly* how to translate them to
simpler language features.  For example the compiler creates new (non-generic)
code for each instantiation of a generic.  It converts tasking constructs into
calls on subprograms which themselves are written in Ada without using tasking.
Ultimately there is a piece of hardware at the bottom that only has gotos and
a handful of datatypes.

I appreciate the *complexity* of doing any kind of program proving in
the presence of generics, separate compilation, tasking, exceptions, and
so on.  What I find irritating is the often repeated premise that one
*must* subset in order to make proving feasible.  If a compiler can translate
generics into non-generic code, why can't a program prover do the same?

What if my application *needs* more than one thread of control, because of
multiple asynchronous interactions with the outside world?  Am I to implement
a full executive in Ada (or assembler) and prove it?  If so, how is this any
easier than proving the implementation of the tasking semantics that happen
to be built into Ada already?

If exceptions are not permitted, I presume that the prover is able to prove
that no exceptions such as numeric error or constraint error can ever occur.
If so, it can *surely* also tell whether a given raise statement is going
to be executed and when (i.e. which handler will be activated).  If I were
on an airplane, I'd rather believe that there was an appropriate handler for
every possible exceptional condition than that someone had mathematically
proven that the *source code* of the flight control software would never
cause an exception.

There is no doubt that Spark is *easier* to prove than Ada.  If the claim
is being made that full Ada is inherently unprovable, I'd like to see
the proof.

Please excuse the flame, which is personal, not corporate.
Mike Ryer
Intermetrics