From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: * X-Spam-Status: No, score=1.1 required=5.0 tests=BAYES_20,INVALID_DATE, MSGID_SHORT autolearn=no autolearn_force=no version=3.4.4 Path: utzoo!attcan!uunet!husc6!ukma!mailrus!cornell!uw-beaver!uw-june!jon From: jon@june.cs.washington.edu (Jon Jacky) Newsgroups: comp.lang.ada Subject: Vendor introduces "safe" Ada subset Keywords: Ada, safety, verification, formal methods, Spark, Viper Message-ID: <6073@june.cs.washington.edu> Date: 14 Oct 88 16:06:29 GMT Organization: U of Washington, Computer Science, Seattle List-Id: 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