Differences

This shows you the differences between two versions of the page.

--- sav08:sign_analysis_of_expressions_and_programs [2008/05/07 00:17]
vkuncak
+++ sav08:sign_analysis_of_expressions_and_programs [2008/05/07 23:18]
giuliano
@@ Line 1: / Line 1: @@
 ====== Sign Analysis of Expressions and Programs ======
 ===== Sign Analysis of Expressions =====
@@ Line 32: / Line 33: @@
 Abstract domain: $A = \{ neg, nul, pos, \top \}$
-Abstract operations: $\oplus, \otimes : A^2 \to A$ defined by tables:
+Abstract operations: $\oplus, \otimes : A^2 \to A$ defined by tables:\\
+\\
+$\begin{tabular}{ |c |c |c |c |c |c |}
+\hline \oplus & neg & nul & pos & \top \\
+\hline  neg & neg & neg & \top & \top \\
+\hline  nul & neg & nul & pos & \top \\
+\hline pos & \top & pos & pos & \top \\
+\hline \top & \top & \top & \top & \top \\ \hline
+\end{tabular}
+$\\
+\\
+$\begin{tabular}{ |c |c |c |c |c |c |}
+\hline \otimes & neg & nul & pos & \top \\
+\hline  neg & pos & nul & neg & \top \\
+\hline  nul & nul & nul & nul & nul \\
+\hline pos & neg & nul & pos & \top \\
+\hline \top & \top & nul & \top & \top \\ \hline
+\end{tabular}
+$
+===== Sign Analysis of Programs =====
+Prove that this program never reports error:
+<code>
+i = 20;
+x = 2;
+while (i > 0) {
+  x = x + 4;
+  i = i - 1;
+}
+if (x==0) {
+  error;
+} else {
+  y = 1000/x;
+}
+</code>
+Abstract state: map each variable to element of $A$. Here we have $|A|^3$ possible states.
+  * computation over control-flow graph
+What does it mean for such computation to be correct?