Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!ucsd!ucbvax!pasteur!ladkin@icsib12
From: ladkin@icsib12 (Peter Ladkin)
Newsgroups: comp.theory
Subject: Re: Program correctness/proofs --SUMMARY
Keywords: proofs, program correctness
Message-ID: <27019@pasteur.Berkeley.EDU>
Date: 14 Aug 90 23:15:11 GMT
References: <6996@eos.UUCP>
Sender: news@pasteur.Berkeley.EDU
Reply-To: ladkin@icsib12 (Peter Ladkin)
Distribution: na
Organization: International Computer Science Institute, Berkeley, Ca.
Lines: 14
In-reply-to: jenlan@eos (Jennifer S Lanham)

In article <6996@eos.UUCP>, jenlan@eos (Jennifer S Lanham) writes:
>From Jon Jacky (jon@gaffer.rad.washington.edu)
> [....]  There are a couple of other program-proving
>products around, including something called Refine from Reasoning Systems in
>Palo Alto, CA.  

Refine is not a program-proving system. Its main use is in specification
and transformation of programs. For example, suppose you want to check
if a contractor's code meets your coding standards. Refine may be used
to build a checker for this. The inference capabilities in Refine are
currently limited to type checking and type inference for a standard
collection of data types plus sets and sequences.

Peter Ladkin