Changeset 1792 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 28, 2012, 5:56:20 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1791 r1792 522 522 \begin{displaymath} 523 523 \begin{array}{rll} 524 \mathtt{State } & ::= & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\524 \mathtt{StateRTLabs} & ::= & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\ 525 525 & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\ 526 526 & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem} … … 536 536 537 537 \begin{displaymath} 538 \mathtt{State } ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}538 \mathtt{StateRTL} ::= (\mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}) \times \mathtt{Mem} 539 539 \end{displaymath} 540 540 The internal stack pointer \texttt{ISP}, and its relationship with the stack pointer \texttt{SP}, needs some comment. … … 550 550 Because $\sigma$ is onetomany and, morally, a multivalued function, we use in the sequel the functional notation for $\sigma$, using $\star$ as a distinct marker in the range of $\sigma$ to mean that any value is accepted. 551 551 \begin{displaymath} 552 \mathtt{State } \stackrel{\sigma}{\longrightarrow} \mathtt{State}552 \mathtt{StateRTLabs} \stackrel{\sigma}{\longrightarrow} \mathtt{StateRTL}s 553 553 \end{displaymath} 554 554 … … 607 607 \begin{displaymath} 608 608 \begin{array}{rcl} 609 \mathtt{CALL(id,\ args,\ dst,\ pc) \in State(Frame^*, Frame)} & \longrightarrow & \mathtt{ Call(M(args), dst)}, \\610 & & \mathtt{PUSH(Frame[pc := after\_return])}609 \mathtt{CALL(id,\ args,\ dst,\ pc) \in State(Frame^*, Frame)} & \longrightarrow & \mathtt{PUSH(Frame[pc := after\_return])}, \\ 610 & & \mathtt{Call(M(args), dst)} 611 611 \end{array} 612 612 \end{displaymath} … … 619 619 \begin{displaymath} 620 620 \begin{array}{rcl} 621 \mathtt{ Call(M(args), dst)},& \stackrel{\mathtt{ret\_val = f(M(args))}}{\longrightarrow} & \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} \\622 \mathtt{ PUSH(Frame[pc := after\_return])}& &621 \mathtt{PUSH(Frame[pc := after\_return])}, & \stackrel{\mathtt{ret\_val = f(M(args))}}{\longrightarrow} & \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} \\ 622 \mathtt{Call(M(args), dst)} & & 623 623 \end{array} 624 624 \end{displaymath} … … 705 705 Note, in particular, that this final act of pushing a frame on the stack leaves us in an identical state to the RTLabs case, where the instruction 706 706 \begin{displaymath} 707 \mathtt{PUSH( current\_frame[pc := after\_return])}707 \mathtt{PUSH(Frame[pc := after\_return])} 708 708 \end{displaymath} 709 709 was executed.
Note: See TracChangeset
for help on using the changeset viewer.