Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >

Please use this identifier to cite or link to this item:

This item has been viewed 7 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
ECS-LFCS-97-354.dviLaTeX DVI File534.48 kBTeX dviView/Open
ECS-LFCS-97-354.pdfAdobe PDF1.09 MBAdobe PDFView/Open
ECS-LFCS-97-354.psPostScript File809.18 kBPostscriptView/Open
Title: A Type-Theoretic Analysis of Modular Specifications
Authors: Maharaj, Savitri
Supervisor(s): Anderson, Stuart
Issue Date: Jul-1997
Publisher: University of Edinburgh. College of Science and Engineering. School of Informatics.
Abstract: We study the problem of representing a modular specification language in a type-theory based theorem prover. Our goals are: to provide mechanical support for reasoning about specifications and about the specification language itself; to clarify the semantics of the specification language by formalising them fully; to augment the specification language with a programming language in a setting where they are both part of the same formal environment, allowing us to define a formal implementation relationship between the two. Previous work on similar issues has given rise to a dichotomy between "shallow" and "deep" embedding styles when representing one language within another. We show that the expressiveness of type theory, and the high degree of reflection that it permits, allow us to develop embedding techniques which lie between the "shallow" and "deep" extremes. We consider various possible embedding strategies and then choose one of them to explore more fully. As our object of study we choose a fragment of the Z specification language, which we encode in the type theory UTT, as implemented in the LEGO proof-checker. We use the encoding to study some of the operations on schemas provided by Z. One of our main concerns is whether it is possible to reason about Z specifications at the level of these operations. We prove some theorems about Z showing that, within certain constraints, this kind of reasoning is indeed possible. We then show how these metatheorems can be used to carry out formal reasoning about Z specifications. For this we make use of an example taken from the Z Reference Manual (ZRM). Finally, we exploit the fact that type theory provides a programming language as well as a logic to define a notion of implementation for Z specifications. We illustrate this by encoding some example programs taken from the ZRM.
Appears in Collections:Informatics thesis and dissertation collection

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.


Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy