Formal Program Development with Approximations

  • Eerke A. Boiten
  • John Derrick
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)


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.


Refinement approximations metric spaces 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)Google Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. CUP, Cambridge (1998)Google Scholar
  6. 6.
    Derrick, J., Boiten, E.A.: Refinement in Z and Object-Z: Foundations and Advanced Applications. FACIT. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  7. 7.
    Derrick, J., Boiten, E.A.: Relational concurrent refinement. Formal Aspects of Computing 15(2), 182–214 (2003)zbMATHCrossRefGoogle Scholar
  8. 8.
    Ghosal, A., Jurdzinski, M., Majumdar, R., Prabhu, V.: Approximate refinement for hybrid systems. Berkeley EECS Research Summary for 2003,
  9. 9.
    Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Neilson, D.S.: From Z to C: Illustration of a Rigorous Development Method. PhD thesis, Oxford University Computing Laboratory (1990)Google Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1992)Google Scholar
  15. 15.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Eerke A. Boiten
    • 1
  • John Derrick
    • 2
  1. 1.Computing LaboratoryUniversity of Kent at Canterbury 
  2. 2.Department of Computer ScienceUniversity of Sheffield 

Personalised recommendations