A provably correct functional programming approach to the prototyping of formal Z specifications

Abdallah, A. E. and Bowen, J. and Barros, A. and Barros, J. B. (2003) A provably correct functional programming approach to the prototyping of formal Z specifications. In: Computer Systems and Applications, 2003. Book of Abstracts. ACS/IEEE International Conference. IEEE Conference Publications, p. 73. ISBN 0-7803-7983-7

Full text not available from this repository. (Request a copy)

Abstract

Summary form only given. We describe a systematic way of constructing correct prototypes in a functional language such as Haskell from Z specifications. A formal relationship between Z specifications and functional prototypes is established. This relationship is based on model refinement in the sense of specification refinement in the model-oriented specification style. To reduce the number of proofs required in model refinement, we have defined a set of rules that allow us to derive a prototype from a specification. The use of such a set of rules implicitly guarantees the correctness of the derivation.

Item Type: Book Section
Uncontrolled Keywords: Formal specification, Functional programming, Prototyping, Refinement, Z notation.
Subjects: G400 Computer Science
Divisions: Faculty of Computing, Engineering and the Built Environment
Faculty of Computing, Engineering and the Built Environment > School of Computing and Digital Technology
Faculty of Computing, Engineering and the Built Environment > School of Computing and Digital Technology > Cyber Security
UoA Collections > UoA11: Computer Science and Informatics
Depositing User: Oana-Andreea Dumitrascu
Date Deposited: 07 Apr 2017 10:24
Last Modified: 07 Apr 2017 10:24
URI: http://www.open-access.bcu.ac.uk/id/eprint/4219

Actions (login required)

View Item View Item

Research

In this section...