more exercises
Sat, 26 Oct 2013 23:06:40 +0200
changeset 54210 9d239afc1a90
parent 54209 16723c834406
child 54211 2c024c23d67f
child 54212 5f1e2017eeea
more exercises
--- a/src/Doc/ProgProve/Logic.thy	Sat Oct 26 13:01:41 2013 +0200
+++ b/src/Doc/ProgProve/Logic.thy	Sat Oct 26 23:06:40 2013 +0200
@@ -780,10 +780,10 @@
-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
+Consider the stack machine from Chapter~3
+and recall the concept of \concept{stack underflow}
+from Exercise~\ref{exe:stack-underflow}.
+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