# HG changeset patch
# User nipkow
# Date 1382382379 -7200
# Node ID ea92cce67f09cb03a4185aee09027ae154cc141c
# Parent  3fe3b5d33e41877029f6016406ffb31b78a69183
added exercise

diff -r 3fe3b5d33e41 -r ea92cce67f09 src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Mon Oct 21 10:49:02 2013 +0200
+++ b/src/Doc/ProgProve/Logic.thy	Mon Oct 21 21:06:19 2013 +0200
@@ -764,6 +764,26 @@
 conditions}. In rule inductions, these side-conditions appear as additional
 assumptions. The \isacom{for} clause seen in the definition of the reflexive
 transitive closure merely simplifies the form of the induction rule.
+
+\ifsem
+\subsection{Exercises}
+
+\begin{exercise}
+Consider the stack machine from \autoref{sec:aexp_comp}.
+A \concept{stack underflow} occurs when executing an instruction
+on a stack containing too few values, e.g., executing an @{text ADD}
+instruction on a stack of size less than two. Define an inductive predicate
+@{text "ok :: nat \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> bool"}
+such that @{text "ok n is n'"} means that with any initial stack of length
+@{text n} the instructions @{text "is"} can be executed
+without stack underflow and that the final stack has length @{text n'}.
+Prove that @{text ok} correctly computes the final stack size
+@{prop[display] "\<lbrakk>ok n is n'; length stk = n\<rbrakk> \<Longrightarrow> length (exec is s stk) = n'"}
+and that instruction sequences generated by @{text comp}
+cannot cause stack underflow: \ @{text "ok n (comp a) ?"} \ for
+some suitable value of @{text "?"}.
+\end{exercise}
+\fi
 *}
 (*<*)
 end