Changeset 1018


Ignore:
Timestamp:
Jun 21, 2011, 11:21:51 AM (8 years ago)
Author:
mulligan
Message:

tidying

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r1017 r1018  
    315315\end{lstlisting}
    316316Now, it's possible to define what a `good policy' is for a program \texttt{p}.
    317 A policy \texttt{pol} is deemed good when it prevents \texttt{sigma\_safe} from failing on \texttt{p}. Failure is only possible when the policy prescribes
    318 short/middle jumps to too far locations or when the prouced object code does
    319 not fit in code memory. A \texttt{policy} for a program \texttt{p}
    320 is a policy that is good for \texttt{p}.
    321 \begin{lstlisting}
    322 definition policy_ok := $\lambda$pol.$\lambda$p. sigma_safe p $\neq$ None $\ldots$.
    323 definition policy ≝ λp. $\Sigma$jump_expansion:policy_type. policy_ok jump_expansion p.
    324 \end{lstlisting}
    325 Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters that takes in input a good policy and thus never fails. Note how
    326 we avoid failure here and in most of the remaining functions by restricting
    327 the domain using the dependent type \texttt{policy}.
     317A policy \texttt{pol} is deemed good when it prevents \texttt{sigma\_safe} from failing on \texttt{p}.
     318Failure is only possible when the policy dictates that short or medium jumps be expanded to jumps to locations too far away, or when the produced object code does not fit into code memory.
     319A \texttt{policy} for a program \texttt{p} is a policy that is good for \texttt{p}:
     320\begin{lstlisting}
     321definition policy_ok := $\lambda$pol.$\lambda$p. sigma_safe p $\neq$ None $\ldots$
     322definition policy := $\lambda$p. $\Sigma$jump_expansion: policy_type. policy_ok jump_expansion p
     323\end{lstlisting}
     324Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters that takes in input a good policy and thus never fails.
     325Note how we avoid failure here, and in most of the remaining functions, by restricting the domain using the dependent type \texttt{policy}:
    328326\begin{lstlisting}
    329327definition sigma: $\forall$p. policy p $\rightarrow$ Word $\rightarrow$ Word := $\ldots$
Note: See TracChangeset for help on using the changeset viewer.