1: \subsection{Describing Boolean Shape Analysis Constraints}
2: \label{sec:bsac}
3:
4: \begin{figure}
5: \begin{equation*}
6: \begin{array}{rcl}
7: F & ::= & \curlyb{C} \mid \curlyb{\curlyb{C_1' \land C_2 \land R}}
8: \mid F_1 \land F_2 \mid \lnot F \mnl
9: C & ::= & A \mid C_1 \land C_2 \mid \lnot C \mnl
10: R & ::= & f \mid \lnot f \mid R_1 \lor R_2 \mnl
11: A & - & \mbox{atomic unary predicate} \mnl
12: f & - & \mbox{atomic binary predicate}
13: \end{array}
14: \end{equation*}
15: \caption{Boolean Shape Analysis Constraints expressed as a sublogic of
16: $\RLtwo$\label{fig:bsacSyntax}}
17: \end{figure}
18:
19: Boolean Shape Analysis Constraints
20: \cite{KuncakRinard03OnBooleanAlgebraShapeAnalysisConstraints}
21: are a natural language for describing dataflow facts of
22: shape analyses \cite{SagivETAL02Parametric}.
23:
24: Figure~\ref{fig:bsacSyntax} presents the syntax of Boolean
25: Shape Analysis Constraints as a subset of role logic. This
26: presentation of Boolean Shape Analysis Constraints shows
27: that they are a subset of the decidable fragment $\RLtwo$ of
28: role logic. In fact, Boolean Shape Analysis Constraints do
29: not use counting quantifiers, so they are already
30: expressible in the two-variable predicate logic $L^2$
31: (without counting).
32:
33: % The reduction from $\RLtwo$ to $C^2$ in
34: % Section~\ref{sec:decidable} followed by the decision method
35: % for $C^2$
36: % \cite{GraedelETAL97TwoVariableLogicCountingDecidable,
37: % PacholskiETAL00ComplexityResultsFirstOrderTwo} generalizes
38: % some of the results of
39: % \cite{KuncakRinard03OnBooleanAlgebraShapeAnalysisConstraints}.
40: % The decidability of $C^2$ itself can be given in the
41: % framework of
42: % \cite{KuncakRinard03OnBooleanAlgebraShapeAnalysisConstraints},
43: % \cite[Appendix A]{Kuncak01DesigningRoleAnalysis},
44: % \cite{Calvanese96UnrestrictedFiniteModelReasoning} and will
45: % be the subject of a forthcoming study.
46:
47: % To use $\RLtwo$ to describe complex properties, we propose
48: % factoring out subformulas that fall out of $\RLtwo$ fragment
49: % into defined predicates. We may then transform the
50: % resulting formula to normal form using the techniques behind
51: % the decidability of $C^2$, treating defined predicates as
52: % relations of the vocabulary. To check the satisfiability of
53: % normal forms, we may use specialized, potentially
54: % incomplete, proof procedures that take into account the
55: % definitions of defined predicates. If the defined
56: % predicates are expressed in terms of relations that form a
57: % tree, we may use MSOL over trees
58: % \cite{Thomas97LanguagesAutomataLogic, ComonETAL97Tata,
59: % KlarlundSchwartzbach93GraphTypes, Moeller01PALE} to check
60: % the decidability of properties involving reachability.
61:
62: \paragraph{A note on usability of role logic.} An anecdotal
63: evidence of the usability of role logic is the fact that all
64: results of
65: \cite{KuncakRinard03OnBooleanAlgebraShapeAnalysisConstraints}
66: were initially shown using role logic notation and then
67: translated into the standard first-order logic notation. We
68: have found the variable-free aspect of role logic convenient
69: when showing the results of
70: \cite{KuncakRinard03OnBooleanAlgebraShapeAnalysisConstraints}.
71: We have subsequently discovered the connection of role
72: logic with $C^2$
73: \cite{GraedelETAL97TwoVariableLogicCountingDecidable}, presented
74: in Section~\ref{sec:decidable}, and the connection with
75: description logics \cite{BaaderETAL03DescriptionLogicHandbook}, presented
76: in Section~\ref{sec:dlencoding}.
77:
78: %%% Local Variables:
79: %%% mode: latex
80: %%% TeX-master: "main"
81: %%% End:
82: