Quelle  README.thy   Sprache: Isabelle

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