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=1.1 required=5.0 tests=BAYES_20,INVALID_DATE,
	MSGID_SHORT autolearn=no autolearn_force=no version=3.4.4
Path: utzoo!attcan!utgpu!jarvis.csri.toronto.edu!mailrus!cornell!oravax!davidg
From: davidg@oravax.UUCP (David Guaspari)
Newsgroups: comp.lang.ada
Subject: Re: Ada Specification Languages
Summary: Existing Ada specification languages
Keywords: Ada Anna
Message-ID: <1062@oravax.UUCP>
Date: 29 Sep 89 22:01:56 GMT
References: <1549@moondance.cs.uq.oz>
Organization: Odyssey Research Associates, Ithaca NY
List-Id: <comp.lang.ada>

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