Reuse of verified design templates through extended pattern matching

  • David Hemer
  • Peter A. Lindsay
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


CARE provides a framework for construction and verification of programs, based around the recording of reusable design knowledge in parameterized templates. This paper shows how pattern-matching can be used to aid in the selection and application of design templates from a reusable library. A general framework is presented which is independent of the particular matching algorithm used at the level of mathematical expressions. A prototype has been built which supports a large subset of the Z mathematical language.


formal methods program development refinement software verification pattern matching 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    B. Fischer, F. Kievernagel, and W. Struckman. VCR: A VDM-based software component retrieval tool. Technical report,Technical University of Braunschwieg, Germany, November 1994.Google Scholar
  2. 2.
    K. Harwood. Towards tools for formal correctness. In The Fifth Australian Software Engineering Conference, pages 153–158. IREE Australia, May 1990.Google Scholar
  3. 3.
    D. Hemer and P.A. Lindsay. Formal specification of proof obligation generation in CARE. Technical Report 95-13, Software Verification Research Centre, The University of Queensland, 1995.Google Scholar
  4. 4.
    D. Hemer and P.A. Lindsay. The CARE toolset for developing verified programs from formal specifications. In O. Frieder and J. Wigglesworth, editors, Proceeding of the Fourth International Symposium on Assessment of Software Tools, pages 24–35. IEEE Computer Society Press, May 1996.Google Scholar
  5. 5.
    G.P. Huet. A unification algorithm for typed A-calculus. Theoretical Computer Science, 1:27–57, 1975.CrossRefGoogle Scholar
  6. 6.
    C. B. Jones, K. D. Jones, P. A. Lindsay, and R. Moore. mural: A Formal Development Support System. Springer-Verlag, 1991.Google Scholar
  7. 7.
    K. Lano. The B Language and Method: A Guide to Practical Formal Development. FACIT Series. Springer-Verlag, 1996.Google Scholar
  8. 8.
    P.A. Lindsay. The data logger case study in CARE. In Proc 5th Australasian Refinement Workshop (ARW'96), 1996. Scholar
  9. 9.
    P.A. Lindsay and D. Hemer. An industrial-strength method for the construction of formally verified software. In Proceedings of the 1996 Australian Software Engineering Conference, pages 27–36. IEEE Computer Society Press, July 1996.Google Scholar
  10. 10.
    D.E. Perry and S.S. Popovich. Inquire: Predicate-based use and reuse. In Proceedings of the 8th Knowledge-Based Software Engineering Conference, pages 144–151, September 1993.Google Scholar
  11. 11.
    M. Rittri. Using types as search keys in function libraries. In 0Proceedings of the Fourth International Conference on Functional Programming and Computer Architecture, pages 174–183. ACM Press, 1989.Google Scholar
  12. 12.
    E.J. Rollins and J.M. Wing. Specifications as search keys for software libraries. In Eighth International Conference on Logic Programming, pages 173–187. 1991.Google Scholar
  13. 13.
    C. Runciman and I. Toyn. Retrieving re-usable software components by polymorphic type. In Proceedings of the Fourth International Conference on Functional Programming and Computer Architecture, pages 166–173. ACM Press, 1989.Google Scholar
  14. 14.
    M. Stickel, R. Waldinger, M. Lowry, T. Pressburger, and I. Underwood. Deductive composition of astronomical software from subroutine libraries. In Proceedings 12th International Conference on Automated Deduction, pages 341–355, June 1994.Google Scholar
  15. 15.
    A. Moormann Zaremski and J.M. Wing. Specification matching of software components. In Third ACM SIGSOFT Symposium on the Foundations of Software Engineering, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • David Hemer
    • 1
  • Peter A. Lindsay
    • 1
  1. 1.Software Verification Research Centre School of Information TechnologyThe University of QueenslandBrisbaneAustralia

Personalised recommendations