paul@batserver.cs.uq.oz (Paul Bailes) (09/18/89)
I'm looking for information about software specification languages developed or modified to have a specifically Ada flavour. For example, the March 85 issue of IEEE Software describes one such, called ``Anna''. * is ``Anna'' still a vital tool (ie being used, at least as a research tool) * are there any/many other descriptions of Anna * are there any other products like Anna Thanks in advance, Paul Bailes (paul@batserver.cs.uq.oz) (PS please post replies to comp.lang.ada - direct e-mail from the rest of the world to Australia doesn't ALWAYS work: addresses sometimes bounce)
davidg@oravax.UUCP (David Guaspari) (09/30/89)
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