howell@COMMUNITY-CHEST.MITRE.ORG (10/16/88)
[forwarded from Risks-forum. Chuck Howell] Date: Fri, 14 Oct 88 09:04:38 PDT From: jon@june.cs.washington.edu <Jonathan Jacky, University of Washington> Subject: Vendor introduces "safe" Ada subset From ELECTRONIC ENGINEERING TIMES, 26 Sept 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.