Changeset 3131


Ignore:
Timestamp:
Apr 12, 2013, 6:10:36 PM (4 years ago)
Author:
campbell
Message:

Add rest of correctness.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.4/Report/report.tex

    r3128 r3131  
    304304to \textsf{Clight} programs.
    305305
    306 TODO: rest of correctness; discuss full functional correctness
     306There is a second part to the statement, which says that the initial
     307processing of the input program to produce the cost labelled version
     308does not affect the semantics of the program:
     309% Yes, I'm paraphrasing the result a tiny bit to remove the observe non-function
     310\begin{lstlisting}[language=matita]
     311  $\forall$input_program,output.
     312  compile input_program = return output $\rightarrow$
     313  not_wrong … (exec_inf … clight_fullexec input_program) $\rightarrow$
     314  sim_with_labels
     315   (exec_inf … clight_fullexec input_program)
     316   (exec_inf … clight_fullexec (c_labelled_clight … output))
     317\end{lstlisting}
     318That is, any successful compilation produces a labelled program that
     319has identical behaviour to the original, so long as there is no
     320`undefined behaviour'.
     321
     322Note that this provides full functional correctness, including
     323preservation of (non-)termination.  The intensional result above does
     324not do this directly --- it does not guarantee the same result or same
     325termination.  There are two mitigating factors, however: first, to
     326prove the intensional property you need local simulation results that
     327can be pieced together to form full behavioural equivalence, only time
     328constraints have prevented us from doing so.  Second, if we wish to
     329confirm a result, termination, or non-termination we could add an
     330observable witness, such as a function that is only called if the
     331correct result is given.  The intensional result guarantees that the
     332observable witness is preserved, so the program must behave correctly.
    307333
    308334\section{Intermediate goals for the front-end}
     
    374400  subtrace.
    375401\item An additional property about the structured trace that no
    376   `program counter' is repeated between cost labels.  Together with
     402  `program counter' is \textbf{repeated} between cost labels.  Together with
    377403  the structure in the trace, this takes over from showing that
    378404  cost labelling is sound and precise.
    379 \item A proof that the observables have been preserved.
    380 \item A proof that the stack limit is still observed by the prefix and
     405\item A proof that the \textbf{observables} have been preserved.
     406\item A proof that the \textbf{stack limit} is still observed by the prefix and
    381407  the structure trace.  (This is largely a consequence of the
    382408  preservation of observables.)
Note: See TracChangeset for help on using the changeset viewer.