src/HOL/Isar_examples/HoareEx.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10838 9423817dee84
child 11701 3d51fbf81c17
permissions -rw-r--r--
improved theory reference in comment
     1 
     2 header {* Using Hoare Logic *}
     3 
     4 theory HoareEx = Hoare:
     5 
     6 subsection {* State spaces *}
     7 
     8 text {*
     9  First of all we provide a store of program variables that
    10  occur in any of the programs considered later.  Slightly unexpected
    11  things may happen when attempting to work with undeclared variables.
    12 *}
    13 
    14 record vars =
    15   I :: nat
    16   M :: nat
    17   N :: nat
    18   S :: nat
    19 
    20 text {*
    21  While all of our variables happen to have the same type, nothing
    22  would prevent us from working with many-sorted programs as well, or
    23  even polymorphic ones.  Also note that Isabelle/HOL's extensible
    24  record types even provides simple means to extend the state space
    25  later.
    26 *}
    27 
    28 
    29 subsection {* Basic examples *}
    30 
    31 text {*
    32  We look at few trivialities involving assignment and sequential
    33  composition, in order to get an idea of how to work with our
    34  formulation of Hoare Logic.
    35 *}
    36 
    37 text {*
    38  Using the basic \name{assign} rule directly is a bit cumbersome.
    39 *}
    40 
    41 lemma
    42   "|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = #10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
    43   by (rule assign)
    44 
    45 text {*
    46  Certainly we want the state modification already done, e.g.\ by
    47  simplification.  The \name{hoare} method performs the basic state
    48  update for us; we may apply the Simplifier afterwards to achieve
    49  ``obvious'' consequences as well.
    50 *}
    51 
    52 lemma "|- .{True}. \<acute>N := #10 .{\<acute>N = #10}."
    53   by hoare
    54 
    55 lemma "|- .{2 * \<acute>N = #10}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
    56   by hoare
    57 
    58 lemma "|- .{\<acute>N = #5}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
    59   by hoare simp
    60 
    61 lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
    62   by hoare
    63 
    64 lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
    65   by hoare simp
    66 
    67 lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
    68   by hoare
    69 
    70 lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
    71   by hoare simp
    72 
    73 lemma
    74 "|- .{\<acute>M = a & \<acute>N = b}.
    75     \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I
    76     .{\<acute>M = b & \<acute>N = a}."
    77   by hoare simp
    78 
    79 text {*
    80  It is important to note that statements like the following one can
    81  only be proven for each individual program variable.  Due to the
    82  extra-logical nature of record fields, we cannot formulate a theorem
    83  relating record selectors and updates schematically.
    84 *}
    85 
    86 lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."
    87   by hoare
    88 
    89 lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}."
    90   oops
    91 
    92 lemma
    93   "Valid {s. x s = a} (Basic (\<lambda>s. x_update (x s) s)) {s. x s = n}"
    94   -- {* same statement without concrete syntax *}
    95   oops
    96 
    97 
    98 text {*
    99  In the following assignments we make use of the consequence rule in
   100  order to achieve the intended precondition.  Certainly, the
   101  \name{hoare} method is able to handle this case, too.
   102 *}
   103 
   104 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
   105 proof -
   106   have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}."
   107     by auto
   108   also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
   109     by hoare
   110   finally show ?thesis .
   111 qed
   112 
   113 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
   114 proof -
   115   have "!!m n. m = n --> m + 1 ~= n"
   116       -- {* inclusion of assertions expressed in ``pure'' logic, *}
   117       -- {* without mentioning the state space *}
   118     by simp
   119   also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
   120     by hoare
   121   finally show ?thesis .
   122 qed
   123 
   124 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
   125   by hoare simp
   126 
   127 
   128 subsection {* Multiplication by addition *}
   129 
   130 text {*
   131  We now do some basic examples of actual \texttt{WHILE} programs.
   132  This one is a loop for calculating the product of two natural
   133  numbers, by iterated addition.  We first give detailed structured
   134  proof based on single-step Hoare rules.
   135 *}
   136 
   137 lemma
   138   "|- .{\<acute>M = 0 & \<acute>S = 0}.
   139       WHILE \<acute>M ~= a
   140       DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
   141       .{\<acute>S = a * b}."
   142 proof -
   143   let "|- _ ?while _" = ?thesis
   144   let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}."
   145 
   146   have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto
   147   also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}."
   148   proof
   149     let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1"
   150     have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}."
   151       by auto
   152     also have "|- ... ?c .{\<acute>?inv}." by hoare
   153     finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." .
   154   qed
   155   also have "... <= .{\<acute>S = a * b}." by auto
   156   finally show ?thesis .
   157 qed
   158 
   159 text {*
   160  The subsequent version of the proof applies the \name{hoare} method
   161  to reduce the Hoare statement to a purely logical problem that can be
   162  solved fully automatically.  Note that we have to specify the
   163  \texttt{WHILE} loop invariant in the original statement.
   164 *}
   165 
   166 lemma
   167   "|- .{\<acute>M = 0 & \<acute>S = 0}.
   168       WHILE \<acute>M ~= a
   169       INV .{\<acute>S = \<acute>M * b}.
   170       DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
   171       .{\<acute>S = a * b}."
   172   by hoare auto
   173 
   174 
   175 subsection {* Summing natural numbers *}
   176 
   177 text {*
   178  We verify an imperative program to sum natural numbers up to a given
   179  limit.  First some functional definition for proper specification of
   180  the problem.
   181 *}
   182 
   183 consts
   184   sum :: "(nat => nat) => nat => nat"
   185 primrec
   186   "sum f 0 = 0"
   187   "sum f (Suc n) = f n + sum f n"
   188 
   189 syntax
   190   "_sum" :: "idt => nat => nat => nat"
   191     ("SUM _<_. _" [0, 0, 10] 10)
   192 translations
   193   "SUM j<k. b" == "sum (\<lambda>j. b) k"
   194 
   195 text {*
   196  The following proof is quite explicit in the individual steps taken,
   197  with the \name{hoare} method only applied locally to take care of
   198  assignment and sequential composition.  Note that we express
   199  intermediate proof obligation in pure logic, without referring to the
   200  state space.
   201 *}
   202 
   203 theorem
   204   "|- .{True}.
   205       \<acute>S := 0; \<acute>I := 1;
   206       WHILE \<acute>I ~= n
   207       DO
   208         \<acute>S := \<acute>S + \<acute>I;
   209         \<acute>I := \<acute>I + 1
   210       OD
   211       .{\<acute>S = (SUM j<n. j)}."
   212   (is "|- _ (_; ?while) _")
   213 proof -
   214   let ?sum = "\<lambda>k. SUM j<k. j"
   215   let ?inv = "\<lambda>s i. s = ?sum i"
   216 
   217   have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
   218   proof -
   219     have "True --> 0 = ?sum 1"
   220       by simp
   221     also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
   222       by hoare
   223     finally show ?thesis .
   224   qed
   225   also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}."
   226   proof
   227     let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
   228     have "!!s i. ?inv s i & i ~= n -->  ?inv (s + i) (i + 1)"
   229       by simp
   230     also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}."
   231       by hoare
   232     finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." .
   233   qed
   234   also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n"
   235     by simp
   236   finally show ?thesis .
   237 qed
   238 
   239 text {*
   240  The next version uses the \name{hoare} method, while still explaining
   241  the resulting proof obligations in an abstract, structured manner.
   242 *}
   243 
   244 theorem
   245   "|- .{True}.
   246       \<acute>S := 0; \<acute>I := 1;
   247       WHILE \<acute>I ~= n
   248       INV .{\<acute>S = (SUM j<\<acute>I. j)}.
   249       DO
   250         \<acute>S := \<acute>S + \<acute>I;
   251         \<acute>I := \<acute>I + 1
   252       OD
   253       .{\<acute>S = (SUM j<n. j)}."
   254 proof -
   255   let ?sum = "\<lambda>k. SUM j<k. j"
   256   let ?inv = "\<lambda>s i. s = ?sum i"
   257 
   258   show ?thesis
   259   proof hoare
   260     show "?inv 0 1" by simp
   261   next
   262     fix s i assume "?inv s i & i ~= n"
   263     thus "?inv (s + i) (i + 1)" by simp
   264   next
   265     fix s i assume "?inv s i & ~ i ~= n"
   266     thus "s = ?sum n" by simp
   267   qed
   268 qed
   269 
   270 text {*
   271  Certainly, this proof may be done fully automatic as well, provided
   272  that the invariant is given beforehand.
   273 *}
   274 
   275 theorem
   276   "|- .{True}.
   277       \<acute>S := 0; \<acute>I := 1;
   278       WHILE \<acute>I ~= n
   279       INV .{\<acute>S = (SUM j<\<acute>I. j)}.
   280       DO
   281         \<acute>S := \<acute>S + \<acute>I;
   282         \<acute>I := \<acute>I + 1
   283       OD
   284       .{\<acute>S = (SUM j<n. j)}."
   285   by hoare auto
   286 
   287 end