# Changeset 1772 for Deliverables

Ignore:
Timestamp:
Feb 27, 2012, 3:46:05 PM (8 years ago)
Message:

...

File:
1 edited

Unmodified
Removed
• ## Deliverables/D1.2/CompilerProofOutline/outline.tex

 r1771 \begin{displaymath} \begin{array}{rcl} \mathtt{Call(M(args), dst)}                        & \longrightarrow & \mathtt{SP = alloc}, regs = \emptyset[- := params] \\ \mathtt{PUSH(current\_frame[PC := after\_return])} &                 & \mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst) \mathtt{Call(M(args), dst)}                        & \longrightarrow & \mathtt{SP = alloc,\ regs = \emptyset[- := params]} \\ \mathtt{PUSH(current\_frame[PC := after\_return])} &                 & \mathtt{State(regs,\ sp,\ pc_\emptyset,\ dst)} \end{array} \end{displaymath} \begin{displaymath} \begin{array}{rcl} \mathtt{sp = alloc}, regs = \emptyset[- := PARAMS] & \longrightarrow & \mathtt{free(sp)} \\ \mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)     &                 & \mathtt{Return(M(ret\_val), dst, Frames)} \mathtt{sp = alloc,\ regs = \emptyset[- := PARAMS]} & \longrightarrow & \mathtt{free(sp)} \\ \mathtt{State(regs,\ sp,\ pc_\emptyset,\ dst)}     &                 & \mathtt{Return(M(ret\_val), dst, Frames)} \end{array} \end{displaymath}
Note: See TracChangeset for help on using the changeset viewer.