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)
PDF
Language: English |
|
Download this file (PDF/203kB) |
![]() |
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: http://dx.doi.org/10.1007/11415787_22 |
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.
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 Nov 2021 09:52 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/14341 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):