Linking Object-Z with Spec#

Shengchao Qin, Guanhua He

Research output: Chapter in Book/Report/Conference proceedingConference contribution

122 Downloads (Pure)


Formal specifications have been a focus of software engineering research for many years and have been applied in a wide variety of settings. Their use in software engineering not only promotes high-level verification via theorem proving or model checking, but also inspires the “correct-by construction” approach to software development via formal refinement. Although this correct-by-construction method proves to work well for small software systems, it is still a utopia in the development of large and complex software systems. This paper moves one step forward in this direction by designing and implementing a sound linkage between the high level specification language Object-Z and the object-oriented specification language Spec#. Such a linkage would allow system requirements to be specified in a high-level formal language but validated and used in program language level. This linking process can be readily integrated with an automated program refinement procedure to achieve correctness-by-construction. In case no such procedures are applicable, the obtained contract based specification can guide programmers to manually generate program code, which can then be verified against the obtained specification using any available program verifiers.
Original languageEnglish
Title of host publicationProceedings of the IEEE international conference on engineering of complex computer systems, ICECCS
Publication statusPublished - 2007
Event12th IEEE International Conference on Engineering Complex Computer Systems - Auckland, New Zealand
Duration: 11 Jul 200714 Jul 2007


Conference12th IEEE International Conference on Engineering Complex Computer Systems
Abbreviated titleICECCS 2007
Country/TerritoryNew Zealand

Bibliographical note

Author can archive publisher's version/PDF.


Dive into the research topics of 'Linking Object-Z with Spec#'. Together they form a unique fingerprint.

Cite this