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=0.5 required=5.0 tests=BAYES_00,TO_NO_BRKTS_PCNT autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,4835289e9b0eb32d,start X-Google-Attributes: gid103376,public From: Peter Amey Subject: Critical code, Ada, Eiffel, Ariane etc. Date: 1997/08/12 Message-ID: X-Deja-AN: 263737737 Organization: Praxis plc, U.K. Newsgroups: comp.lang.ada Date: 1997-08-12T00:00:00+00:00 List-Id: Recent, interesting, threads on programming safety-critical systems, language subsets, assertions, DBC etc. were kicked off by some kind remarks by Tucker Taft about SPARK, our secure, Ada subset. Now that the dust has settled a bit I thought I would return to the original themes and explain why we believe SPARK addresses some of the issues raised. I think two main themes emerged: (1) Languages: special versus general, benefit of subsets, how are subsets constructed? (2) Assertions versus exceptions, DBC etc. (there was also the usual sub-topic of whether each writer's preferred method would have prevented the Ariane 5 failure - I will briefly return to that later). Languages --------- The decision to subset Ada rather than invent a new "perfect" language is a pragmatic one. A special-purpose language cannot hope to get the volume of support needed to gain wide use. By using a standard language as a base we gain access to a range of compiler vendors, a range of target processors, books, training material and a pool of staff. All of these have to be created from scratch if a completely new language is chosen. In the design of SPARK we chose to maximise the amount we could exploit these resources whilst still producing a language with the qualities essential for critical work: complete predictability coupled with sufficient expressive power to do a properly-engineered job. To this end SPARK is compiler-independent: a SPARK program is guaranteed to have the same meaning when compiled with any validated compiler. Put another way, a SPARK program cannot be "erroneous" in the Ada 83 LRM sense. There is a widespread misconception, reflected in this thread, that producing a safe language subset is simply a matter of deciding what to leave out; this is not true. In many cases what is needed is a way of providing more information so that rules can be properly checked (there is no point inventing language rules that cannot be enforced). For example, SPARK has rules that ensure that a program is free from evaluation-order dependencies. One of these rules requires that functions cannot have side-effects. It is quite difficult to show that a function has no side-effects (at least in computationally efficient ways) without some extra information. SPARK provides this by means of annotations, or formal comments, one of which - the global annotation - provides the information needed for the tools to confirm that a function is free from side-effects. There are many cases like this. Another misconception is that any language can be rendered "safe" by subsetting and that all such subsets tend to look the same. Neither is true. A subset must be based on reasonably firm foundation - something that Ada provides. Furthermore, we want the subset to retain language properties that enable things such as abstraction to be properly handled. Thus SPARK includes packages, private types, functions returning structured objects etc. A subset of C, for example, would not have SPARK's properties in this respect. Assertions etc. --------------- The gains from simply using a predictable, secure language subset together with data and information flow analysis are quite significant. It is possible to go further than this with SPARK and perform the sorts of DBC approach discussed in the Eiffel part of this thread. SPARK subprogams can have annotation in the form of pre and post condition expressions. These, however, are not executable but can be mechanically checked by proof techniques. Also of note is that these assertions may make statements about things which are not even visible according to the rules of Ada. For example, we may want to assert that a stack is not full before allowing a push operation; however, we don't want to make the internal details of the stack visible to callers and might not even want to export a "NotFull" function. SPARK annotations can handle cases like this by defining a proof function, which is invisible to the compiler, which can be used to express the precondition. The issues that kept coming up about whether the presence of assertions can affect the behaviour of code simply do not apply to SPARK: the assertions are comments, but comments that can be checked against the code with tool support. Also the issue concerning the effective difference between executable assertions and execptions is not applicable to SPARK: using SPARK we can show the code to be exception-free prior to execution. This proof can also show the absence of Ada-defined run-time errors such as constraint errors. The use of secure subsets and static analysis makes it harder to put bugs in the code; furthermore, it makes their early detection easier which offers dramatic savings in the integration test phase of a project (80% reduction in integration test costs has been quoted). Furthermore, SPARK is not a toy, prototype or even partially completed piece of academic research - it is a real industrial strength tool usable, and used, on real projects. Peter P.S. As for Ariane: yes it is quite clear that a proof of absence of run-time errors using the SPARK Examiner would have revealed the circumstances under which the Ariane code would fail; however, given the real problem -- the decision that off-the-shelf code did not require re-test -- it is almost certain that no re-proof would have been required either!