Quelle  README.thy

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›
  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