* Re: Ada Specification Languages
1989-09-18 4:31 Ada Specification Languages Paul Bailes
@ 1989-09-29 22:01 ` David Guaspari
0 siblings, 0 replies; 2+ messages in thread
From: David Guaspari @ 1989-09-29 22:01 UTC (permalink / raw)
In reponse to the posting about Ada specification languages:
1. The language you asked about, Anna, exists. A group at Stanford
University, headed by David Luckham, has been and still is building
tools. I don't know what's available, but I've seen the tools demoed,
and goofed with some myself, two years ago. Anna applies to
sequential programs. The same bunch, more or less, is also working on
TSL (task sequencing language), which can specify the order in which
tasks rendezvous with one another (thouh no the information passed at
rendezvous). These languages are especially suited for run-time
checking of specifications. Their address is
Computer Science Laboratory
Stanford University
Stanford CA 94305-2192
2. Advertisement: my group is building a formal verification system
for (sequential) Ada programs. The system is called Penelope, and its
specification language, called Larch/Ada, has lots in common with Anna
but is easier to analyze mathematically. It's very much a prototype.
If you want information, write the project manager:
Maureen Stillman
Odyssey Research Associates
301A Harris B. Dates Dr.
Ithaca, NY 14950-1313
3. Other groups are also working on formal verification systems (and
therefore need to devise formal specification languages of their own).
You can try:
Mike Smith
Computational Logic Inc.
1717 W. 6th St. Suite 290
Austin, TX 78703
Mel Cutler
Aerospace Corporation
(In California, I don't have their address at hand)
B.A. Carre and T.J. Jennings
Dept. of Electronics and Computer Science
University of Southampton
(UK)
B. Krieg-Bruckner
FB 3 Mathematik und Informatik
Universitat Bremen
Postfach 330 440, D- 2800 Bremen 33
(West Germany)
David Guaspari
oravax!davidg@cu-arpa.cs.cornell.edu
^ permalink raw reply [flat|nested] 2+ messages in thread