School of Computing

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 375-393. 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 = {375--393},
keywords = {refinement, approximations, metric spaces},
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},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 12/03/2012 17:21