(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer
*)

section ‹Examples using the Verification Environment›

theory VcgEx imports "../HeapList" "../Vcg" begin

text ‹Some examples, especially the single-step Isar proofs are taken from
 texttt{HOL/Isar\_examples/HoareEx.thy}.
 ›

subsection ‹State Spaces›

text ‹
 First of all we provide a store of program variables that
 occur in the programs considered later. Slightly unexpected
 things may happen when attempting to work with undeclared variables.
 ›

record 'g vars = "'g state" +
  A_' :: nat
  I_' :: nat
  M_' :: nat
  N_' :: nat
  R_' :: nat
  S_' :: nat
  B_' :: bool
  Arr_' :: "nat list"
  Abr_':: string



text ‹We decorate the state components in the record with the suffix ‹_'›,
  avoid cluttering the namespace with the simple names that could no longer
  used for logical variables otherwise.
 ›

text ‹We will first consider programs without procedures, later on
  will regard procedures without global variables and finally we
  get the full pictures: mutually recursive procedures with global
  (including heap).
 ›

subsection ‹Basic Examples›

text ‹
 We look at few trivialities involving assignment and sequential
 composition, in order to get an idea of how to work with our
 formulation of Hoare Logic.
 ›

text ‹
 Using the basic rule directly is a bit cumbersome.
 ›

lemma "Γ⊨ {|🚫N = 5|} 🚫N :== 2 * 🚫N {|🚫N = 10|}"
  apply (rule HoarePartial.Basic)  apply simp
  done

text ‹
 If we refer to components (variables) of the state-space of the program
 we always mark these with ‹🚫›. It is the acute-symbol and is present on
 most keyboards. So all program variables are marked with the acute and all
 logical variables are not.
 The assertions of the Hoare tuple are
 ordinary Isabelle sets. As we usually want to refer to the state space
 in the assertions, we provide special brackets for them. They can be written
 as {\verb+{| |}+} in ASCII or ‹{ }› with symbols. Internally
 marking variables has two effects. First of all we refer to the implicit
 state and secondary we get rid of the suffix ‹_'›.
 So the assertion @{term "{|🚫N = 5|}"} internally gets expanded to
 ‹{s. N_' s = 5}› written in ordinary set comprehension notation of
 Isabelle. It describes the set of states where the ‹N_'› component
 is equal to ‹5›.
 ›


text ‹
 Certainly we want the state modification already done, e.g.\ by
 simplification. The ‹vcg› method performs the basic state
 update for us; we may apply the Simplifier afterwards to achieve
 ``obvious'' consequences as well.
 ›


lemma "Γ⊨ {True} 🚫N :== 10 {🚫N = 10}"
  by vcg

lemma "Γ⊨ {2 * 🚫N = 10} 🚫N :== 2 * 🚫N {🚫N = 10}"
  by vcg

lemma "Γ⊨ {🚫N = 5} 🚫N :== 2 * 🚫N {🚫N = 10}"
  apply vcg
  apply simp
  done

lemma "Γ⊨ {🚫N + 1 = a + 1} 🚫N :== 🚫N + 1 {🚫N = a + 1}"
  by vcg

lemma "Γ⊨ {🚫N = a} 🚫N :== 🚫N + 1 {🚫N = a + 1}"
  by vcg


lemma "Γ⊨ {a = a ∧ b = b} 🚫M :== a;; 🚫N :== b {🚫M = a ∧ 🚫N = b}"
  by vcg


lemma "\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>M :== a;; \<acute>N :== b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
  by vcg

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
                \<acute>I :== \<acute>M;; \<acute>M :== \<acute>N;; \<acute>N :== \<acute>I
              \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
  by vcg

text \<open>
We can also perform verification conditions generation step by step by using
the \<open>vcg_step\<close> method.
\<close>

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
               \<acute>I :== \<acute>M;; \<acute>M :== \<acute>N;; \<acute>N :== \<acute>I
              \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
  apply vcg_step
  apply vcg_step
  apply vcg_step
  apply vcg_step
  done

text \<open>
 It is important to note that statements like the following one can
 only be proven for each individual program variable.  Due to the
 extra-logical nature of record fields, we cannot formulate a theorem
 relating record selectors and updates schematically.
\<close>

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N :== \<acute>N \<lbrace>\<acute>N = a\<rbrace>"
  by vcg


(*
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>x = a\<rbrace> \<acute>x :== \<acute>x \<lbrace>\<acute>x = a\<rbrace>"
  apply (rule HoarePartial.Basic)
  -- {* We can't proof this since we don't know what @{text "x_'_update"} is. *}
  oops
 *)
lemma "\<Gamma>\<turnstile>{s. x_' s = a} (Basic (\<lambda>s. x_'_update (x_' s) s)) {s. x_' s = a}"
  oops


text \<open>
 In the following assignments we make use of the consequence rule in
 order to achieve the intended precondition.  Certainly, the
 \<open>vcg\<close> method is able to handle this case, too.
\<close>

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
proof -
  have "\<lbrace>\<acute>M = \<acute>N\<rbrace> \<subseteq> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace>"
    by auto
  also have "\<Gamma>\<turnstile> \<dots> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
    by vcg
  finally show ?thesis .
qed

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
proof -
  have "\<And>m n::nat. m = n \<longrightarrow> m + 1 \<noteq> n"
      \<comment> \<open>inclusion of assertions expressed in ``pure'' logic,\<close>
      \<comment> \<open>without mentioning the state space\<close>
    by simp
  also have "\<Gamma>\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
    by vcg
  finally show ?thesis .
qed

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
  apply vcg
  apply simp
  done

subsection \<open>Multiplication by Addition\<close>

text \<open>
 We now do some basic examples of actual \texttt{WHILE} programs.
 This one is a loop for calculating the product of two natural
 numbers, by iterated addition.  We first give detailed structured
 proof based on single-step Hoare rules.
\<close>

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
      WHILE \<acute>M \<noteq> a
      DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD
      \<lbrace>\<acute>S = a * b\<rbrace>"
proof -
  let "\<Gamma>\<turnstile> _ ?while _" = ?thesis
  let "\<lbrace>\<acute>?inv\<rbrace>" = "\<lbrace>\<acute>S = \<acute>M * b\<rbrace>"

  have "\<lbrace>\<acute>M = 0 & \<acute>S = 0\<rbrace> \<subseteq> \<lbrace>\<acute>?inv\<rbrace>" by auto
  also have "\<Gamma>\<turnstile> \<dots> ?while \<lbrace>\<acute>?inv \<and> \<not> (\<acute>M \<noteq> a)\<rbrace>"
  proof
    let ?c = "\<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1"
    have "\<lbrace>\<acute>?inv \<and> \<acute>M \<noteq> a\<rbrace> \<subseteq> \<lbrace>\<acute>S + b = (\<acute>M + 1) * b\<rbrace>"
      by auto
    also have "\<Gamma>\<turnstile> \<dots> ?c \<lbrace>\<acute>?inv\<rbrace>" by vcg
    finally show "\<Gamma>\<turnstile> \<lbrace>\<acute>?inv \<and> \<acute>M \<noteq> a\<rbrace> ?c \<lbrace>\<acute>?inv\<rbrace>" .
  qed
  also have "\<lbrace>\<acute>?inv \<and> \<not> (\<acute>M \<noteq> a)\<rbrace> \<subseteq> \<lbrace>\<acute>S = a * b\<rbrace>" by auto
  finally show ?thesis by blast
qed


text \<open>
 The subsequent version of the proof applies the \<open>vcg\<close> method
 to reduce the Hoare statement to a purely logical problem that can be
 solved fully automatically.  Note that we have to specify the
 \texttt{WHILE} loop invariant in the original statement.
\<close>

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          WHILE \<acute>M \<noteq> a
          INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
          DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD
          \<lbrace>\<acute>S = a * b\<rbrace>"
  apply vcg
  apply auto
  done

text \<open>Here some examples of ``breaking'' out of a loop\<close>

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          TRY
            WHILE True
            INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
            DO IF \<acute>M = a THEN THROW ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 FI OD
          CATCH
            SKIP
          END
          \<lbrace>\<acute>S = a * b\<rbrace>"
apply vcg
apply auto
done

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          TRY
            WHILE True
            INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
            DO IF \<acute>M = a THEN \<acute>Abr :== ''Break'';;THROW
               ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1
               FI
            OD
          CATCH
            IF \<acute>Abr = ''Break'' THEN SKIP ELSE Throw FI
          END
          \<lbrace>\<acute>S = a * b\<rbrace>"
apply vcg
apply auto
done


text \<open>Some more syntactic sugar, the label statement \<open>\<dots> \<bullet> \<dots>\<close> as shorthand
for the \<open>TRY-CATCH\<close> above, and the \<open>RAISE\<close> for an state-update followed
by a \<open>THROW\<close>.
\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          \<lbrace>\<acute>Abr = ''Break''\<rbrace>\<bullet> WHILE True INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
           DO IF \<acute>M = a THEN RAISE \<acute>Abr :== ''Break''
              ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1
              FI
           OD
          \<lbrace>\<acute>S = a * b\<rbrace>"
apply vcg
apply auto
done

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          TRY
            WHILE True
            INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
            DO IF \<acute>M = a THEN RAISE \<acute>Abr :== ''Break''
               ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1
               FI
            OD
          CATCH
            IF \<acute>Abr = ''Break'' THEN SKIP ELSE Throw FI
          END
          \<lbrace>\<acute>S = a * b\<rbrace>"
apply vcg
apply auto
done

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          \<lbrace>\<acute>Abr = ''Break''\<rbrace> \<bullet> WHILE True
          INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
          DO IF \<acute>M = a THEN RAISE \<acute>Abr :== ''Break''
               ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1
               FI
          OD
          \<lbrace>\<acute>S = a * b\<rbrace>"
apply vcg
apply auto
done

text \<open>Blocks\<close>

lemma  "\<Gamma>\<turnstile>\<lbrace>\<acute>I = i\<rbrace> LOC \<acute>I;; \<acute>I :== 2  COL \<lbrace>\<acute>I \<le> i\<rbrace>"
  apply vcg
  by simp
lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = n\<rbrace> LOC \<acute>N :== 10;; \<acute>N :== \<acute>N + 2 COL \<lbrace>\<acute>N = n\<rbrace>"
  by vcg

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = n\<rbrace> LOC \<acute>N :== 10, \<acute>M;; \<acute>N :== \<acute>N + 2 COL \<lbrace>\<acute>N = n\<rbrace>"
  by vcg


subsection \<open>Summing Natural Numbers\<close>

text \<open>
 We verify an imperative program to sum natural numbers up to a given
 limit.  First some functional definition for proper specification of
 the problem.
\<close>

primrec
  sum :: "(nat => nat) => nat => nat"
where
  "sum f 0 = 0"
| "sum f (Suc n) = f n + sum f n"

syntax
  "_sum" :: "idt => nat => nat => nat"
    (\<open>SUMM _<_. _\<close> [0, 0, 10] 10)
syntax_consts
  "_sum" == sum
translations
  "SUMM j<k. b" == "CONST sum (\<lambda>j. b) k"

text \<open>
 The following proof is quite explicit in the individual steps taken,
 with the \<open>vcg\<close> method only applied locally to take care of
 assignment and sequential composition.  Note that we express
 intermediate proof obligation in pure logic, without referring to the
 state space.
\<close>

theorem "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
           \<acute>S :== 0;; \<acute>I :== 1;;
           WHILE \<acute>I \<noteq> n
           DO
             \<acute>S :== \<acute>S + \<acute>I;;
             \<acute>I :== \<acute>I + 1
           OD
           \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>"
  (is "\<Gamma>\<turnstile> _ (_;; ?while) _")
proof -
  let ?sum = "\<lambda>k. SUMM j<k. j"
  let ?inv = "\<lambda>s i. s = ?sum i"

  have "\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
  proof -
    have "True \<longrightarrow> 0 = ?sum 1"
      by simp
    also have "\<Gamma>\<turnstile> \<lbrace>\<dots>\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
      by vcg
    finally show ?thesis .
  qed
  also have "\<Gamma>\<turnstile> \<lbrace>?inv \<acute>S \<acute>I\<rbrace> ?while \<lbrace>?inv \<acute>S \<acute>I \<and> \<not> \<acute>I \<noteq> n\<rbrace>"
  proof
    let ?body = "\<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1"
    have "\<And>s i. ?inv s i \<and> i \<noteq> n \<longrightarrow>  ?inv (s + i) (i + 1)"
      by simp
    also have "\<Gamma>\<turnstile> \<lbrace>\<acute>S + \<acute>I = ?sum (\<acute>I + 1)\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
      by vcg
    finally show "\<Gamma>\<turnstile> \<lbrace>?inv \<acute>S \<acute>I \<and> \<acute>I \<noteq> n\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>" .
  qed
  also have "\<And>s i. s = ?sum i \<and> \<not> i \<noteq> n \<longrightarrow> s = ?sum n"
    by simp
  finally show ?thesis .
qed

text \<open>
 The next version uses the \<open>vcg\<close> method, while still explaining
 the resulting proof obligations in an abstract, structured manner.
\<close>

theorem "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
           \<acute>S :== 0;; \<acute>I :== 1;;
           WHILE \<acute>I \<noteq> n
           INV \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
           DO
             \<acute>S :== \<acute>S + \<acute>I;;
             \<acute>I :== \<acute>I + 1
           OD
          \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>"
proof -
  let ?sum = "\<lambda>k. SUMM j<k. j"
  let ?inv = "\<lambda>s i. s = ?sum i"

  show ?thesis
  proof vcg
    show "?inv 0 1" by simp
  next
    fix i s assume "?inv s i" "i \<noteq> n"
    thus "?inv (s + i) (i + 1)" by simp
  next
    fix i s assume x: "?inv s i" "\<not> i \<noteq> n"
    thus "s = ?sum n" by simp
  qed
qed

text \<open>
 Certainly, this proof may be done fully automatically as well, provided
 that the invariant is given beforehand.
\<close>

theorem "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
           \<acute>S :== 0;; \<acute>I :== 1;;
           WHILE \<acute>I \<noteq> n
           INV \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
           DO
             \<acute>S :== \<acute>S + \<acute>I;;
             \<acute>I :== \<acute>I + 1
           OD
           \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>"
  apply vcg
  apply auto
  done

subsection \<open>SWITCH\<close>

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> SWITCH \<acute>B
                        {True} \<Rightarrow> \<acute>N :== 6
                      | {False} \<Rightarrow> \<acute>N :== 7
                     END
          \<lbrace>\<acute>N > 5\<rbrace>"
apply vcg
apply simp
done

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> SWITCH \<acute>N
                        {v. v < 5} \<Rightarrow> \<acute>N :== 6
                      | {v. v \<ge> 5} \<Rightarrow> \<acute>N :== 7
                     END
          \<lbrace>\<acute>N > 5\<rbrace>"
apply vcg
apply simp
done

subsection \<open>(Mutually) Recursive Procedures\<close>

subsubsection \<open>Factorial\<close>

text \<open>We want to define a procedure for the factorial. We first
define a HOL functions that calculates it to specify the procedure later on.
\<close>

primrec fac:: "nat \<Rightarrow> nat"
where
"fac 0 = 1" |
"fac (Suc n) = (Suc n) * fac n"

lemma fac_simp [simp]: "0 < i \<Longrightarrow>  fac i = i * fac (i - 1)"
  by (cases i) simp_all

text \<open>Now we define the procedure\<close>

procedures
  Fac (N|R) = "IF \<acute>N = 0 THEN \<acute>R :== 1
                       ELSE \<acute>R :== CALL Fac(\<acute>N - 1);;
                            \<acute>R :== \<acute>N * \<acute>R
                       FI"



text \<open>A procedure is given by the signature of the procedure
followed by the procedure body.
The signature consists of the name of the procedure and a list of
parameters. The parameters in front of the pipe \<open>|\<close> are value parameters
and behind the pipe are the result parameters. Value parameters model call by value
semantics. The value of a result parameter at the end of the procedure is passed back
to the caller.
\<close>



text \<open>
Behind the scenes the \<open>procedures\<close> command provides us convenient syntax
for procedure calls, defines a constant for the procedure body
(named @{term "Fac_body"}) and creates some locales. The purpose of locales
is to set up logical contexts to support modular reasoning.
A locale is named \<open>Fac_impl\<close> and extends the \<open>hoare\<close> locale
with a theorem @{term "\<Gamma> ''Fac'' = Fac_body"} that simply states how the
procedure is defined in the procedure context. Check out the locales.
The purpose of the locales is to give us easy means to setup the context
in which we will prove programs correct.
In these locales the procedure context @{term "\<Gamma>"} is fixed.
So always use this letter in procedure
specifications. This is crucial, if we later on prove some tuples under the
assumption of some procedure specifications.
\<close>

thm Fac_body.Fac_body_def
print_locale Fac_impl

text \<open>
To see how a call is syntactically translated you can switch off the
printing translation via the configuration option \<open>hoare_use_call_tr'\<close>
\<close>

context Fac_impl
begin
text \<open>
@{term "CALL Fac(\<acute>N,\<acute>M)"} is internally:
\<close>
declare [[hoare_use_call_tr' = false]]
text \<open>
@{term "CALL Fac(\<acute>N,\<acute>M)"}
\<close>
term "CALL Fac(\<acute>N,\<acute>M)"
declare [[hoare_use_call_tr' = true]]
end

text \<open>
Now let us prove that @{term "Fac"} meets its specification.
\<close>

text \<open>
Procedure specifications are ordinary Hoare tuples. We use the parameterless
call for the specification; \<open>\<acute>R :== PROC Fac(\<acute>N)\<close> is syntactic sugar
for \<open>Call ''Fac''\<close>. This emphasises that the specification
describes the internal behaviour of the procedure, whereas parameter passing
corresponds to the procedure call.
\<close>


lemma (in Fac_impl)
  shows "\<forall>n. \<Gamma>,\<Theta>\<turnstile>\<lbrace>\<acute>N=n\<rbrace>  PROC Fac(\<acute>N,\<acute>R) \<lbrace>\<acute>R = fac n\<rbrace>"
  apply (hoare_rule HoarePartial.ProcRec1)
  apply vcg
  apply simp
  done


text \<open>
Since the factorial was implemented recursively,
the main ingredient of this proof is, to assume that the specification holds for
the recursive call of @{term Fac} and prove the body correct.
The assumption for recursive calls is added to the context by
the rule @{thm [source] HoarePartial.ProcRec1}
(also derived from general rule for mutually recursive procedures):
@{thm [display] HoarePartial.ProcRec1 [no_vars]}
The verification condition generator will infer the specification out of the
context when it encounters a recursive call of the factorial.
\<close>

text \<open>We can also step through verification condition generation. When
the verification condition generator encounters a procedure call it tries to
use the rule \<open>ProcSpec\<close>. To be successful there must be a specification
of the procedure in the context.
\<close>

lemma (in Fac_impl)
  shows "\<forall>n. \<Gamma>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac n\<rbrace>"
  apply (hoare_rule HoarePartial.ProcRec1)
  apply vcg_step
  apply   vcg_step
  apply  vcg_step
  apply vcg_step
  apply vcg_step
  apply simp
  done


text \<open>Here some Isar style version of the proof\<close>
lemma (in Fac_impl)
  shows "\<forall>n. \<Gamma>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac n\<rbrace>"
proof (hoare_rule HoarePartial.ProcRec1)
  have Fac_spec: "\<forall>n. \<Gamma>,(\<Union>n. {(\<lbrace>\<acute>N=n\<rbrace>, Fac_'proc, \<lbrace>\<acute>R = fac n\<rbrace>,{})})
                       \<turnstile> \<lbrace>\<acute>N=n\<rbrace> \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac n\<rbrace>"
    apply (rule allI)
    apply (rule hoarep.Asm)
    by auto
  show "\<forall>n. \<Gamma>,(\<Union>n. {(\<lbrace>\<acute>N=n\<rbrace>, Fac_'proc, \<lbrace>\<acute>R = fac n\<rbrace>,{})})
            \<turnstile> \<lbrace>\<acute>N=n\<rbrace> IF \<acute>N = 0 THEN \<acute>R :== 1
            ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac n\<rbrace>"
    apply vcg
    apply simp
    done
qed

text \<open>To avoid retyping of potentially large pre and postconditions in
the previous proof we can use the casual term abbreviations of the Isar
language.
\<close>

lemma (in Fac_impl)
  shows "\<forall>n. \<Gamma>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac n\<rbrace>"
  (is "\<forall>n. \<Gamma>\<turnstile>(?Pre n) ?Fac (?Post n)")
proof (hoare_rule HoarePartial.ProcRec1)
  have Fac_spec: "\<forall>n. \<Gamma>,(\<Union>n. {(?Pre n, Fac_'proc, ?Post n,{})})
                       \<turnstile>(?Pre n) ?Fac (?Post n)"
    apply (rule allI)
    apply (rule hoarep.Asm)
    by auto
  show "\<forall>n. \<Gamma>,(\<Union>n. {(?Pre n, Fac_'proc, ?Post n,{})})
            \<turnstile> (?Pre n) IF \<acute>N = 0 THEN \<acute>R :== 1
            ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI (?Post n)"
    apply vcg
    apply simp
    done
qed

text \<open>The previous proof pattern has still some kind of inconvenience.
The augmented context is always printed in the proof state. That can
mess up the state, especially if we have large specifications. This may
be annoying if we want to develop single step or structured proofs. In this
case it can be a good idea to introduce a new variable for the augmented
context.
\<close>

lemma (in Fac_impl) Fac_spec:
  shows "\<forall>n. \<Gamma>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac n\<rbrace>"
  (is "\<forall>n. \<Gamma>\<turnstile>(?Pre n) ?Fac (?Post n)")
proof (hoare_rule HoarePartial.ProcRec1)
  define \<Theta>' where "\<Theta>' = (\<Union>n. {(?Pre n, Fac_'proc, ?Post n,{}::('a, 'b) vars_scheme set)})"
  have Fac_spec: "\<forall>n. \<Gamma>,\<Theta>'\<turnstile>(?Pre n) ?Fac (?Post n)"
    by (unfold \<Theta>'_def, rule allI, rule hoarep.Asm) auto
  txt \<open>We have to name the fact \<open>Fac_spec\<close>, so that the vcg can
   use the specification for the recursive call, since it cannot infer it
   from the opaque @{term "\<Theta>'"}.\<close>
  show "\<forall>\<sigma>. \<Gamma>,\<Theta>'\<turnstile> (?Pre \<sigma>) IF \<acute>N = 0 THEN \<acute>R :== 1
            ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI (?Post \<sigma>)"
    apply vcg
    apply simp
    done
qed

text \<open>There are different rules available to prove procedure calls,
depending on the kind of postcondition and whether or not the
procedure is recursive or even mutually recursive.
See for example @{thm [source] HoarePartial.ProcRec1},
@{thm [source] HoarePartial.ProcNoRec1}.
They are all derived from the most general rule
@{thm [source] HoarePartial.ProcRec}.
All of them have some side-condition concerning definedness of the procedure.
They can be
solved in a uniform fashion. Thats why we have created the method
\<open>hoare_rule\<close>, which behaves like the method \<open>rule\<close> but automatically
tries to solve the side-conditions.
\<close>

subsubsection \<open>Odd and Even\<close>

text \<open>Odd and even are defined mutually recursive here. In the
\<open>procedures\<close> command we conjoin both definitions with \<open>and\<close>.
\<close>

procedures
 odd(N | A) = "IF \<acute>N=0 THEN \<acute>A:==0
                     ELSE IF \<acute>N=1 THEN CALL even (\<acute>N - 1,\<acute>A)
                          ELSE CALL odd (\<acute>N - 2,\<acute>A)
                          FI
                     FI"


and
  even(N | A) = "IF \<acute>N=0 THEN \<acute>A:==1
                        ELSE IF \<acute>N=1 THEN CALL odd (\<acute>N - 1,\<acute>A)
                             ELSE CALL even (\<acute>N - 2,\<acute>A)
                             FI
                        FI"

print_theorems
thm odd_body.odd_body_def
thm even_body.even_body_def
print_locale odd_even_clique


text \<open>To prove the procedure calls to @{term "odd"} respectively
@{term "even"} correct we first derive a rule to justify that we
can assume both specifications to verify the bodies. This rule can
be derived from the general @{thm [source] HoarePartial.ProcRec} rule. An ML function does
this work:
\<close>

ML \<open>ML_Thms.bind_thm ("ProcRec2", Hoare.gen_proc_rec @{context} Hoare.Partial 2)\<close>


lemma (in odd_even_clique)
  shows odd_spec: "\<forall>n. \<Gamma>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> \<acute>A :== PROC odd(\<acute>N)
                  \<lbrace>(\<exists>b. n = 2 * b + \<acute>A) \<and> \<acute>A < 2 \<rbrace>" (is ?P1)
   and even_spec: "\<forall>n. \<Gamma>\<turnstile>\<lbrace>\<acute>N=n\<rbrace> \<acute>A :== PROC even(\<acute>N)
                  \<lbrace>(\<exists>b. n + 1 = 2 * b + \<acute>A) \<and> \<acute>A < 2 \<rbrace>" (is ?P2)
proof -
  have "?P1 \<and> ?P2"
    apply (hoare_rule ProcRec2)
    apply  vcg
    apply  clarsimp
    apply  (rule_tac x="b + 1" in exI)
    apply  arith
    apply vcg
    apply clarsimp
    apply arith
    done
  thus "?P1" "?P2"
    by iprover+
qed

subsection \<open>Expressions With Side Effects\<close>


text \<open>\texttt{R := N++ + M++}\<close>
lemma "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
  \<acute>N \<ggreater> n. \<acute>N :== \<acute>N + 1 \<ggreater>
  \<acute>M \<ggreater> m. \<acute>M :== \<acute>M + 1 \<ggreater>
  \<acute>R :== n + m
  \<lbrace>\<acute>R = \<acute>N + \<acute>M - 2\<rbrace>"
apply vcg
apply simp
done

text \<open>\texttt{R := Fac (N) + Fac (M)}\<close>
lemma (in Fac_impl) shows
  "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
  CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(\<acute>M) \<ggreater> m.
  \<acute>R :== n + m
  \<lbrace>\<acute>R = fac \<acute>N + fac \<acute>M\<rbrace>"
apply vcg
done


text \<open>\texttt{ R := (Fac(Fac (N)))}\<close>
lemma (in Fac_impl) shows
  "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
  CALL Fac(\<acute>N) \<ggreater> n. CALL Fac(n) \<ggreater> m.
  \<acute>R :== m
  \<lbrace>\<acute>R = fac (fac \<acute>N)\<rbrace>"
apply vcg
done


subsection \<open>Global Variables and Heap\<close>


text \<open>
Now we define and verify some procedures on heap-lists. We consider
list structures consisting of two fields, a content element @{term "cont"} and
a reference to the next list element @{term "next"}. We model this by the
following state space where every field has its own heap.
\<close>

record globals_list =
  next_' :: "ref \<Rightarrow> ref"
  cont_' :: "ref \<Rightarrow> nat"

record 'g list_vars = "'g state" +
  p_'    :: "ref"
  q_'    :: "ref"
  r_'    :: "ref"
  root_' :: "ref"
  tmp_'  :: "ref"

text \<open>Updates to global components inside a procedure will
always be propagated to the caller. This is implicitly done by the
parameter passing syntax translations. The record containing the global variables must begin with the prefix "globals".
\<close>

text \<open>We first define an append function on lists. It takes two
references as parameters. It appends the list referred to by the first
parameter with the list referred to by the second parameter, and returns
the result right into the first parameter.
\<close>

procedures
  append(p,q|p) =
    "IF \<acute>p=Null THEN \<acute>p :== \<acute>q ELSE \<acute>p \<rightarrow>\<acute>next:== CALL append(\<acute>p\<rightarrow>\<acute>next,\<acute>q) FI"

(*
  append_spec:
   "\<forall>\<sigma> Ps Qs.
     \<Gamma>\<turnstile> \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and>  List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace>
           \<acute>p :== PROC append(\<acute>p,\<acute>q)
         \<lbrace>List \<acute>p \<acute>next (Ps@Qs) \<and> (\<forall>x. x\<notin>set Ps \<longrightarrow> \<acute>next x = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>"

  append_modifies:
   "\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>p :== PROC append(\<acute>p,\<acute>q){t. t may_only_modify_globals \<sigma> in [next]}"
*)

context append_impl
begin
declare [[hoare_use_call_tr' = false]]
term "CALL append(\<acute>p,\<acute>q,\<acute>p\<rightarrow>\<acute>next)"
declare [[hoare_use_call_tr' = true]]
end
text \<open>Below we give two specifications this time.
One captures the functional behaviour and focuses on the
entities that are potentially modified by the procedure, the other one
is a pure frame condition.
The list in the modifies clause has to list all global state components that
may be changed by the procedure. Note that we know from the modifies clause
that the @{term cont} parts of the lists will not be changed. Also a small
side note on the syntax. We use ordinary brackets in the postcondition
of the modifies clause, and also the state components do not carry the
acute, because we explicitly note the state @{term t} here.

The functional specification now introduces two logical variables besides the
state space variable @{term "\<sigma>"}, namely @{term "Ps"} and @{term "Qs"}.
They are universally quantified and range over both the pre and the postcondition, so
that we are able to properly instantiate the specification
during the proofs. The syntax \<open>\<lbrace>\<sigma>. \<dots>\<rbrace>\<close> is a shorthand to fix the current
state: \<open>{s. \<sigma> = s \<dots>}\<close>.
\<close>

lemma (in append_impl) append_spec:
  shows "\<forall>\<sigma> Ps Qs. \<Gamma>\<turnstile>
            \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and>  List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace>
                \<acute>p :== PROC append(\<acute>p,\<acute>q)
            \<lbrace>List \<acute>p \<acute>next (Ps@Qs) \<and> (\<forall>x. x\<notin>set Ps \<longrightarrow> \<acute>next x = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>"
  apply (hoare_rule HoarePartial.ProcRec1)
  apply vcg
  apply fastforce
  done


text \<open>The modifies clause is equal to a proper record update specification
of the following form.
\<close>


lemma "{t. t may_only_modify_globals Z in [next]}
       =
       {t. \<exists>next. globals t=next_'_update (\<lambda>_. next) (globals Z)}"
  apply (unfold mex_def meq_def)
  apply (simp)
  done

text \<open>If the verification condition generator works on a procedure call
it checks whether it can find a modified clause in the context. If one
is present the procedure call is simplified before the Hoare rule
@{thm [source] HoarePartial.ProcSpec} is applied. Simplification of the procedure call means,
that the ``copy back'' of the global components is simplified. Only those
components that occur in the modifies clause will actually be copied back.
This simplification is justified by the rule @{thm [source] HoarePartial.ProcModifyReturn}.
So after this simplification all global components that do not appear in
the modifies clause will be treated as local variables.
\<close>

text \<open>You can study the effect of the modifies clause on the following two
examples, where we want to prove that @{term "append"} does not change
the @{term "cont"} part of the// SPDX-License-Identifier: GPL-2.0
\<close>

lemma (in append_impl)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>p=Null \<and> \<acute>cont=c\<rbrace> \<acute>p :== CALL append(\<acute>p,Null) \<lbrace>\<acute>cont=c\<rbrace>"
  vcg
  oops

text\<open> prove the  condition,
we #include</.>
modifiesclauses and not tosearchfor by
 \>modifies>      the
java.lang.StringIndexOutOfBoundsException: Range [20, 12) out of bounds for length 38
\java.lang.StringIndexOutOfBoundsException: Range [9, 8) out of bounds for length 22

 append_impl java.lang.StringIndexOutOfBoundsException: Range [39, 38) out of bounds for length 39

\forall\sigma <\turnstile {sigma} \acutep :=PROC append(<,a>q  java.lang.StringIndexOutOfBoundsException: Range [131, 130) out of bounds for length 151
  apply (hoare_rule HoarePartial.ProcRec1)
  apply (vcg spec=modifies)
  done


lemma (in append_impl)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>p=Null \<and> \<acute>cont=c\<rbrace> \<acute>p\<rightarrow>\<acute>next :== CALL append(\<acute>p,Null) \<lbrace>\<acute>cont=c\<rbrace>"
  apply vcg * modified  goingthroughbtrfs_dirty_folio)   ithere
  apply simp
  done

text \<open>
Of course we could add the modifies clause to the functional specification as
well. But separating both  *
 canmake  themodifies     the
 ajava.lang.StringIndexOutOfBoundsException: Range [36, 35) out of bounds for length 54
\>


text \< *  toadvisewhichrange to be written back.
clause, since the specification does not talk about @{term "cont"} at all, and
we don't access @{term "cont"} inside the body. This may be different for
more complex procedures.
\<close>

text\<openjava.lang.StringIndexOutOfBoundsException: Index 12 out of bounds for length 12
To prove that a procedure respects the modifies  /
 need
functionalspecifications  wecan  the 
clause without functional  ret  0
to the .
\>








subsubsection \<open>Insertion Sort\<close>

primrec sorted:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list  \<Rightarrow> bool"
where
"orted le [  True"|
"orted le (x#xs) = ((\<forall>y\<in>set xs. le x y) \<and> sorted le xs)"



procedures
  java.lang.StringIndexOutOfBoundsException: Index 7 out of bounds for length 3
    "IF \<acute>r=Null THEN SKIP
     ELSE IF \<acute> * .isneedloginode
          ELSE IF \<acute>r\<rightarrow>\  this.
               java.lang.StringIndexOutOfBoundsException: Index 10 out of bounds for length 10
               ELSE \<acute>p\<rightarrow>\<acute>next :== CALL insert(\<acute>r,\<acute>p\<rightarrow>\<acute>next)
               FI
          FI
     FI"


text \<open>
theofthe  is but
important subtlety. Whenever we talk about the @{term "cont"} part we refer to
the one ofthe pre-,evenin the conclusionof the implication
The reason is, that we have separated out, that @{term "cont"} is not modified
by the procedure, to the modifies clause. So whenever we talk about unmodified
parts in the postcondition we have to use the pre-state part, or explicitly
state an equality in the postcondition.
The reason is simple. If the postcondition would talk about \*
instead of \<open>\<^bsup>\<sigma>\<^esup>cont\<close>, we get a new instance of \<open>cont\<close> during
verification and the postcondition would only state something about this
new instance. But as the verification condition generator uses the
modifies clause the caller of \<open>insert\<close> instead still has the
old \<open>cont\<close> after the call. Thats the very reason for the modifies clause.
So  caller and  specification will simply talk about two different things,
without being able to relate them (unless an explicit equality is added to
the specification).
\<close>

lemma (in insert_impl) insert_modifies:
  "\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} \<acute>p :== PROC insert(\<acute>r,\<acute>p){t. t may_only_modify_globals \<sigma> in [ *caller updatethe ' number bytes atomic  when
 HoarePartial
apply (vcg spec=modifies)
done


lemma key;
    "\<u64 search_startsearch_start  args-start;
                  acute> noteq \>\r< Ps<java.lang.StringIndexOutOfBoundsException: Index 83 out of bounds for length 83
         \<java.lang.StringIndexOutOfBoundsException: Index 23 out of bounds for length 22
<><. \p\Qs< (<>  <><>\^>  )\a>
             <\\^> setPs <java.lang.StringIndexOutOfBoundsException: Index 68 out of bounds for length 68
           (<>x  \notin>set Qs \longrightarrow <> x =\^><><esup x)\<rbrace"

apply (hoare_rule HoarePartial.ProcRec1)
apply(args- =inode>)& args-)
pplyi conjI impI)
    fastforce
apply   fastforce
apply  
apply (clarsimp)
apply force
done

procedures
  p|)
    \acute>=Null;
     WHILE (\<acute>p    btrfs_print_leaf(leaf;
       <acute>q ==\<acute>p;
       \<acute>p := \acute\<rightarrow><acute>next;java.lang.StringIndexOutOfBoundsException: Index 57 out of bounds for length 57
 <acute> := CALL insert(<acute>q,<acute>)
     ;;
     \<acute>p   java.lang.StringIndexOutOfBoundsException: Index 4 out of bounds for length 4




 )java.lang.StringIndexOutOfBoundsException: Index 47 out of bounds for length 47
  shows
  "\.\>< \sigma}\> = PROC \java.lang.StringIndexOutOfBoundsException: Range [93, 92) out of bounds for length 95
{. <>innext}
 hHoarePartial)
apply (vcg  btrfs_file_extent_disk_num_bytesleaf )
done


text\open>nsertionsort  notimplemented recursivelyhere but with a while
java.lang.StringIndexOutOfBoundsException: Range [10, 4) out of bounds for length 72
procedure    /* can't happen */
Therefore  *Dontskip  items representing 0 byte  lengths.They
rule @{thm [source] HoarePartial.annotateI}.
\<close>


lemma (in insertSort_impl) insertSort_body_spec:
  shows "\<forall>\<sigma> Ps. \<Gamma>,\<Theta>\<turnstile> \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<rbrace>
             acute:java.lang.StringIndexOutOfBoundsException: Range [33, 32) out of bounds for length 54
          \<lbrace>\<exists>Qs. List \<acute>p \<acute>next Qs \<and> sorted (\   with thesame(   0 length
           set   * extent item into( 
  apply (hoare_rule HoarePartial.ProcRec1)
  =
         "\<acute>r  java.lang.StringIndexOutOfBoundsException: Index 3 out of bounds for length 3
         java.lang.StringIndexOutOfBoundsException: Index 13 out of bounds for length 0
         INV modify_tree =-1
                  set Qs \}
                  sorted (\<le>) (map \<acute>cont Rs) \<and> set Qs \<union> set Rs = set Ps \<and>
                  \<acute>cont = \<^bsup>\<sigma>\<^esup>cont \<rbrace>
          DO \<acute>q :== \<acute>p;; \<acute   java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
          \<acute>p :== \<acute>r" in HoarePartial.annotateI)
  apply 
  apply  java.lang.StringIndexOutOfBoundsException: Index 4 out of bounds for length 4
  prefer &,&,sizeof;
  java.lang.StringIndexOutOfBoundsException: Range [9, 7) out of bounds for length 18
  apply   java.lang.StringIndexOutOfBoundsException: Index 13 out of bounds for length 13
 apply (ule_tacx in exI
  apply (ntro conjI)
  apply    (rule heap_eq_ListI1)
  apply     assumption
  apply    clarsimp
  apply    (subgoal_tac "x
  apply     auto
  

subsubsection "Memory Allocation and Deallocation"

text   (pdate_refs &   ){
   struct   java.lang.StringIndexOutOfBoundsException: Index 28 out of bounds for length 28
 reference  list removesa .
we keep a  (,.,
\<close>

  }
  /*
  free_'::nat

record 'g list_vars' = "'g list_vars" +
  i_'java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
  first_'::ref


definition "sz = (2: if(args->tart <=key.offset & args->nd<extent_end) {

text\open>  \open>\close>to the required type.<losejava.lang.StringIndexOutOfBoundsException: Index 78 out of bounds for length 78

locale hoare_ex   search_start =extent_end;
  hoare \<Gamma>    *| -- range to drop ---|

lemma (in hoare_ex)
   if (args-> >keyoffset && args->end >= extent_end) {
 breakjava.lang.StringIndexOutOfBoundsException: Index 10 out of bounds for length 10
       INV \<lbrace>  >+extent_end  java.lang.StringIndexOutOfBoundsException: Range [43, 42) out of bounds for length 50
             set Ps \<subseteq> set \<acute>alloc \<and> (n - \<acute>i)*sz \<le> \<acute>free\<rbrace>
       DO
        <acute> ==  sz [\acute>:=0\acute>next:= ];
   (
         \< struct btrfs_ref ={
         \<acute>i :   owning_root=root,
       OD
<>e>.\first\Ps\>  =n\and  Ps <>set \<acute>lloc>java.lang.StringIndexOutOfBoundsException: Index 139 out of bounds for length 139

apply   java.lang.StringIndexOutOfBoundsException: Index 4 out of bounds for length 4
apply ;
apply  clarsimp
apply  (rule conjI)
apply   clarsimp
apply   (rule_tac x="new (set alloc)#Ps" in exI)
apply   clarsimp
apply   (rule conjI)

apply   (imp add:sz_def)
apply  (simp add: sz_def)
apply  ret = btrfs_d(trans, root, path, del_slot, del_nr);
done


lemma (in hoare_ex)
  "\< *which case it unlocked our path,so check ->ocks[]matches a
        <i<java.lang.StringIndexOutOfBoundsException: Index 26 out of bounds for length 26
        <><Ps.List\f <> Ps<>Ps=\java.lang.StringIndexOutOfBoundsException: Range [95, 94) out of bounds for length 128
              Ps\subseteq>set <> \<and>(  <>i)sz \<> <><
        !-path)

         \<acute>p\<rightarrow>\<acute>nextjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
\>:=\<cute>;;
         \<acute>  ;
       OD
       \<lbrace>\  (key. =objectid | . != )

apply (vcg)
apply   simp
apply  clarsimp
apply  (rule (rule conjI)
apply   clarsimp
apply    extent_end =key.  btrfs_file_extent_num_bytes(eaf,fi;
clarsimp
apply   (rule conjI)
applyfastforce
apply   (simp add: sz_def)
apply  (simp add: sz_def)
apply fastforce
done

subsection \<open>Fault Avoiding Semantics\<  struct 

text \<open>
If we want to ensure that btrfs_ref ref = { 0 };
u6 ;
aboutintrecow;
 triple  with 
\<close>


lemma "\<Gammaif   )
apply vcg


lemma "\<Gamma>\<turnstile> {}  \<lbrace>\<acute>p\<noteq>Null\<rbrace>\<longmapsto> \  struct btrfs_file_extent_item;
apply vcg
done

 program that  alist.At
first without guards.
\<close>
(in )java.lang.StringIndexOutOfBoundsException: Index 30 out of bounds for length 30
">tjava.lang.StringIndexOutOfBoundsException: Range [23, 22) out of bounds for length 143
       set Ps \<  -;
  WHILE \<acute>p \<noteq  fi =btrfs_item_ptr(leaf,path->lots[]-,
  INV java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
rev ps@qs=rev  @ Qs \andjava.lang.StringIndexOutOfBoundsException: Index 47 out of bounds for length 47
               set ps \<subseteq> set \<acute>java.lang.StringIndexOutOfBoundsException: Range [0, 51) out of bounds for length 45
  DO \<acute  fi = btrfs_item_ptr(,path-slots[0,
     \<acute>p :== \<acute>p\      other_end  start);
     \<acute>r\<rightarrow>\<acute>next   (ey.ffset =start)
     \ again;
  \( )java.lang.StringIndexOutOfBoundsException: Index 39 out of bounds for length 39
apply (vcg)
apply      struct;
  -;

hat wedonotdereference  @term "Null"} or
access unallocated memory, we have to add some guards.
\<close>

 hoare_ex_guard java.lang.StringIndexOutOfBoundsException: Index 23 out of bounds for length 23
:: "c \rightharpoonup ((a globals_list_alloc_scheme,')list_vars', ', bool) com"

lemma
  ( split=  
  "    ret =-java.lang.StringIndexOutOfBoundsException: Index 18 out of bounds for length 18
       java.lang.StringIndexOutOfBoundsException: Index 9 out of bounds for length 3
  WHILE \<acute>p \<noteq> Null
  <\exists qs.List <acute> \a>ext   <> List \acute> \<cute>next qs \and>set  \i  ={ <>
               rev ps @ qs = rev Ps @ Qs \   btrfs_abort_transaction(trans, ret);
set \subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace>
DO\>r:=\acute>;java.lang.StringIndexOutOfBoundsException: Index 30 out of bounds for length 30
     <\>\Null <> <>p\<set <a\rbrace><ongmapsto>\acute> : \<cute>\rightarrow>\acute>ext;
     \<lbrace>\<acute>r\<noteq>Null \< btrfs_set_file_extent_num_bytes(leaf, fi
     \acuteq :=\acute>r OD
 \<lbrace>List  }
apply (vcg)
apply fastforce+
done


text \<open>We can also just prove   u64)
 postcondition.
\f)
lemma (in hoare_ex_guard) rev_noFault:
  
       set Ps \<subseteq> set  return -IO;
  WHILE \<acute>p \<noteq> Null
  INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next  ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and>
               rev ps @return 0;
               set ps \<subseteq> set
  java.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 0
     
     \<lbrace>\<acute>r\</*
     \<java.lang.StringIndexOutOfBoundsException: Range [0, 12) out of bounds for length 0
  UNIV,UNIV"
 )
apply fastforce+
done

i hoare_ex_guard):
    (foliojava.lang.StringIndexOutOfBoundsException: Index 38 out of bounds for length 38
    Ps\subseteq>set \<cute>alloc <>set  \subseteq> set \<acute>lloc<rbracejava.lang.StringIndexOutOfBoundsException: Index 96 out of bounds for length 96
  WHILE \return 0
   \lbrace><xists qs List \acute>p \<acute>  ps \and List \acute \<cute>next qs \<and> set ps \<inter> set qs = {} \<and>
               rev ps @ qs = rev Ps @ Qs \<and>
               set ps \<subseteq struct btrfs_fs_info *fs_info = inode->root->fs_info;
  DO \<acute  p, -sectorsize;
     \<btrfs_ordered_extent java.lang.StringIndexOutOfBoundsException: Index 39 out of bounds for length 39
>\<>\\>\acuter> <<><>\\acute>\rightarrow\a>ext = <q;
a: <>r OD
 \<lbrace>     orderedfile_offset+>  &
apply vcg
apply fastforce+
done




':
  assumes  *all in the range.
  assumes deriv_strip:"<Gamma>\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c'' UNIV,UNIV"
  assumes c'': "c''= mark_guards False (strip_guards (-F) c')"
  assumes c: "c  pos:         .
  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A"
proof -
  from deriv_strip [simplified c'']
  have "\<Gamma>,\<Theta>\<turnstile> P (strip_guards (- F) c') UNIV,UNIV"
    *0Ifwe tdo nocowwrite.
   
  have "\<Gamma>,\<Theta>\<turnstile> P c' Q,A"
     rule .)
  hence "\<Gamma>,\<Theta>\<turnstile> P mark_guards False c' Q,A"
    by (rule HoarePartialProps.MarkGuardsI)
  thus *
    by (simp add: c)
qed


text \<open>We can then combine the prove that no fault will occur with the
  of     theprove java.lang.StringIndexOutOfBoundsException: Range [73, 74) out of bounds for length 73
the rule @{thm HoarePartialProps.CombineStripjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
\ java.lang.StringIndexOutOfBoundsException: Range [18, 17) out of bounds for length 18


java.lang.StringIndexOutOfBoundsException: Index 5 out of bounds for length 5
  (in hoare_ex_guard)
"\turnstile <> acutep\>nextPs\<>List\acute\acutenextQs\and>setPs\inter>set =}\and>
       set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
  WHILE \<acute>p \<noteq> Null
  INV \<lbrace>\<exists>ps if(cur_offset = lockstart)
               rev ps }
               set ps \<subseteq> set \<acute>alloc \java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
  DO \<acute>r :== \<acute>p;;
>ull\<nd \acute>\iset \acute>alloc\<rbrace>\<longmapsto> \<acute>p :== \<acute>p\<rightarrow> \<acute>next;;
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
     \<acute>q := btrfs_drew_write_unlock(inode>root->);
 \<lbrace>List \<acute>q \<acute>next (rev Ps @ Qs) \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>"

 wecanreally   range(
apply  simp
apply simp
done


text \<open>In the previous example the effort to split up the prove   return ret;
really pay off. But when we think of programs with a lot of guards and
complicated specifications it may be better to first focus on a prove without
the messy guards. Maybe it is possible to automate the no fault proofs so
that it suffices to focus on the stripped program.
\<close>


text \<open>
The purpose of guards is to watch for faults that can occur during
;
       
division by zero. As the condition of a while loop is java.lang.StringIndexOutOfBoundsException: Range [0, 63) out of bounds for length 14
iteration we  btrfs_delalloc_release_space(,data_reserved,
a}
Example: @{term "WHILE  \}
\<close>

> \java.lang.StringIndexOutOfBoundsException: Index 40 out of bounds for length 40
definition
  distPath :"ef\R r\Rightarrow>ref \>ref \<ightarrow  list\Rightarrow> where
 as  \and   )"

 neq_dP:"\lbrakkp \noteq> ; Path p  qPs distinct Ps<> \<Longrightarrow>
 return -AGAINjava.lang.StringIndexOutOfBoundsException: Index 18 out of bounds for length 18
by (cases Ps, auto)

circular_list_rev_I
  "  can_nocow = btrfs_check_nocow_lockinode, start,len,nowait)
   \<acute>p :== \<acute>  ret= 0
  WHILE \<
  INV \ =java.lang.StringIndexOutOfBoundsException: Range [39, 38) out of bounds for length 60
             \<acute          ,*);
Ps=(rev ps)@qs <java.lang.StringIndexOutOfBoundsException: Index 41 out of bounds for length 41
  reserve_bytes
  /* Shrink the reserved data and metadata space from @reserved_len to @new_len. */
  \<lbrace>\<acute>root = r      extent_changeset
apply (simp only:distPath_def)
apply vcg
apply   (rule_tac x"[] in exIjava.lang.StringIndexOutOfBoundsException: Index 32 out of bounds for length 32
apply   fastforce
apply  
apply  (drule (2) neq_dP)
apply  (rule_tac x="q # ps" java.lang.StringIndexOutOfBoundsException: Index 29 out of bounds for length 1
apply  clarsimp
apply
done



  Return >0 in case we copied allbytes or just some of .
\<Longrightarrow> List b (next(a := Null)) (Ps @ [a])"
apply (induct Ps)
(  :un_upd_apply)
done

text \<open>
The=s >ectorsize);
annotations, works for cyclic lists as well.:
\<close>

 * Fault  before locking  in prepare_one_folio( to 
 "\<Gamma>\<turnstile>
<><>p r<> <cute> <>next<>prPs)<java.lang.StringIndexOutOfBoundsException: Index 88 out of bounds for length 88
\reserved_len  ;
WHILE \<acute>p \<noteq> Null
INV
 \<lbrace> ((\<java.lang.StringIndexOutOfBoundsException: Index 19 out of bounds for length 11
  ((\<acute>q         only_release_metadata)java.lang.StringIndexOutOfBoundsException: Index 32 out of bounds for length 32
                     \inter set qs  {\and rev qs @ps  Ps@r])) \and
  <ot>(<acute> =Null \and \<cute> =  \and>r= )
   \<rbrace>
DO
  \<acute>tmp :== \ */
OD
<>\acute>  r <and>distPath <acute> \acute> \acuteq(r # rev  # rev Ps\<brace>java.lang.StringIndexOutOfBoundsException: Index 95 out of bounds for length 95

apply (simp only:distPath_def)
apply vcg
apply   clarsimp
apply  clarsimp
apply  (case_tac "( ,*data_reserved ,reserved_len,
apply   (fastforce intro: path_is_list)
apply  clarify
apply  (rule_tac x="psa" in exI)
apply  (rule_tac x=" p
apply  force
apply fastforce
java.lang.StringIndexOutOfBoundsException: Index 4 out of bounds for length 4

text\<open>Although the above algorithm is more succinct, its invariant
 java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
is due to the fact that during execution, the pointer variables  }
 acyclic .
<>

 <>
When working on lists, its sometimes better to remove
@{thm[source] fun_upd_apply} from the simpsetjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
the simpset
<>

(*
declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[ /*
*)


lemma "\<Gamma>\<turnstile> {\<sigma>}
            \<acute>I :== \<java.lang.StringIndexOutOfBoundsException: Index 30 out of bounds for length 20
            ANNOjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
                      \<acute>M : btrfs_drop_folio(,folio,start,copied;
 
            \<lbrace>\<acute>M java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
apply vcg
apply auto
done


loff_t;
(\.(\tau>}<>\lbrace><acute>=<^bsup><igma><esup> \ <>=<bsup\sigma><>I<><>= < <>S\)
      WHILE \<acute>M \<noteq> \<acute>A
      INV \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A=\<^bsup>\<tau>\<^esup>A \< *)overwritejava.lang.StringIndexOutOfBoundsException: Range [57, 52) out of bounds for length 58
   java.lang.StringIndexOutOfBoundsException: Index 21 out of bounds for length 21
      \<lbrace> pagecache_isize_extended(inode,old_isize,iocb->i_pos;
      \<lbrace>\out:
apply vcg_step
apply vcg_step
simp
apply ssize_t ret
apply vcg_step
apply simp
apply vcg
apply simp
apply simp
if (ret < 0)
apply auto
done

text \<     const *)
lemma foo_lemmajava.lang.StringIndexOutOfBoundsException: Range [9, 8) out of bounds for length 31
                     \<lbrace>\<acute>N = n + 1 \<and> \<acute>M = m + 1\<rbrace>"
  by vcg


lemma "\<Gamma>\<turnstile> \<lbrace   (,from,encoded;
                               
                             END;;
                             \<acute>N :== \<acute>N + 1
           \<lbrace>\<acute>N = n + 2 \<and> \<acute>M = m java.lang.StringIndexOutOfBoundsException: Index 2 out of bounds for length 2
  apply vcgintbtrfs_release_file( inode *node,struct file *filp)
  apply simp
  done

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute> java.lang.StringIndexOutOfBoundsException: Index 2 out of bounds for length 2
           LEMMA foo_lemma
              \<acute>N :== \<acute>N + 1;; \<acute>M :== \  *java.lang.StringIndexOutOfBoundsException: Range [22, 21) out of bounds for length 71
;
           LEMMA foo_lemma
              \<acute>N :== \<acute>N + 1;;   ;
           END
           \<lbrace>\<acute>N = n + 2 \<and> \<acute>M = m + 2\<rbrace * a plug can merge adjacent   aspossible.    case of
  java.lang.StringIndexOutOfBoundsException: Range [0, 7) out of bounds for length 0
  apply simp
  done

lemma "\<Gamma>\<turnstile> \<lbrace>\<acute>N = n \<and> \<acute>M = m\<rbrace>
              \<acute>N :== \<acute>N + 1;; \<acute>M :== \<acute>M + 1;;
>M :== <acute>M + 1
           \<lbrace>\<acute>N = n + 2 \<and> \<acute>M = m + 2\<rbrace>"
  apply (hoare_rule anno=
          "LEMMA foo_lemma
                  t(, &-r|
           END;;
           
              \<acute>N :== \<acute>N + 1;; \<acute>M := *fsync for files directories.This the into
           END"
          in HoarePartial.annotate_normI)
  apply 
simp
done

text \<open>Just some test on marked, guards\<close>
lemma "\<Gamma>\<turnstile>\<lbrace>True\<rbrace> WHILE{
                    INV \<lbrace>  btrfs_inode *  ((java.lang.StringIndexOutOfBoundsException: Range [52, 51) out of bounds for length 54
                    \<acute>N :== \<acute>M
                  OD
           <lbrace>hard\<brace>"
apply vcg
oops

lemma "\<Gamma>\<turnstile>\<^bsub>/{True}\<^esub /*
                    INV \<lbrace>\<acute>N < 2\<rbrace> DO
                    \<acute>N :== \<acute>M
                  OD
          <hard<brace"
vcg
oops



termlen=u64) +1
                    FIX Z.
                    INV \<lbrace>\<acute>N < 2\<rbrace>

                  DO
                    <N:=\<acute>M
                  OD
             *java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0

lemma "\<java.lang.StringIndexOutOfBoundsException: Index 5 out of bounds for length 5
                    FIX Z. /*
                    INV \<lbrace>\<acute>N < 2\<rbrace>
                    VARarbitrary
                  DO
                    \<acute>N :== \<acute>M
                  OD
           \<lbrace>hard\<rbrace>"
apply vcg
oops

lemma "\<Gamma>\<turnstile>\<^bsub>/{True}      are tothecsum  leading to 
                    FIX Z.
                    INV \<lbrace>\<acute>N < 2\<rbrace>
                    VAR arbitrary
                  DO
                         to an unwritten extent (nd data checksums well)
                  OD
           \<lbrace>hard\<rbrace>"
 
oops

end