Browse by author
Lookup NU author(s): Dr Leo Freitas
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
We propose a unifying theory of undefined expressions in logics used for formally specifying software systems. We show how to use classical logic to prove facts in a monotonic partial logic with guards, and we exhibit guards for several different semantical systems. We show how classical logic can be used to prove semi-classical facts. The mechanical theorem prover Z/Eves is used to prove facts about semi-classical Z specifications, although it uses classical logic; it does this with guards from McCarthy logic. It can also be used to prove facts about VDM specifications. The use of left-to-right guards guarantees, for example, that every theorem proved in Z/Eves is valid in VDM and in Z.
Author(s): Woodcock J, Saaltink M, Freitas L
Editor(s): Broy, M., Sitou, W., Hoare, T.
Publication type: Book Chapter
Publication status: Published
Book Title: Engineering Methods and Tools for Software Safety and Security
Year: 2009
Volume: 22
Pages: 311-330
Series Title: NATO Science for Peace and Security Series - D: Information and Communication Security
Publisher: IOS Press
Place Published: Amsterdam
URL: http://dx.doi.org/10.3233/978-1-58603-976-9-311
DOI: 10.3233/978-1-58603-976-9-311
Notes: Online ISBN: 9781607504108
Library holdings: Search Newcastle University Library for this item
ISBN: 9781586039769
