Vendor introduces "safe" Ada subset

[jon@june.cs.washington.edu (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