Advertisement

Extending window inference

  • Joakim von Wright
Invited Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1479)

Abstract

Window inference is a proof paradigm where a theorem is proved by stepwise transformation, including transformations that change subterms while taking the context of these subterms into account. Originally developed for mathematical equivalence reasoning, window inference has proved powerful in other fields as well, and in particular for reasoning about refinement of programs. Although window inference is powerful and flexible, it has many limitations. The paper shows how some restrictions can be relaxed without compromising the elegance and simplicity of the window inference paradigm. We suggest a number of extensions, discuss their possible implementations and give examples of their use.

Keywords

Inference Rule Proof Obligation Data Refinement Predicate Transformer Program Refinement 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. J. Back. Refinement diagrams. In J.M. Morris and R.C.F. Shaw, editors, Proc. 4th Refinement Workshop, Workshops in Computer Science, pages 125–137, Cambridge, England, 9–11 January 1991. Springer-Verlag.Google Scholar
  2. 2.
    R. J. Back, J. Grundy, and J. von Wright. Structured calculational proof. Tech. Rpt. 65, Turku Centre for Computer Science, November 1996. to appear in Formal Aspects of Computing.Google Scholar
  3. 3.
    R. J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag, 1998.Google Scholar
  4. 4.
    H. Becht, A. Bloesch, R. Nickson and I. Hayes. Ergo 4.1 Reference Manual. Tech.Rpt. 96-31, Dept. Computer Science, Queensland University, November 1996.Google Scholar
  5. 5.
    M. J. Butler, J. Grundy, T. Långbacka, R. Ruksenas, and J. von Wright. The refinement calculator: Proof support for program refinement. In Proc. FMP'97 — Formal Methods Pacific, Discrete Mathematics and Theoretical Computer Science, Wellington, New Zealand, July 1997. Springer-Verlag.Google Scholar
  6. 6.
    M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, New York, 1993.Google Scholar
  7. 7.
    J. Grundy. A window inference tool for refinement. In Jones et al, editor, Proc. 5th Refinement Workshop, London, Jan. 1992. Springer-Verlag.Google Scholar
  8. 8.
    J. Grundy. A Method of Program Refinement. PhD thesis, University of Cambridge Computer Laboratory, Cambridge, England, 1993. Tech. Rpt. 318.Google Scholar
  9. 9.
    J. Grundy. Transformational Hierarchical Reasoning. The Computer Journal, 39(4):291–302, 1996.CrossRefGoogle Scholar
  10. 10.
    P. Heuberger. The minimal user-interface of a simple refinement tool. In Proc. 3rd Workshop on User Interfaces for Theorem Provers, INRIA Sophia-Antipolis, September 1997.Google Scholar
  11. 11.
    R. Nickson. Window inference for data refinement. In Proc. 5th Australasian Refinement Workshop, University of Queensland, 1996.Google Scholar
  12. 12.
    R. Nickson and I. Hayes. Supporting contexts in program refinement. Tech.Rpt. 96-29, Dept. Computer Science, Queensland University, 1996.Google Scholar
  13. 13.
    P. J. Robinson and J. Staples. Formalising a hierarchical structure of practical mathematical reasoning. Journal of Logic and Computation, 3(1):47–61, 1993.zbMATHMathSciNetGoogle Scholar
  14. 14.
    M. Staples. Window inference in Isabelle. In Proc. Isabelle Users Workshop, University of Cambridge Computer Laboratory, September 1995.Google Scholar
  15. 15.
    M. Utting. The Ergo 5 Generic Proof Engine. Tech.Rpt. 97-44, Dept. Computer Science, Queensland University, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Joakim von Wright
    • 1
  1. 1.åbo Akademi University and Turku Centre for Computer Science (TUCS)TurkuFinland

Personalised recommendations