Changeset 393

Dec 8, 2010, 6:08:05 PM (11 years ago)

A few more details in D3.1.

3 edited


  • C-semantics/

    r392 r393  
    1053 ntheorem exec_inf_sound:
     1053ntheorem exec_inf_equivalence:
    10541054  ∀classic:(∀P:Prop.P ∨ ¬P).
    10551055  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
  • Deliverables/D3.1/Report/report.tex

    r381 r393  
    580580The definition also incorporates errors, and uses a coercion to automatically
    581581transform values from the plain error monad.
    582 \todo{should perhaps give more details of the resumption monad?}
     583The definition of the monad is:
     586ninductive IO (output:Type) (input:output $\rightarrow$ Type) (T:Type) : Type :=
     587| Interact : $\forall$o:output. (input o $\rightarrow$ IO output input T) $\rightarrow$ IO output input T
     588| Value : T $\rightarrow$ IO output input T
     589| Wrong : IO output input T.
     591nlet rec bindIO (O:Type) (I:O $\rightarrow$ Type) (T,T':Type) (v:IO O I T) (f:T $\rightarrow$ IO O I T') on v : IO O I T' :=
     592match v with
     593[ Interact out k $\Rightarrow$ (Interact ??? out ($\lambda$res. bindIO O I T T' (k res) f))
     594| Value v' $\Rightarrow$ (f v')
     595| Wrong $\Rightarrow$ Wrong O I T'
     599Note that the type of the input value is dependent on the output value.
     600This enables us to ensure that the input is always well-typed.  An
     601alternative approach is a check in the semantics, but this causes
     602programs to fail in a way that has no counterpart in the inductive
    584605The execution of assignments is straightforward,
    716 \begin{quote}
    717737We then show the completeness theorems, such as
    719740ntheorem step_complete: $\forall$ge,s,tr,s'.
    723744by case analysis on the inductive derivation and a mixture of
    724745reduction and rewriting.
    725 \todo{Whole execution equivalence}
     747Showing the equivalence of whole program execution is a little
     748trickier.  Our executable semantics produces a coinductive
     749\lstinline'execution' which is really a tree of executions, branching
     750at each I/O resumption on the input value:
     754However, the inductive semantics divides program behaviours into four
     755categories which have \emph{individual} (co)inductive descriptions:
     757\item successfully terminating executions;
     758\item programs which eventually diverge (with an empty trace);
     759\item programs which keep interacting in some way (with an infinite
     760  trace\footnote{In our setting this includes passing through cost
     761    labels as well as I/O.}; and
     762\item programs which \emph{go wrong}.
     765We cannot constructively decide which of these categories an execution
     766can fit into because the properties they describe are undecidable.
     767Hence we follow CompCert's approach for showing that one of the
     768behaviours always exists using classical logic.  Thus we characterise
     769the executions, then show the existence of the inductive semantics'
     770behaviour that matches.  We limit the scope of classical reasoning by
     771taking the relevant axioms as hypotheses:
     774ntheorem exec_inf_equivalence:
     775  $\forall$classic:($\forall$P:Prop.P $\vee$ $\neg$P).
     776  $\forall$constructive_indefinite_description:($\forall$A:Type. $\forall$P:A$\rightarrow$Prop. ($\exists$x. P x) $\rightarrow$ $\Sigma$x : A. P x).
     777  $\forall$p. $\exists$b.execution_matches_behavior (exec_inf p) b $\wedge$ exec_program p b.
    727781\subsection{Animation of simple C programs}
Note: See TracChangeset for help on using the changeset viewer.