Differences

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

--- sav08:sign_analysis_of_expressions_and_programs [2008/05/07 01:08]
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 =====
@@ Line 52: / Line 72: @@
 </code>
-Abstract state: map each variable to element of $A$.
+Abstract state: map each variable to element of $A$. Here we have $|A|^3$ possible states.
   * computation over control-flow graph