Changeset 3427 for Papers/fopara2013/fopara13.tex

Timestamp:

Feb 11, 2014, 6:41:19 PM (7 years ago)

Author:

campbell

Message:

Make example clearer for readers in black and white.

File:

• Papers/fopara2013/fopara13.tex (modified) (1 diff)

Papers/fopara2013/fopara13.tex

@@ -435 +435 @@
 \label{test1}
 \end{figure}
-We illustrate the workflow we envisage (on the right of~\autoref{test1})
-on an example program (on the left of~\autoref{test1}).
-The user writes the program and feeds it to the CerCo compiler, which outputs
-an instrumented version of the same program that updates global variables
-that record the elapsed execution time and the stack space usage.
-The red lines in \autoref{itest1} are the instrumentation introduced by the
-compiler. The annotated program can then be enriched with complexity assertions 
-in the style of Hoare logic, that are passed to a deductive platform (in our 
-case Frama-C). We provide as a Frama-C cost plugin a simple automatic 
-synthesiser for complexity assertions (the blue lines in \autoref{itest1}), 
-which can be overridden by the user to increase or decrease accuracy. From the 
-assertions, a general purpose deductive platform produces proof obligations 
-which in turn can be closed by automatic or interactive provers, ending in a 
-proof certificate.
+We illustrate the workflow we envisage (on the right
+of~\autoref{test1}) on an example program (on the left
+of~\autoref{test1}).  The user writes the program and feeds it to the
+CerCo compiler, which outputs an instrumented version of the same
+program that updates global variables that record the elapsed
+execution time and the stack space usage.  The red lines in
+\autoref{itest1} introducing variables, functions and function calls
+starting \lstinline'__cost' and \lstinline'__stack' are the instrumentation introduced by the
+compiler.
+
+ The annotated program can then be enriched with complexity
+assertions in the style of Hoare logic, that are passed to a deductive
+platform (in our case Frama-C). We provide as a Frama-C cost plugin a
+simple automatic synthesiser for complexity assertions (the blue
+comments starting with \lstinline'/*@' in \autoref{itest1}), which can
+be overridden by the user to increase or decrease accuracy. From the
+assertions, a general purpose deductive platform produces proof
+obligations which in turn can be closed by automatic or interactive
+provers, ending in a proof certificate.
 
 % NB: if you try this example with the live CD you should increase the timeout