src/HOL/Hoare/README.thy
author wenzelm
Mon, 11 Sep 2023 19:30:48 +0200
changeset 78659 b5f3d1051b13
parent 75916 b6589c8ccadd
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
75916
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
     1
theory README imports Main
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
     2
begin
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
     3
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
     4
section \<open>Hoare Logic for a Simple WHILE Language\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
     5
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
     6
subsection \<open>Language and logic\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
     7
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
     8
text \<open>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
     9
  This directory contains an implementation of Hoare logic for a simple WHILE
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    10
  language. The constructs are
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    11
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    12
    \<^item> \<^verbatim>\<open>SKIP\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    13
    \<^item> \<^verbatim>\<open>_ := _\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    14
    \<^item> \<^verbatim>\<open>_ ; _\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    15
    \<^item> \<^verbatim>\<open>IF _ THEN _ ELSE _ FI\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    16
    \<^item> \<^verbatim>\<open>WHILE _ INV {_} DO _ OD\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    17
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    18
  Note that each WHILE-loop must be annotated with an invariant.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    19
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    20
  Within the context of theory \<^verbatim>\<open>Hoare\<close>, you can state goals of the form
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    21
    @{verbatim [display] \<open>VARS x y ... {P} prog {Q}\<close>}
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    22
  where \<^verbatim>\<open>prog\<close> is a program in the above language, \<^verbatim>\<open>P\<close> is the precondition,
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    23
  \<^verbatim>\<open>Q\<close> the postcondition, and \<^verbatim>\<open>x y ...\<close> is the list of all \<^emph>\<open>program
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    24
  variables\<close> in \<^verbatim>\<open>prog\<close>. The latter list must be nonempty and it must include
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    25
  all variables that occur on the left-hand side of an assignment in \<^verbatim>\<open>prog\<close>.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    26
  Example:
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    27
    @{verbatim [display] \<open>VARS x {x = a} x := x+1 {x = a+1}\<close>}
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    28
  The (normal) variable \<^verbatim>\<open>a\<close> is merely used to record the initial value of
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    29
  \<^verbatim>\<open>x\<close> and is not a program variable. Pre/post conditions can be arbitrary HOL
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    30
  formulae mentioning both program variables and normal variables.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    31
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    32
  The implementation hides reasoning in Hoare logic completely and provides a
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    33
  method \<^verbatim>\<open>vcg\<close> for transforming a goal in Hoare logic into an equivalent list
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    34
  of verification conditions in HOL: \<^theory_text>\<open>apply vcg\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    35
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    36
  If you want to simplify the resulting verification conditions at the same
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    37
  time: \<^theory_text>\<open>apply vcg_simp\<close> which, given the example goal above, solves it
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    38
  completely. For further examples see \<^file>\<open>Examples.thy\<close>.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    39
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    40
  \<^bold>\<open>IMPORTANT:\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    41
  This is a logic of partial correctness. You can only prove that your program
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    42
  does the right thing \<^emph>\<open>if\<close> it terminates, but not \<^emph>\<open>that\<close> it terminates. A
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    43
  logic of total correctness is also provided and described below.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    44
\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    45
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    46
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    47
subsection \<open>Total correctness\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    48
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    49
text \<open>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    50
  To prove termination, each WHILE-loop must be annotated with a variant:
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    51
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    52
    \<^item> \<^verbatim>\<open>WHILE _ INV {_} VAR {_} DO _ OD\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    53
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    54
  A variant is an expression with type \<^verbatim>\<open>nat\<close>, which may use program variables
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    55
  and normal variables.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    56
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    57
  A total-correctness goal has the form \<^verbatim>\<open>VARS x y ... [P] prog [Q]\<close> enclosing
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    58
  the pre- and postcondition in square brackets.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    59
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    60
  Methods \<^verbatim>\<open>vcg_tc\<close> and \<^verbatim>\<open>vcg_tc_simp\<close> can be used to derive verification
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    61
  conditions.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    62
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    63
  From a total-correctness proof, a function can be extracted which for every
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    64
  input satisfying the precondition returns an output satisfying the
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    65
  postcondition.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    66
\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    67
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    68
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    69
subsection \<open>Notes on the implementation\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    70
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    71
text \<open>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    72
  The implementation loosely follows
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    73
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    74
  Mike Gordon. \<^emph>\<open>Mechanizing Programming Logics in Higher Order Logic\<close>.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    75
  University of Cambridge, Computer Laboratory, TR 145, 1988.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    76
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    77
  published as
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    78
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    79
  Mike Gordon. \<^emph>\<open>Mechanizing Programming Logics in Higher Order Logic\<close>. In
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    80
  \<^emph>\<open>Current Trends in Hardware Verification and Automated Theorem Proving\<close>,
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    81
  edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    82
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    83
  The main differences: the state is modelled as a tuple as suggested in
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    84
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    85
  J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    86
  \<^emph>\<open>Mechanizing Some Advanced Refinement Concepts\<close>. Formal Methods in System
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    87
  Design, 3, 1993, 49-81.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    88
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    89
  and the embeding is deep, i.e. there is a concrete datatype of programs. The
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    90
  latter is not really necessary.
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    91
\<close>
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    92
b6589c8ccadd discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff changeset
    93
end