A Window Inference Tool for Refinement

Reference

Jim Grundy. A Window Inference Tool for Refinement. In Jones, et.al. (eds). Proceedings of the 5th Refinement Workshop, Workshops in Computing. January 1992, London. Springer-Verlag, London. pages 230-254.

Abstract

This paper proposes a refinement tool based on a style of reasoning called window inference. Window inference allows a user to transform one expression into another while maintaining some specified relationship between them. A program refinement tool is described that combines window inference with an approach to refinement that treats programs as predicates.

BibTeX

Here is a suitable BibTeX entry:

  @INPROCEEDINGS{Grundy:1992:WIT,
    author      = "Jim Grundy",
    title       = "A Window Inference Tool for
                   Refinement",
    pages       = "230-254",
    editor      = "Clifford Bryn Jones and B. Tim Denvir
                   and Roger C. F. Shaw",
    booktitle   = "Proceedings of the 5th
                   Refinement Workshop",
    series      = "Workshops in Computing",
    address     = "Lloyd's Register, London",
    month       = jan,
    year        = 1992,
    organization= "BCS FACS",
    publisher   = "Springer-Verlag"}

Citations

If you liked this paper, then you might also like the following papers which cite it:

• David Carrington, Ian Hayes, Ray Nickson, Geoffrey Watson and Jim Welsh. A Program Refinement Tool. Formal Aspects of Computing. 10:97-124. 1998.
• Michael Butler and Thomas Långbacka. Program Derivation Using the Refinement Calculator. In von Wright, et.al. (eds). Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, Turku, Finalnd, August 1996. Springer-Verlag. pages 93-108.
• David Carrington, Ian Hayes, Ray Nickson, Geoffrey Watson and Jim Welsh. A Review of Existing Refinement Tools. Technical Report 94-8. Department of Computer Science, University of Queensland, QLD 4072, Australia. June 1994.
• Jim Grundy. Predicative Programming - A Survey. In D. Bjørner, et.al. (eds). Formal Methods in Programming and Their Applications: Proceedings of the International Conference, volume 735 of Lecture Notes in Computer Science. June 1993, Novosibirsk. Springer-Verlag, Berlin. pages 8-25.
• Jim Grundy. A Three-Valued Logic for Refinement. In D. Bjørner, et.al. (eds). Formal Methods in Programming and Their Applications: Proceedings of the International Conference, volume 735 of Lecture Notes in Computer Science. June 1993, Novosibirsk. Springer-Verlag, Berlin. pages 26-42.
• Jim Grundy. A Method of Program Refinement. PhD Thesis, Technical Report 318. University of Cambridge, Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England. November 1993.
• Mats Larsson. A Transformational Approach to Formal Digital System Design. Licentiate Thesis 378. Institutionen för Datavetenskap, Universitetet och Tekniska Högskolan i Linköping, S-581 83 Linköping, Sweden. May 1993.
• Thomas Låbacka, Rimvydas Ruksenas and Joakim con Wright. A Tool for Doing Window Inference in HOL. In P. J. Windley, et.al. (eds), Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, Aspen Grove, 11-14 September 1995. volume 971 of Lecture Notes in Computer Science, Springer-Verlag, Berlin.
• Ray Nickson and Ian Hayes. Program Window Inference. Technical Report 95-29. Department of Computer Science, University of Queensland, QLD 4072, Australia. July 1995.
• Peter J. Robinson and John Staples. Formalizing a Hierarchical Structure of Practical Mathematical Reasoning. Journal of Logic and Computation, 3(1):47-61, February 1993.
• Joakim von Wright, J. Hekanaho, P. Loustarinen and Thomas Långbaka. Mechanising Some Advanced Refinement Concepts. Formal Methods in System Design, 3(1/2), August 1993.
• Joakim von Wright. Program Refinement by Theorem Prover. In D. Till, et.al. (eds), Proceedings of the 6th Refinement Workshop, Workshops in Computing, City University, London, 5-7 January 1994. Springer-Verlag, London.

Where To Find it

If you are having trouble finding the proceedings in which this paper appears, then the following information may be of help:

Title:	Proceedings of the 5th Refinement Workshop
Editors:	Cliff B. Jones, Roger C. Shaw and Tim Denvir
Series:	Workshops in Computing
Copyright:	1992
Publisher:	Springer-Verlag With the British Computer Society London
LoC Call #:	QA76.76.D47 R44 1992
LoC Card #:	92-7438
Dewy Call #:	005.1 dc20
ISBN:	0-387-19752-4