As promised here is the completed source code for an initial version of the
stack machine we started implementing in class. The plan is to now write a
compiler from aexp to sinstr programs. Then we’ll verify the compiler to be
correct.
Fixpoint s_execute (st : state) (stack : list nat)
(prog : list sinstr)
: list nat :=
match prog with
| SPush n :: p' => s_execute st (n::stack) p'
| SLoad s :: p' => s_execute st ((st s)::stack) p'
| SPlus :: p' => match stack with
| a1 :: a2 :: stack' => s_execute st ((a1+a2)::stack') p'
| _ => s_execute st stack p'
end
| SMinus :: p' => match stack with
| a1 :: a2 :: stack' =>
s_execute st ((if (a1<?a2) then (a2-a1) else 0)::stack') p'
| _ => s_execute st stack p'
end
| SMult :: p' => match stack with
| a1 :: a2 :: stack' => s_execute st ((a1*a2)::stack') p'
| _ => s_execute st stack p'
end
| _ => stack
end.
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *)
Check s_execute.
Example s_execute1 :
s_execute empty_st []
[SPush 5; SPush 3; SPush 1; SMinus]
= [2; 5].
Proof.
reflexivity.
Qed.
(* FILL IN HERE *)
Example s_execute2 :
s_execute (X !-> 3) [3;4]
[SPush 4; SLoad X; SMult; SPlus]
= [15; 4].
Proof.
reflexivity.
Qed.
(* FILL IN HERE *)