home > publications > Z > *Using
PVS to Prove a Z Refinement*

### David W. J. Stringer-Calvert, Susan Stepney, Ian
Wand.

Using PVS to Prove a Z Refinement: a case study.

#### In C. Jones, J. Fitzgerald, editors. *FME '97:
Formal Methods: Their Industrial Application and Strengthened Foundations,
Graz, Austria, September 1997*. LNCS 1313. Springer, 1997.

**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.

More on the

**Full paper** : PDF 243K

@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
)