Skip to main content
SpringerLink
Log in
Book cover

International Symposium of Formal Methods Europe

FME 1997: FME '97: Industrial Applications and Strengthened Foundations of Formal Methods pp 495–514Cite as

Reuse of verified design templates through extended pattern matching

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1313))

Abstract

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.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. K. Harwood. Towards tools for formal correctness. In The Fifth Australian Software Engineering Conference, pages 153–158. IREE Australia, May 1990.

    Google Scholar 

  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. 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. G.P. Huet. A unification algorithm for typed A-calculus. Theoretical Computer Science, 1:27–57, 1975.

    Article  Google Scholar 

  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. K. Lano. The B Language and Method: A Guide to Practical Formal Development. FACIT Series. Springer-Verlag, 1996.

    Google Scholar 

  8. P.A. Lindsay. The data logger case study in CARE. In Proc 5th Australasian Refinement Workshop (ARW'96), 1996. http://www.it.uq.edu.au/conferences/arw96/.

    Google Scholar 

  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. 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. 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. 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. 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. 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. 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 

Download references

Author information

Authors and Affiliations

  1. Software Verification Research Centre School of Information Technology, The University of Queensland, 4072, Brisbane, Australia

    David Hemer & Peter A. Lindsay

Authors
  1. David Hemer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter A. Lindsay
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

John Fitzgerald Cliff B. Jones Peter Lucas

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hemer, D., Lindsay, P.A. (1997). Reuse of verified design templates through extended pattern matching. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds) FME '97: Industrial Applications and Strengthened Foundations of Formal Methods. FME 1997. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63533-5_26

Download citation

  • DOI: https://doi.org/10.1007/3-540-63533-5_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63533-8

  • Online ISBN: 978-3-540-69593-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation