© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Formal program development with approximations
Eerke A. Boiten and John Derrick
In Helen Treharne, Steve King, Martin Henson, and Steve Schneider, editors, ZB 2005, volume 3455 of Lecture Notes in Computer Science, pages 182-196. Springer, April 2005.Abstract
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.
Download publication 198 kbytes (PDF)Bibtex Record
@conference{2050,
author = {Eerke A. Boiten and John Derrick},
title = {Formal Program Development with Approximations},
month = {April},
year = {2005},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2005/2050},
publication_type = {conference},
submission_id = {14041_1110378069},
booktitle = {ZB 2005},
editor = {Helen Treharne and Steve King and Martin Henson and Steve Schneider},
volume = {3455},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
refereed = {yes},
ISBN = {3-540-25559-1},
}