Skip to main content
SpringerLink
Log in

A Tactic Driven Refinement Tool

  • Conference paper
5th Refinement Workshop

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

This paper describes a refinement tool we are developing, with special emphasis on the use of tactics. The operation of the tool is illustrated by stepping through the derivation of a selection sort algorithm. Several aspects of the tool and its implementation are then discussed in more detail, stressing the way in which the tool assists the user in deriving programs using the refinement calculus.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.-R. Abrial, S. T. Davies, M. K. O. Lee, D. S. Neilson, P. N. Scharbach and I. H. Sorensen, The B Method, BP Research, Sunbury Research Centre, U.K., 1991.

    Google Scholar 

  2. R. J. R. Back, “A Calculus of Refinements for Program Derivations”, Acta Informatica, 25: 593–624, 1988.

    Article  MathSciNet  MATH  Google Scholar 

  3. R. J. R. Back, “Refinement Diagrams”, Proceedings Fourth Refinement Workshop, Cambridge, 9–11 January, 1991, British Computer Society.

    Google Scholar 

  4. R. J. R. Back and J. von Wright, “Refinement Concepts Formalised in Higher Order Logic”, Formal Aspects of Computing, 2: 247–272, 1990.

    Article  MATH  Google Scholar 

  5. F. L. Bauer et al. (The CIP Language Group), The Munich Project CIP, Volume I: The Wide Spectrum Language CIP-L, Springer-Verlag, Lecture Notes in Computer Science 183, 1985.

    Google Scholar 

  6. F. L. Bauer et al. (The CIP System Group), The Munich Project CIP, Volume II: The Program Transformation System CIP-S, Springer-Verlag, Lecture Notes in Computer Science 292, 1987.

    Google Scholar 

  7. Mats Carlsson and Johan Widén, SICStus Prolog User’s Manual,Swedish Institute of Computer Science, 1988.

    Google Scholar 

  8. D. A. Carrington and K. A. Robinson, “Tool Support for the Refinement Calculus”, Computer Aided Verification Workshop, New Jersey, June 1990.

    Google Scholar 

  9. R. L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System,Prentice-Hall, 1986.

    Google Scholar 

  10. E. W. Dijkstra, “A Constructive Approach to the Problem of Program Correctness”, BIT, 8 (3): 181–185, 1969.

    MathSciNet  Google Scholar 

  11. E. W. Dijkstra, A Discipline of Programming, Academic Press, 1976.

    Google Scholar 

  12. Geoff Dromey, Program Derivation: The Development of Programs from Specifications,Addison-Wesley, 1989.

    Google Scholar 

  13. Mireille Ducassé and Anna-Maria Emde, “OPIUM: A Debugging Environment for Prolog Development and Debugging Research”, ACM Software Engineering Notes, 16 (2): 67–72, April 1991.

    Article  Google Scholar 

  14. R. W. Floyd, Towards Interactive Design of Correct Programs, Technical Report CS-235, Stanford University, September 1971.

    Google Scholar 

  15. David Gries, The Science of Programming,Springer-Verlag, 1981.

    Google Scholar 

  16. L. J. Groves and R. G. Nickson, Towards a Program Derivation Editor, Technical Report, Department of Computer Science, Victoria University of Wellington, 1988.

    Google Scholar 

  17. C. B. Jones, K.D. Jones, P.A. Lindsay and R. Moore, mural: A Formal Development Support System, Springer-Verlag, 1991.

    Google Scholar 

  18. Anne Kaldewaij, Programming: The Derivation of Algorithms,Prentice-Hall, 1990.

    Google Scholar 

  19. Ted Kim, XWIP Reference Manual, University of California, Los Angeles, 1989.

    Google Scholar 

  20. Carroll Morgan and Ken Robinson, “Specification Statements and Refinement”, IBM Journal of Research and Development, 31 (5): 546–555, September 1987.

    Article  MathSciNet  MATH  Google Scholar 

  21. Carroll Morgan, “Types and Invariants in the Refinement Calculus”, in Mathematics of Program Construction,J. L. A. van de Snepscheut (Ed.), Springer Verlag, Lecture Notes in Computer Science 375, 1989, pp 363–378.

    Google Scholar 

  22. Carroll Morgan, Programming from Specification,Prentice-Hall, 1990.

    Google Scholar 

  23. Carroll Morgan and Paul Gardiner, “Data Refinement by Calculation”, Acta Informatica, 27: 481–503, 1990.

    Article  MathSciNet  MATH  Google Scholar 

  24. Joseph M. Morris, “A Theoretical Basis for Stepwise Refinement and the Programming Calculus”, Science of Computer Programming, 9: 287–306, 1987.

    Article  MathSciNet  MATH  Google Scholar 

  25. M. Neilson, K. Havelund, K. R. Wagner and E. Saaman, “The RAISE Language, Method and Tools”, Formal Aspects of Computing, 1: 85–114, 1989.

    Article  Google Scholar 

  26. H. Partsch and R. Steinbrüggen, “Program Transformation Systems”, ACM Computing Surveys, 15: 199–236, 1983.

    Article  Google Scholar 

  27. L. C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge University Press, 1987.

    Google Scholar 

  28. Brian Ritchie and Paul Taylor, The Interactive Proof Editor: An Experiment in Interactive Theorem (sic), Technical Report LFCS-88–61, University of Edinburgh, July, 1988.

    Google Scholar 

  29. Robert W. Scheifler and Jim Gettys, “The X Win- dow System”, ACM Transactions on Graphics, 5 (2): 79–109, April 1986.

    Article  Google Scholar 

  30. T. Vickers, “An Overview of a Refinement Editor”, 5th Aus-tralian Software Engineering Conference,May 1990, Sydney, pp. 39–44.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Victoria University of Wellington, Wellington, New Zealand

    Lindsay Groves & Raymond Nickson

  2. University of New South Wales, Sydney, Australia

    Mark Utting

Authors
  1. Lindsay Groves
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Raymond Nickson
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mark Utting
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, The University, M13 9PL, Manchester, UK

    Cliff B. Jones DPhil

  2. Lloyd’s Register House, Lloyd’s Register of Shipping, 29 Wellesley Road, CR0 2AJ, Croydon, Surrey, UK

    Roger C. Shaw GIMA, MBCS

  3. Translimina Ltd, 37 Orpington Road, N21 3PD, Winchmore Hill, London, UK

    Tim Denvir MA, CEng, MIEE, MBCS

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag London

About this paper

Cite this paper

Groves, L., Nickson, R., Utting, M. (1992). A Tactic Driven Refinement Tool. In: Jones, C.B., Shaw, R.C., Denvir, T. (eds) 5th Refinement Workshop. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3550-0_14

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3550-0_14

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19752-2

  • Online ISBN: 978-1-4471-3550-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation