Using PVS to Prove a Z Refinement: A Case Study

David W. J. Stringer-Calvert; Susan Stepney; Ian Wand

Using PVS to Prove a Z Refinement: A Case Study

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

Computer Science

Research output: Contribution to conference › Paper › peer-review

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.

Original language	Undefined/Unknown
Pages	573-588
Publication status	Published - 1997

Access to Document

http://dx.doi.org/10.1007/3-540-63533-5_30

Cite this

@conference{7468c1e3c6c144a99cf22b52ff61ffde,

title = "Using PVS to Prove a Z Refinement: A Case Study",

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.",

author = "Stringer-Calvert, {David W. J.} and Susan Stepney and Ian Wand",

year = "1997",

language = "Undefined/Unknown",

pages = "573--588",

}

TY - CONF

T1 - Using PVS to Prove a Z Refinement

T2 - A Case Study

AU - Stringer-Calvert, David W. J.

AU - Stepney, Susan

AU - Wand, Ian

PY - 1997

Y1 - 1997

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

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

M3 - Paper

SP - 573

EP - 588

ER -