Theory README

theory README imports Main
begin

section ‹Hoare Logic for a Simple WHILE Language›

subsection ‹Language and logic›

text ‹
  This directory contains an implementation of Hoare logic for a simple WHILE
  language. The constructs are

    ▪ ▩‹SKIP›
    ▪ ▩‹_ := _›
    ▪ ▩‹_ ; _›
    ▪ ▩‹IF _ THEN _ ELSE _ FI›
    ▪ ▩‹WHILE _ INV {_} DO _ OD›

  Note that each WHILE-loop must be annotated with an invariant.

  Within the context of theory ▩‹Hoare›, you can state goals of the form
    @{verbatim [display] ‹VARS x y ... {P} prog {Q}›}
  where ▩‹prog› is a program in the above language, ▩‹P› is the precondition,
  ▩‹Q› the postcondition, and ▩‹x y ...› is the list of all ∗‹program
  variables› in ▩‹prog›. The latter list must be nonempty and it must include
  all variables that occur on the left-hand side of an assignment in ▩‹prog›.
  Example:
    @{verbatim [display] ‹VARS x {x = a} x := x+1 {x = a+1}›}
  The (normal) variable ▩‹a› is merely used to record the initial value of
  ▩‹x› and is not a program variable. Pre/post conditions can be arbitrary HOL
  formulae mentioning both program variables and normal variables.

  The implementation hides reasoning in Hoare logic completely and provides a
  method ▩‹vcg› for transforming a goal in Hoare logic into an equivalent list
  of verification conditions in HOL: ⬚‹apply vcg›

  If you want to simplify the resulting verification conditions at the same
  time: ⬚‹apply vcg_simp› which, given the example goal above, solves it
  completely. For further examples see 🗏‹Examples.thy›.

  ❙‹IMPORTANT:›
  This is a logic of partial correctness. You can only prove that your program
  does the right thing ∗‹if› it terminates, but not ∗‹that› it terminates. A
  logic of total correctness is also provided and described below.
›


subsection ‹Total correctness›

text ‹
  To prove termination, each WHILE-loop must be annotated with a variant:

    ▪ ▩‹WHILE _ INV {_} VAR {_} DO _ OD›

  A variant is an expression with type ▩‹nat›, which may use program variables
  and normal variables.

  A total-correctness goal has the form ▩‹VARS x y ... [P] prog [Q]› enclosing
  the pre- and postcondition in square brackets.

  Methods ▩‹vcg_tc› and ▩‹vcg_tc_simp› can be used to derive verification
  conditions.

  From a total-correctness proof, a function can be extracted which for every
  input satisfying the precondition returns an output satisfying the
  postcondition.
›


subsection ‹Notes on the implementation›

text ‹
  The implementation loosely follows

  Mike Gordon. ∗‹Mechanizing Programming Logics in Higher Order Logic›.
  University of Cambridge, Computer Laboratory, TR 145, 1988.

  published as

  Mike Gordon. ∗‹Mechanizing Programming Logics in Higher Order Logic›. In
  ∗‹Current Trends in Hardware Verification and Automated Theorem Proving›,
  edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989.

  The main differences: the state is modelled as a tuple as suggested in

  J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka.
  ∗‹Mechanizing Some Advanced Refinement Concepts›. Formal Methods in System
  Design, 3, 1993, 49-81.

  and the embeding is deep, i.e. there is a concrete datatype of programs. The
  latter is not really necessary.
›

end