Skip to main content

Formal Program Development with Approximations

Boiten, Eerke Albert and Derrick, John (2005) Formal Program Development with Approximations. In: Treharne, Helen and King, Steve and Henson, Martin C. and Schneider, Steve A., eds. ZB 2005: Formal Specification and Development in Z and B 4th International Conference of B and Z Users. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 374-392. ISBN 978-3-540-25559-8. E-ISBN 978-3-540-32007-4. (doi:10.1007/11415787_22) (KAR id:14341)

Language: English
Download (272kB) Preview
[thumbnail of FormalProgram.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL


We describe a method for combining formal program development with a disciplined and documented way of introducing realistic compromises, for example necessitated by resource bounds. Idealistic specifications are identified with the limits of sequences of more ''realistic'' specifications, and such sequences can then be refined in their entirety. Compromises amount to focusing the attention on a particular element of the sequence instead of the sequence as a whole. This method addresses the problem that initial formal specifications can be abstract or complete but rarely both. Various potential application areas are sketched, some illustrated with examples. Key research issues are found in identifying metric spaces and properties that make them usable for refinement using approximations.

Item Type: Book section
DOI/Identification number: 10.1007/11415787_22
Uncontrolled keywords: refinement, approximations, metric spaces
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Eerke Boiten
Date Deposited: 24 Nov 2008 18:03 UTC
Last Modified: 16 Feb 2021 12:25 UTC
Resource URI: (The current URI for this page, for reference purposes)
Boiten, Eerke Albert:
  • Depositors only (login required):


Downloads per month over past year