Path-Aware Static Program Analyses for Specification Mining* - Mining Software Specifications: Methodologies and Applications - page 323

where the consequent defines a judgment whose validity depends upon the
satisfiability of the constraints defined by the antecedent. The constraints
impose restrictions on the structure of the specication map , a map that
identifies a set of preconditions with every program point.
A precondition of an expression e denes an action or predicate that must
hold prior to e's execution. Our analysis tracks a number of such actions;
these actions are defined with respect to the abstract values computed for
each expression in the program by the flow analysis. Thus, an action of the
formread(`; v) asserts that a reference created at label ` holding the abstract
value v is read;write(`; v) asserts a similar condition for reference assignment;
andalloc(`; v) holds if in an expression ref (z) ` 2 P and F(z) = v. In the
same vein,bind(x; v) is true whenever variable x is bound to e ` and F(`) is
v, andcbind(x; v) is used to express predicates that reect if-splitting of ow
values across conditionals; nally,call(` 1 ` 2 ) is used to capture control-
ow precedence relationships among procedure calls { it holds whenever a
procedure with label ` 2 is invoked after an invocation of a procedure with
label ` 1 , with no intervening invocation of any other procedure.
The rules for expressions that bind constants and primitive operations are
straightforward. The preconditions of the expression in the let -body within
which the binding occurs include the preconditions of the let expression,
as well as a precondition that reflects the existence of the new binding. If a
variable is bound in a let -expression to the result of a call to a primitive
operation, the preconditions of the expression in the let -body must include
this action; the values of the arguments to the primitive are approximated by
the abstract values of the operation's arguments as determined by the ow
analysis.
A reference binding induces a precondition on the let -body that includes
both the binding as well as a predicate that captures the reference creation.
Since references are first-class, a variable occurrence may be bound to many
different references during its lifetime. In an expression of the form,
( let x = deref (y) ` 1 in e ` ) ` 0
consider the set of references that y may be bound to (defined by F(y)). Each
element in this set contains a label ` corresponding to a reference expression
ref (z) found in the program. The precondition for e ` must therefore include
predicates that reflect the potential read of each such location, and predicates
that reflect the binding of x to the contents of these locations. Assignment
expressions are defined similarly, with write predicates replacing reads as a
consequence of the operation. The preconditions following a conditional in-
clude the intersection of the specification sets of the two branches; within
these branches, an action that reflects the value of the Boolean guard is in-
cluded as part of the precondition associated with the respective branches.
We now describe the rules dealing with procedure abstraction and call. The
precondition associated with the procedure body is defined as the intersection
of a collection of sets, each of which represents the specifications extant at a