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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
America, P., Rutten, J.: Solving reflexive domain equations in a category of complete metric spaces. In: de Bakker, J.W., Rutten, J.J.M. (eds.) Ten Years of Concurrency Semantics: Selected Papers of the Amsterdam Concurrency Group, pp. 131–163. World Scientific, Singapore (1992)
Banach, R., Poppleton, M.: Retrenchment, refinement and simulation. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, pp. 304–323. Springer, Heidelberg (2000)
Boiten, E.A.: Loose specification and refinement in Z. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 226–241. Springer, Heidelberg (2002)
de Bakker, J.W., Meyer, J.-J.C.: Metric semantics for concurrency. In: de Bakker, J.W., Rutten, J.J.M. (eds.) Ten Years of Concurrency Semantics: Selected Papers of the Amsterdam Concurrency Group, pp. 104–130. World Scientific, Singapore (1992)
de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. CUP, Cambridge (1998)
Derrick, J., Boiten, E.A.: Refinement in Z and Object-Z: Foundations and Advanced Applications. FACIT. Springer, Heidelberg (2001)
Derrick, J., Boiten, E.A.: Relational concurrent refinement. Formal Aspects of Computing 15(2), 182–214 (2003)
Ghosal, A., Jurdzinski, M., Majumdar, R., Prabhu, V.: Approximate refinement for hybrid systems. Berkeley EECS Research Summary for 2003, http://buffy.eecs.berkeley.edu/ResearchSummary/03abstracts/vinayak.1.html
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)
Jacobs, B.: Java’s integral types in PVS. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 1–15. Springer, Heidelberg (2003)
Kwiatkowska, M., Norman, G.: A fully abstract metric-space denotational semantics for reactive probabilistic processes. In: Edalat, A., Jung, A., Keimel, K., Kwiatkowska, M. (eds.). Electronic Notes in Theoretical Computer Science, vol. 13. Elsevier, Amsterdam (2000)
Neilson, D.S.: From Z to C: Illustration of a Rigorous Development Method. PhD thesis, Oxford University Computing Laboratory (1990)
Smith, G.: From ideal to realisable real-time specifications. In: Leslie, N. (ed.) Fifth New Zealand Formal Program Development Colloquium, number 99-1 in IIMS Technical Report. Institute of Information and Mathematical Sciences, Massey University at Albany (1999)
Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1992)
Stepney, S., Clark, J.A., Johnson, C.G., Partridge, D., Smith, R.E.: Artificial immune systems and the grand challenge for non-classical computation. In: Timmis, J., Bentley, P.J., Hart, E. (eds.) ICARIS 2003. LNCS, vol. 2787, pp. 204–216. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boiten, E.A., Derrick, J. (2005). Formal Program Development with Approximations. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds) ZB 2005: Formal Specification and Development in Z and B. ZB 2005. Lecture Notes in Computer Science, vol 3455. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11415787_22
Download citation
DOI: https://doi.org/10.1007/11415787_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25559-8
Online ISBN: 978-3-540-32007-4
eBook Packages: Computer ScienceComputer Science (R0)