A question

• To: garland@larch.lcs.mit.edu
• Subject: A question
• From: sakthi@ba.tis.com (Sakthi Subramanian)
• Date: Fri, 20 Oct 95 10:17:02 PDT
• Cc: ns@cage.rug.ac.be, garland@lcs.mit.edu, larch-interest@pa.dec.com
• Delivery-Date: Fri, 20 Oct 95 10:29:53 -0700

Hi, all! This maybe a naive question. But I have always wondered why
one shouldn't use a proven powerful verification system such as Nqthm
(Boyer-Moore theorem prover) for specification of programs. After all
when you verify a program you have to express the specification of the
program.  Nqthm has been used sucessfully to verify programs in a
number of languages. So why not use that? Why use systems like Larch
and LP which are specifically geared only to express specifications and
not verification? Of course there are cosmetic differences like one is
a typed language and the other is not, etc. But I think these can be
ignored.

sakthi

........................................................................
  Sakthi Subramanian                     Office Phone: (415) 962-8885 ext 3005.
  Computer Scientist
  Trusted Information Systems             FAX: (415) 962-9330.
  444 Castro Street, Suite 800,           email: sakthi@ba.tis.com
  Mountain View, CA 94041.
........................................................................



        

• Re: A question
• From: "Stephen J. Garland" <garland@larch.lcs.mit.edu>

• Prev: Re: A question
• Next: Re: Some questions about Larch
• Index: Larch archive index