Unification Degrees

Because the domain-specific unification procedure succeeds where the general-purpose procedure may fail, it computes a unification degree that reflects the likelihood that such a domain-specific unification may introduce false positives. The underlying theory is that of fuzzy logic. Fuzzy logic is a logic of quantified truth. Concretely, SOUL associates truth degrees with each result it reports —thus facilitating their assessment. To this end, SOUL features a quantified resolution procedure. For the logic terms and template terms in a specification, the truth degree of a result is bounded respectively by the matching strategy and logic rules used in their resolution. The properties of the result itself further refine this upper bound. Solutions are ranked lower if they required a domain-specific unification that could introduce false positives (due to imprecision in the program analyses the unification relies on). Unification degrees are therefore associated with each domain-specific unification. 

The following table lists some important domain-specific extensions to the general-purpose unification procedure and their unification degrees:

?x unifies with ?y
binding for ?x binding for ?y conditions degree
an ASTNode an ASTNode unify according to general-purpose unification procedure (i.e., the ASTNodes are identical)
 1
a Type a Type according to a semantic analsyis, denote same type or are co-variant return types 1
a MethodInvocation a MethodDeclaration invocation may invoke declaration according to the static type of the receiver or the dynamic type of the objects it may evaluate to 1/4 or 1/2
an Expression an Expression according to an intra-procedural must-alias analysis or according to an inter-procedural may-alias analysis, must or may evaluate to the same object at run- time 9/10 or 1/2

Most notably, expressions unify with a unification degree of 1/2 if they are in a may-alias relation according to an inter-procedural points-to analysis. Unifying such expressions can introduce false positives if the expressions do not evaluate to the same object during all possible program executions. Expressions that reside in the same method unify with a unification degree of 9/10 if they are guaranteed to alias during all executions according to an intra-procedural must-alias analysis. If both expressions are the same AST node, they unify with a complete unification degree.