Changeset 393
 Timestamp:
 Dec 8, 2010, 6:08:05 PM (10 years ago)
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/CexecIOcomplete.ma
r392 r393 1051 1051 nqed. 1052 1052 1053 ntheorem exec_inf_ sound:1053 ntheorem exec_inf_equivalence: 1054 1054 ∀classic:(∀P:Prop.P ∨ ¬P). 1055 1055 ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x). 
Deliverables/D3.1/Report/report.tex
r381 r393 580 580 The definition also incorporates errors, and uses a coercion to automatically 581 581 transform values from the plain error monad. 582 \todo{should perhaps give more details of the resumption monad?} 582 583 The definition of the monad is: 584 \begin{quote} 585 \begin{lstlisting} 586 ninductive 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. 590 591 nlet 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' := 592 match 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' 596 ]. 597 \end{lstlisting} 598 \end{quote} 599 Note that the type of the input value is dependent on the output value. 600 This enables us to ensure that the input is always welltyped. An 601 alternative approach is a check in the semantics, but this causes 602 programs to fail in a way that has no counterpart in the inductive 603 semantics. 583 604 584 605 The execution of assignments is straightforward, … … 714 735 \end{lstlisting} 715 736 \end{quote} 716 \begin{quote}717 737 We then show the completeness theorems, such as 738 \begin{quote} 718 739 \begin{lstlisting} 719 740 ntheorem step_complete: $\forall$ge,s,tr,s'. … … 723 744 by case analysis on the inductive derivation and a mixture of 724 745 reduction and rewriting. 725 \todo{Whole execution equivalence} 746 747 Showing the equivalence of whole program execution is a little 748 trickier. Our executable semantics produces a coinductive 749 \lstinline'execution' which is really a tree of executions, branching 750 at each I/O resumption on the input value: 751 \begin{quote} 752 [TODO] 753 \end{quote} 754 However, the inductive semantics divides program behaviours into four 755 categories which have \emph{individual} (co)inductive descriptions: 756 \begin{itemize} 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}. 763 \end{itemize} 764 765 We cannot constructively decide which of these categories an execution 766 can fit into because the properties they describe are undecidable. 767 Hence we follow CompCert's approach for showing that one of the 768 behaviours always exists using classical logic. Thus we characterise 769 the executions, then show the existence of the inductive semantics' 770 behaviour that matches. We limit the scope of classical reasoning by 771 taking the relevant axioms as hypotheses: 772 \begin{quote} 773 \begin{lstlisting} 774 ntheorem 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. 778 \end{lstlisting} 779 \end{quote} 726 780 727 781 \subsection{Animation of simple C programs}
Note: See TracChangeset
for help on using the changeset viewer.