Window inference is a method for contextual rewriting and renement supported by the HOL Window Inference Library. This paper describes a userfriendly interface for window inference. The interface permits the user to select subexpressions by pointing and clicking and to select transformations from menus. The correctness of each transformation step is proved automatically by the HOL system. The interface can be tailored to particular userdened theories. One such extension for program renement is described.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Lammich, Peter; Tuerk, Thomas: Applying data refinement for monadic programs to Hopcroft’s algorithm (2012)
- Bortin, Maksym; Broch Johnsen, Einar; Lüth, Christoph: Structured formal development in Isabelle (2006)
- Johnsen, Einar Broch; Lüth, Christoph: Abstracting refinements for transformation (2003)
- Back, Ralph-Johan; Mikhajlova, Anna; von Wright, Joakim: Class refinement as semantics of correct object substitutability (2000)
- Lüth, C.; Wolff, B.: Functional design and implementation of graphical user interfaces for theorem provers (1999)
- Heuberger, Philipp: The minimal user interface of a simple refinement tool. (1998)
- Långbacka, Thomas; Rukšėnas, Rimvydas; von Wright, Joakim: TkWinHOL: a tool for window inference in HOL (1995)