Show simple item record

dc.contributor.advisorAnderson, Stuart
dc.contributor.authorMaharaj, Savitri
dc.date.accessioned2004-03-03T11:28:37Z
dc.date.available2004-03-03T11:28:37Z
dc.date.issued1997-07
dc.identifier.urihttp://hdl.handle.net/1842/390
dc.description.abstractWe 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.en
dc.format.extent547304 bytes
dc.format.extent1119373 bytes
dc.format.extent828597 bytes
dc.format.mimetypeapplication/x-dvi
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.language.isoen
dc.publisherUniversity of Edinburgh. College of Science and Engineering. School of Informatics.en
dc.titleA Type-Theoretic Analysis of Modular Specificationsen
dc.typeThesis or Dissertation
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record