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.8 required=5.0 tests=BAYES_00,INVALID_DATE, MSGID_SHORT autolearn=no autolearn_force=no version=3.4.4 Path: utzoo!attcan!uunet!lll-winken!lll-tis!ames!mailrus!cornell!uw-beaver!uw-june!jon From: jon@june.cs.washington.edu (Jon Jacky) Newsgroups: comp.lang.ada Subject: Re: "Safe" Ada and program verification Keywords: Ada, Spark, SPADE, software safety, verification, formal methods Message-ID: <6316@june.cs.washington.edu> Date: 2 Nov 88 16:37:18 GMT Organization: U of Washington, Computer Science, Seattle List-Id: A few of you have written back to me with comments or questions about Spark, a n Ada subset marketed by Program Validation Ltd, of Southampton, England. Spark is claimed to promote "safe" programming. It accomplishes this by omitting Ada features thought to be problematical, including tasks, generic units, access types, "declare" statements, "go to" statements, and exceptions. There's an important piece of information I didn't include with the original posting (it wasn't in the news story). This vendor also sells a program verification tool called SPADE. Although the news release didn't mention this , I'll bet Spark is tailored to SPADE, and the constructs available in Spark are just the ones that happen to be handled by SPADE. Program Validation also sells products that adapt other languages to SPADE, including Pascal and 8080 assembler (!). I'll bet Spark is just the latest of these. Spark is not the only attempt to define a verifiable Ada subset. A recent issue of ACM Ada Letters describes work by Odyssey Research Associates on a dialect called Ada' (that's "Ada-prime", I guess) and work by Computational Logic, Inc. on a dialect called AVA ("A verifiable (or "vanilla") Ada"). I go t the impression these two were research efforts, not products like Spark. Like Spark, they both eliminate a lot of constructs in order to match the language to practical verification techniques. Both agree that exceptions create difficulties and apparently restrict them to some degree, though perhaps not a s much as Spark. Not everyone agrees that exception handlers promote safety. In particular, many British advocates of formal methods (whence Spark comes) abhor them. Soon after Ada was first announced, C.A.R. Hoare wrote: "The danger of exception handling is that an 'exception' is too often a sympto m of some entirely unrelated problem. ... The right solution is to treat all exceptions in the same way as symptoms of disaster; and switch the entire operating regime to one designed to survive arbitrary failure of the entire computer running the program which generated the exception." Exactly this approach is taken by the new VIPER microprocessor, which comes from the same community. VIPER's design is formally verified, its architectur e is intended for safety-critical applications, and I suspect it is the intended target for Spark. Any run time error causes VIPER to halt! - Jonathan Jacky, University of Washington (I haven't used any of these tools or techniques or dealt with any of these vendors, so I have no opinions about them. I'm just passing along information I've seen in journals, trade publications, and meetings.) REFERENCES A good introduction to the SPADE approach is in: B.A. Carre, Software Validation, MICROPROCESSORS AND MICROSYSTEMS 4(10), 395 - 406, 1980. A brief introduction to the SPADE tool (I didn't find it as informative as the previous reference) is: Carre BA, O'Neill IM, Clutterbuck DL and Debney CW. SPADE - the Southampton analysis and development environment. In: Sommerville, I (ed.) Software Engineering Environments, London: Peter Peregrinus Ltd. 1986. A more detailed description of the theory and details of SPADE are in: Bergeretti, J-F, and Carre B, Information flow and data flow analysis of while-programs. ACM Transactions on Programming Languages and Systems, 1985 7(1), 37 - 61. An interesting SPADE application to - of all things - an 8080 assembler progra m is: Clutterbuck DL and Carre BA, The verification of low level code, SOFTWARE ENGINEERING JOURNAL (a publication of the British IEE) May 1988 96 - 110. Other efforts to define verifiable Ada dialects are discussed in: Cohen NH, Nyberg K, Guaspari D, Polak W, Smith MK. Formal methods committee report, ACM Ada Letters 8(4), July/August 1988, pps. 136 - 142. C.A.R Hoare on exceptions: Letter, COMMUNICATIONS OF THE ACM, vol 24, no 7, July 1981, p. 477. VIPER Microprocessor: There is a short blurb in the current (Nov. 1 1988) issue of the trade paper COMPUTER DESIGN (p. 41 - 42). VIPER and the British formal methods approach was the subject of much animated discussion at the COMPASS '88 conference last June. Some of it is reported in a trip report that will appear in the Oct. 1988 issue of ACM Software Engineering Notes. VENDORS Spark, SPADE: Program Validation Ltd, 34 Bassett Crescent East, Southampton SO 2 3FL, Tel. 0703-767841. Ada': Odyssey Research Associates, 301A Harris B. Dates Drive, Ithaca, NY 14850, (607)-277-2020 AVA: Computational Logic Inc. 1717 W 6th, Suite 290, Austin TX 78703, (512)-322-9951