jon@june.cs.washington.edu (Jon Jacky) (10/14/88)
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
gore@eecs.nwu.edu (Jacob Gore) (10/16/88)
/ 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
ryer@inmet.UUCP (10/18/88)
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