equal
deleted
inserted
replaced
778 @{prop "aval a s = v \<Longrightarrow> aval_rel a s v"} and thus |
778 @{prop "aval a s = v \<Longrightarrow> aval_rel a s v"} and thus |
779 \noquotes{@{prop [source] "aval_rel a s v \<longleftrightarrow> aval a s = v"}}. |
779 \noquotes{@{prop [source] "aval_rel a s v \<longleftrightarrow> aval a s = v"}}. |
780 \end{exercise} |
780 \end{exercise} |
781 |
781 |
782 \begin{exercise} |
782 \begin{exercise} |
783 Consider the stack machine from \autoref{sec:aexp_comp}. |
783 Consider the stack machine from Chapter~3 |
784 A \concept{stack underflow} occurs when executing an instruction |
784 and recall the concept of \concept{stack underflow} |
785 on a stack containing too few values, e.g., executing an @{text ADD} |
785 from Exercise~\ref{exe:stack-underflow}. |
786 instruction on a stack of size less than two. Define an inductive predicate |
786 Define an inductive predicate |
787 @{text "ok :: nat \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> bool"} |
787 @{text "ok :: nat \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> bool"} |
788 such that @{text "ok n is n'"} means that with any initial stack of length |
788 such that @{text "ok n is n'"} means that with any initial stack of length |
789 @{text n} the instructions @{text "is"} can be executed |
789 @{text n} the instructions @{text "is"} can be executed |
790 without stack underflow and that the final stack has length @{text n'}. |
790 without stack underflow and that the final stack has length @{text n'}. |
791 Prove that @{text ok} correctly computes the final stack size |
791 Prove that @{text ok} correctly computes the final stack size |