SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Using PVS to Prove a Z Refinement: A Case Study
 by Dave W.J. Stringer-Calvert, Susan Stepney & Ian Wand.


The development of critical systems often places undue trust in the software tools used. This is especially true of compilers, which are a weak link between the source code produced and the object code which is executed. Stepney [23] advocates a method for the production of trusted compilers (i.e. those which are guaranteed to produce object code that is a correct refinement of the source code) by developing a proof of a small, but non trivial compiler by hand in the Z specification language. This approach is quick, but the type system of Z is too weak to ensure that partial functions are correctly applied.

Here, we present a re-working of that development using the PVS specification and verification system. We describe the problems involved in translating from the partial set theory of Z to the total, higher order logic of the PVS system and the strengths and weaknesses of this approach.



About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2019 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy