header {* Hoare Logik *}

(*<*)
theory Aufgabe6 = Hoare:
(*>*)

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 (siehe z.B.[1]).

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 Nachbedingung
automatisch ableiten. 
Die Taktik @{text hoare_tac} erzeugt f"ur ein Hoare-Tripel @{text "{P} c {Q}"}
Verifikationsbedingungen, durch die sich die G"ultigkeit des Tripels
beweisen l"a" st.


Beispiele finden Sie unter 
  \texttt{http://www.in.tum.de/\~\relax isabelle/library/HOL/Hoare}

Wichtige Informationen finden Sie unter\\
\texttt{http://www4.in.tum.de/\~\relax isabelle/library/HOL/Hoare/README.html} *}
 

text {*
 Im Folgenden sollen einige imperative Programme mit Hilfe der Hoare
 Logik verifiziert werden.  Die zugrundeliegende Theorie ist in
 \cite{Wenzel:2000:Hoare} genauer beschrieben.  Weitere Informationen
 zur axiomatischen Semantik finden sich z.B.\ in
 \cite[\S5.7.1]{Broy-PartI}
 \cite[\S6]{Winskel:1993} oder \cite[\S4]{Huth-Ryan:2000}.

 \medskip Hier ein einfaches Beispiel zur Anwendung der Hoare Logik.
 Wir verifizieren ein Programm, das zwei nat"urliche Zahlen durch
 wiederholte Addition multipliziert.

 Zuerst deklarieren wir die verwendeten Programmvariablen als
 Record-Typ.
*}

record mult_vars =
  M :: nat
  N :: nat

text {*
 Die zu beweisende Aussage wird als Hoare-Tripel wie folgt formuliert.
 Man beachte die Unterscheidung von Programmvariablen von einfachen
 Werten der Logik (z.B.\ @{text "\<acute>M"} vs.\ @{term a}).
*}

theorem
"|- .{\<acute>M = 0 \<and> \<acute>N = 0}.
    WHILE \<acute>M ~= a
    INV .{\<acute>N = \<acute>M * b}.
    DO \<acute>N := \<acute>N + b; \<acute>M := \<acute>M + 1 OD
    .{\<acute>N = a * b}."

  txt {* \normalsize Die Hauptarbeit des Beweises erledigt die
 \name{hoare} Methode, welche ein mit Invarianten annotiertes
 Hoare-Tripel auf ein rein logisches Problem reduziert. Den Rest kann
 man in diesem Beispiel einfach mit \name{auto} erledigen. *}

  apply hoare
  apply auto
  done

subsection {* Quotient und Rest *}
 
text {* Geben Sie ein annotiertes imperatives Program zur Berechnung
des Quotients und Rests zweier nat"urlichen Zahlen @{text x}
 und @{text y}. Beweisen Sie dann, da" s folgendes Hoare-Tripel g"ultig ist: *}

record quo_vars =
  quo  :: nat
  rest :: nat

theorem "|- .{True}. program .{\<acute>quo * y + \<acute>rest = x \<and> \<acute>rest < y }."
sorry

subsection {* Minimumsuche *}

text {* Gesucht ist ein verifiziertes imperatives Programm das den
Index des Minimums einer nicht-leeren ganzzahligen Liste @{text A}
berechnet.  Der gefundene Index soll in einer Variable
@{text j} gespeichert werden.

Die Notation @{text "A!j"} bezeichnet den Zugriff auf die @{text j}-te
Komponente einer Liste @{text A}.  *}

record list_vars =
  j :: nat

theorem
"|- .{0<length A}.
      program
    .{\<forall>i < length A. A!\<acute>j \<le> A!i}."
  sorry

text {*
 \textbf{Hinweis:} Man beachte, da"s f"ur die Sprache der Zusicherungen
 die volle Ausdrucksst"arke von HOL zur Verf"ugung steht.

 \textbf{Hinweis:} Wird die Einf"uhrung von Hilfsvariablen
 im Programm ben"otigt, m"ussen diese auch im Record der Programm-Variablen
 deklariert werden. *}

subsection {* Die Fibonacci Funktion *}


text {*
 Schreiben Sie ein \texttt{WHILE}-Programm, das die @{text n}-te Fibonacci
 Zahl iterativ berechnet.
 
 Die Spezifikation verwendet dabei eine rekursive Definition der
 Fibonacci Funktion @{text fib}, die Sie in~\cite{Tutorial} finden
 k"onnen.  *}

text {* 
 Ein imperatives Programm zur Berechnung der @{text n}-ten Fibonacci
 Zahl sei wie folgt spezifiziert:
*}

record Fib_vars =
  Fib :: nat

theorem "|- .{0 \<le> n}. program .{\<acute>Fib = fib(n)}."
  sorry

text {*
 \textbf{Hinweis:} Um mit der Multiplikation besser zurecht
 zu kommen, bieten sich u.a.\ folgende Simplifikationsregeln an:
*}

thm add_mult_distrib 
thm add_mult_distrib2

text {*
 Simplifikations-Regeln werden von links nach rechts
 angewendet. Falls Sie die umgekehrte Richtung einer Gleichung 
 verwenden m"ochten, k"onnen Sie diese durch Verkn"upfung mit dem 
 Theorem @{text sym} z. B. folgenderma"sen erhalten: 
*}

thm add_mult_distrib [THEN sym]

text {*
 Setzen Sie f"ur \isa{program} einen geeigneten Text ein und beweisen
 Sie die Behauptung mit Hilfe der Hoare-Logik.  Dabei d"urfen im
 Programm nur die arithmetische Operationen \isa{+} und 
 \isa{-} vorkommen.
*}

subsubsection {* Rekursive Version *}

text {* Definieren Sie einen rekursiven Algorithmus f"ur die Fibonacci
Funktion, die wie die iterative Version auch nur lineare Komplexit"at
hat. Beweisen Sie die G"ultigkeit vom selben Hoare-Triple. *}

(*<*)
end
(*>*)