Formalised Execution
Reduction semantics:
(TH,H,S,R,i;I) ?(TH,H',S',R',I')
Rules depend upon i:
- i=add r1,r2; R'=R{r1:=R(r1)+R(r2)}
- i=mov r1,[r2+n]; R'=R{r1:=wn}; l=R(r2); H(l)=<w0,…,wm> 0<=n<=m
- i=mov [r1+n],r2; l=R(r1); H(l)=<w0,…,wm> 0<=n<=m; H'=H{l:=<w0,…,wm>[n:=R(r2)]}