[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: problem of pvs to z specification

It is not easy to translate the fragment of Z you give into PVS without
knowledge of the entire specification.  For example, I'd need to know how
you are representing Client, ID, and accounts in PVS.  Generally speaking,
delta schemas will translate into PVS functions, and the only tricky bit
in the NewAccount schema is the overriding taking place in what is
effectively an update extending the account function --- this should
translate to a PVS "WITH" expression, but it very much depends on the
representation you have chosen for account, and thereby whether you need a
plain update (:=) or domain extending update (|->) in the WITH.

One difficulty you will find in translating Z specifications into PVS
concerns the ubiquitous use of partial functions in Z (PVS provides only
total functions).  You can usually achieve the intent of a Z specification
that has partial functions by using (functions defined on) predicate
subtypes in PVS.  These will usually generate several proof obligations
(TCCs) to show that functions are not applied outside their domain--often
revealing significant errors along the way.  The Z/Eves tool provides a
"domain checker" that does similar checks directly on Z specifications
(Mark Saaltink's paper at ZUM'97 noted that it found out-of-domain errors
in *every* Z specification to which it has been applied).

Based on my own experience translating a very large Z specification into
PVS and proving properties about it, (See my paper at FM'97 - available
from my web page at http://www.csl.sri.com/~dave_sc) my personal view is
that you should not try to cast the Z specification directly into PVS, but
should treat it as a guideline and start afresh in PVS: the styles and
capabilities of the two languages are so different that a direct
translation does justice to neither.  Furthermore, the automation and
speed achieved in PVS proofs (and proofs and other forms of mechanized
analysis are the whole point of PVS) can vary widely with the style of
specification.  Direct translation of a Z specification is likely to lead
to difficult proofs in PVS because you're carrying along the baggage of
another specification language style.

If you want to try writing directly in PVS, you have to forget all about
schemas, sets, and so on and think in terms of theories, types, and
functions.  I would suggest carefully reading the PVS language and prover
guides, and the various tutorials available from the SRI web site at


Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com