(*<*)
theory Blatt5 = "Hoare":
(*>*)

section {* Hoare Logik *}
text {* Die Beschreibung imperativer Programme durch sogenannte Hoare-Tripel
eignet sich gut, um Eigenschaften von Programmen zu beweisen. Hierbei
werden Programmkonstrukte mit Zusicherungen (= Pr"adikate "uber
die Programmvariablen) annotiert, die das
Verhalten des Programms beschreiben. @{text "{P} c {Q}"} ist genau dann ein
g"ultiges Hoare-Tripel, wenn f"ur das Programm @{text c} und die
Vorbedingung @{text P} nach Ausf"uhrung von @{text c} die Nachbedingung
@{text Q} gilt.

F"ur Isabelle/HOL existiert eine Definition der Hoare-Logik
f"ur eine einfache imperative Sprache mit folgenden syntaktischen
Konstrukten: 

\(
\begin{array}{lll}
\name{c} & =   & \name{SKIP}\\
  &\mid &  \name{x} := \name{a}\\
  &\mid &  \name{c}_0;\ \name{c}_1\\
  &\mid &  \name{IF}\ b\ \name{THEN}\ \name{c}_0\ \name{ELSE}\ \name{c}_1\ \name{FI}\\
  &\mid &  \name{WHILE}\ \name{b}\ \name{INV}\ \{\name{I}\}\ \name{DO}\ \name{c}\ \name{OD}\\
p  &=  &\{\name{P}\}\ \name{c}\ \{\name{Q}\}
\end{array}
\)

Wie man sieht, gen"ugt es, innerhalb eines Programms nur den Rumpf
von @{text WHILE}-Schleifen mit einer Schleifeninvariante @{text I}
zu annotieren, f"ur die anderen Konstrukte
lassen sich die schw"achsten Vorbedingungen aus den jeweiligen Nachbedingungen
automatisch ableiten. 
Die Taktik @{text vcg} erzeugt f"ur ein Hoare-Tripel @{text "{P} c {Q}"}
Verifikationsbedingungen, durch die sich die G"ultigkeit des Tripels
beweisen l"a" st.
*}

text {* Hier ein Beispiel. Wir implementieren Multiplikation durch
wiederholte Addition. *}
lemma multiply_by_add: "VARS m s a b
  {a=A \<and> b=B}
    m := 0; s := 0;
    WHILE m\<noteq>a
    INV {s=m*b \<and> a=A \<and> b=B}
    DO s := s+b; m := m+(1::nat) OD
  {s = A*B}"
apply vcg
txt "@{subgoals [display]}"
txt {* Anhand der entstandenen Beweisziele kann man die
Bedeutung der Invariante gut ersehen. 
\begin{enumerate}
\item Die Invariante muss aus der Vorbedingung folgen.
\item Die Invariante zusammen mit der Schleifenbedingung impliziert
      die Invariante nach Ausführung des Schleifenkörpers.
\item Die Invariante zusammen mit der negierten Schleifenbedingung impliziert
      die Nachbedingung.
\end{enumerate}
*}
(*<*)by auto(*>*)

text {* Wir wollen nun die Suche in Arrays korrekt
beweisen. *}

text {* Arrays werden in Isabelle als Listen modelliert. 
Der Operator @{text "!"}  kann verwendet werden,
um einzelne Elemente einer Liste {\"u}ber ihren Index zu selektieren 
(@{text nth}). Mit @{text "set xs"} bekommt man die Menge der Elemente
in der Liste und mit @{text "take i xs"} bekommt man die ersten i Elemente
aus xs, wiederum als Liste.
*}
text {* 
 Sehen Sie sich hierzu die entsprechenden Definitionen und Lemmas 
über @{text nth}, @{text set} und @{text take} an:
\url{http://isabelle.in.tum.de/library/HOL/List.html}
*}

subsection {* Lineare Suche *}  

lemma LinearSearch: "VARS A i
 {True}
 i := 0;
 WHILE i < length A \<and> A!i \<noteq> v
 INV {insert_invariant_here}
 DO
   i := i + 1
 OD
 {if v \<in> set A then A!i = v else i = length A}"
(*<*)
apply vcg
oops
(*>*)

text {* Finden Sie eine geeignete Invariante und beweisen Sie 
        die lineare Suche korrekt. *}
text {*
Hinweis: Das 2. Beweisziel (Erhalt der Invariante in der Schleife) ist
meist am schwierigsten zu zeigen. Es ist deshalb empfehlenswert zunächst die
Beweisziele 1 und 3 anzugehen. Beweisziel 3 stellt schonmal sicher, dass die
Invariante stark genug ist um die Nachbedingung abzuleiten. Mit dem Kommando
@{text "prefer i"} kann man das i-te Beweisziel vorziehen.
*}

subsection {* Binäre Suche *}

text {* Ist das Array sortiert, so kann man die effizientere binäre Suche
verwenden. *}

text {* Definieren sie ein Prädikat @{term sorted}, das eine sortierte Liste
beschreibt. *}

consts sorted:: "('a::linorder) list \<Rightarrow> bool"

constdefs mean:: "nat \<Rightarrow> nat \<Rightarrow> nat"
"mean l u \<equiv> (l + u) div 2"

lemma BinSearch: "VARS A l u p m
 {sorted A \<and> 0 < length A}
 l := 0;
 u := length A - 1;
 p := length A;
 WHILE l \<le> u
 INV {insert_invariant_here}
 DO
   m := mean l u;
   IF A!m < v THEN
      l := m + 1
   ELSE
      IF v < A!m THEN
         u := m - 1
      ELSE p := m; l := u + 1
      FI
   FI
 OD
 {p \<le> length A \<and> (if p = length A then v \<notin> set A else A!p = v)}"
(*<*)
apply vcg
oops
(*>*)

text {* Finden sie eine geeignete Invariante und beweisen Sie 
        die binäre Suche korrekt. *}

text {*
Hinweis: Ein Hilfsprädikat der Art @{term "in_slice v l u A"} welches besagt, 
dass Element @{term v} in Array @{term A} irgendwo zwischen den 
Indizes @{term l} und @{term u} liegt, kann von Nutzen sein.
*}
(*<*)
end
(*>*)