added exercise
Mon, 21 Oct 2013 21:06:19 +0200
changeset 54186 ea92cce67f09
parent 54185 3fe3b5d33e41
child 54187 80259d79a81e
added exercise
--- 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.
+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 "?"}.