jon@june.cs.washington.edu (Jon Jacky) (11/03/88)
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