Abstract:

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, 1993] 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 hand 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.

@inproceedings(SS-FME97,
  author = "David W. J. Stringer-Calvert and Susan Stepney and Ian Wand",
  title = "Using {PVS} to Prove a {Z} Refinement: a case study",
  crossref = "FME97"
)

@proceedings(FME97,
  title = "FME '97: Formal Methods:
          Their Industrial Application and Strengthened Foundations,
          Graz, Austria, September 1997",
  booktitle = "FME '97: Formal Methods:
              Their Industrial Application and Strengthened Foundations,
              Graz, Austria, September 1997",
  editor = "C. Jones and J. Fitzgerald",
  series = "LNCS",
  volume = 1313,
  publisher = "Springer",
  year = 1997
)