Changeset 3131
 Timestamp:
 Apr 12, 2013, 6:10:36 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.4/Report/report.tex
r3128 r3131 304 304 to \textsf{Clight} programs. 305 305 306 TODO: rest of correctness; discuss full functional correctness 306 There is a second part to the statement, which says that the initial 307 processing of the input program to produce the cost labelled version 308 does not affect the semantics of the program: 309 % Yes, I'm paraphrasing the result a tiny bit to remove the observe nonfunction 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} 318 That is, any successful compilation produces a labelled program that 319 has identical behaviour to the original, so long as there is no 320 `undefined behaviour'. 321 322 Note that this provides full functional correctness, including 323 preservation of (non)termination. The intensional result above does 324 not do this directly  it does not guarantee the same result or same 325 termination. There are two mitigating factors, however: first, to 326 prove the intensional property you need local simulation results that 327 can be pieced together to form full behavioural equivalence, only time 328 constraints have prevented us from doing so. Second, if we wish to 329 confirm a result, termination, or nontermination we could add an 330 observable witness, such as a function that is only called if the 331 correct result is given. The intensional result guarantees that the 332 observable witness is preserved, so the program must behave correctly. 307 333 308 334 \section{Intermediate goals for the frontend} … … 374 400 subtrace. 375 401 \item An additional property about the structured trace that no 376 `program counter' is repeatedbetween cost labels. Together with402 `program counter' is \textbf{repeated} between cost labels. Together with 377 403 the structure in the trace, this takes over from showing that 378 404 cost labelling is sound and precise. 379 \item A proof that the observableshave been preserved.380 \item A proof that the stack limitis still observed by the prefix and405 \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 381 407 the structure trace. (This is largely a consequence of the 382 408 preservation of observables.)
Note: See TracChangeset
for help on using the changeset viewer.