header {* Hoare Logik *};

(*<*) theory Aufgabe = 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} 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://www4.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
text {*\subsection*{Arrays}*}
text {*
  In dieser {\"U}bung werden wir Hoare-Logik verwenden, um die partielle Korrektheit imperativer Programme, die auf Arrays 
  arbeiten, zu beweisen. Arrays werden in Isabelle als Listen modelliert. Der Operator @{text "!"} kann verwendet werden,
  um einzelne Elemente einer Liste {\"u}ber ihren Index zu selektieren, z.B.: *}

lemma "[a,b,c,d] ! 2 = c"
by simp

text {*
  Der folgende Algorithmus implementiert serielle Suche in einem Array: *}
     
types val = nat
record vars =
  i :: nat
  v :: val
  A :: "val list"

lemma SerialSearch:"\<turnstile> 
  \<lbrace>length \<acute>A = n \<and> \<acute>A = I\<rbrace> 
  \<acute>i := 0; 
  WHILE \<acute>i < n \<and> \<acute>A ! \<acute>i \<noteq> \<acute>v 
    INV \<lbrace>\<acute>A = I \<and> length \<acute>A = n\<rbrace> 
    DO 
    \<acute>i := \<acute>i + 1 
    OD
  \<lbrace>length \<acute>A = n \<and> \<acute>A = I \<and> (n \<le> \<acute>i \<or> \<acute>A ! \<acute>i = \<acute>v)\<rbrace>"
oops

text {*
\begin{itemize}
\item Beweisen Sie die Unterziele, die bei diesem Hoare-Tripel auftreten.
\item F{\"u}gen Sie der Nachbedingung die Aussage \mbox{@{text "(\<acute>v \<in> set \<acute>A \<longrightarrow> \<acute>A ! \<acute>i = \<acute>v)"}} hinzu.
  Beweisen Sie die Unterziele dieses neuen Hoare-Tripels.\\
  Hinweis: Sie werden auch die Schleifeninvariante {\"a}ndern m{\"u}ssen.

\item Beweisen Sie jetzt das entsprechende Hoare-Tripel f{\"u}r serielle Suche in einer sortierten Liste:
  \begin{itemize}                                                                                        
    \item Nehmen Sie an, daß das gegebene Array sortiert ist.
    \item {\"A}ndern Sie die Vorbedingung entsprechend.
    \item {\"A}ndern Sie die Schleifenbedingung, um  durch Ausn{\"u}tzen der Tatsache, daß die Liste sortiert ist,
  m{\"o}glicherweise die Laufzeit des Algorithmus zu verk{\"u}rzen.
    \item Beweisen Sie \mbox{@{text "(\<acute>v \<in> set \<acute>A \<longrightarrow> \<acute>A ! \<acute>i = \<acute>v)"}} als eine Nachbedingung.
  \end{itemize}                                                                                        
Hinweise: 
  \begin{itemize}
    \item Definieren Sie eine Funktion @{text "sorted: val list \<Rightarrow> bool"}, die {\"u}berpr{\"u}ft, ob eine Liste sortiert ist.
    \item Machen Sie sich mit den Funktionen @{term "take"} und @{term "drop"} in der Isabelle Listen-Bibliothek vertraut.
  \end{itemize}

\end{itemize}                                                                                                                          
*}

(*<*) end (*>*)