[Prev][Next][Index]
A question
Sakthi Subramanian wrote:
> 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.
This question is interesting indeed,
however I would reformulate it as follows:
how can a specifier choose a logical framework
and/or a theorem proving tool to help in
expressing and analyzing
and checking a specification document?
are there any papers comparing the expressivity
of theorem proving tools and logical frameworks
from the point of view of sw engineering?
I know several papers comparing for instance Z and VDM and Larch,
and some papers showing how a specific theorem prover
(eg LP, PVS, HOL, Isabelle, Ergo, etc.) can
be used say for proving Larch or Z or Unity formulae
(thus helping in the analysis of a formal document
written with those formalisms),
but how can we, as "formal" sw engineers,
know which tool is useful for what?
Is this a correct and interesting question?
Many thanks for any answer.
Paolo
--
Prof. Paolo Ciancarini
Dept. of Computer Science, Univ. of Bologna
Pza. di Porta S.Donato, 5 -- 40127 Bologna - Italy
tel. +39 51 354506 fax. +39 51 354510 e-mail: cianca@cs.unibo.it
WWW Home page: http://www.cs.unibo.it/~cianca/index.html