Implementing Z in LEGO

Citation

Maharaj S (1990) Implementing Z in LEGO. Master of Science. University of Edinburgh.

Abstract
The formal notation known as Z has generated widespread interest within the field of software engineering and has been used for the specification of a varied selection of computer-based systems. While Z offers a precise mathematical notation for the specification of systems and the formulation of theorems regarding the behaviour of these systems, proving these theorems is generally a matter of intuition or of traditional pen and paper methods of theorem proving. Lego provides a proof-checking environment wherein mathematical structures can be modelled and theorems proved with confidence that the proofs are logically valid within the chosen model. The aim of this project is to complement the Z notation with the proof-checking capabilities of Lego by implementing Z within Lego. The first step is to translate into Lego a selection of the mathematical concepts most frequently used in Z specifications. Thus the various methods of representing sets, functions, relations and numbers in Lego are examined and particular ones chosen for implementation. These are then implemented and a number of theorems about the resulting models are proven. These provide a library of rules for use in Z proofs. A Z specification example is then translated into Lego by means of this implementation. Two theorems about the specification are formulated, expressed in Lego and then proved by the use of the library of definitions and rules and Lego's own proof-checking capacity.