Re: Proving Interface Specifications Correct.

To: Poetzsch-Heffter <poetzsch@informatik.tu-muenchen.de>
Subject: Re: Proving Interface Specifications Correct.
From: horning
Date: Wed, 09 Feb 94 15:26:33 -0800
Cc: larch-interest, detlefs, gnelson, evs@sds.lcs.mit.edu (David Evans)
Delivery-Date: Wed, 09 Feb 94 15:30:40 -0800
In-Reply-To: Message of Wed, 9 Feb 1994 09:56:29 +0100 from Poetzsch-Heffter <poetzsch@informatik.tu-muenchen.de>

Arnd,

This sounds like a very challenging project; I look forward to seeing your
results.  I don't know of any previous work on exactly this project, but
there are two different projects that each have some relation to what you
are attempting:

- Extended Static Checking, Dave Detlefs and Greg Nelson, here at SRC.
The main goal is not to prove satisfaction of interface specifications, but
to detect and diagnose "runtime errors" (e.g., array index out of bounds,
dereferencing NIL) statically ("at compile time").  The language is
Modula-3, but the method (conversion of programs to guarded command form)
might be applicable, depending on the form of your language semantics.
[detlefs@src.dec.com, gnelson@src.dec.com]

- LCLint, Dave Evans, MIT Laboratory for Computer Science.  The main goal
is to extend the power of lint-like checking of C programs by using partial
specifications written in a subset of LCL.  Right now, it supports checking
that abstract data type representations aren't violated, that only the
named global variables are accessed, that only the named variables are
modified, etc., but does not look at the requires and modifies clauses.
This should be ready for release soon.
[evs@lcs.mit.edu]

Jim H.