Information Technology Reference
In-Depth Information
constraints: (
a,a
[
i
]
>i
) and (
b,j
=0=
⇒
b
[
i,j
]=1); whereas
∀
i,j
•
i<j
=
⇒
c
[
i
]
<c
[
j
] determines: (
a,
c
[
i
]
<c
[
j
]).
Boogaloo evaluates parametrized constraints for a given map store
μ
iteratively: pick
an element
p
=(
m,
e
,s
) of
μ
, instantiate all parametrized constraints for
m
with
e
and evaluate them, and mark
p
; repeat until all elements of
μ
are marked. If a
Q
in a
parametrized constraint (
m,Q
) contains quantifiers, instantiating
m
triggers the gener-
ation of new parametrized constraints from
Q
.
Since evaluating a parametrized constraint may add new points to
μ
, termination
of the evaluation procedure is not guaranteed in the presence of recursive formulas,
which determine constraints (
m,Q
(
y
,m
[
y
])) where
Q
also contains applications of
m
to elements other than
y
. For example, an axiomatization of the factorial
f
as
f
[0] = 1
and
∀
j
•
i<j
=
⇒
∀
i
•
i>
0=
⇒
f
[
i
]=
i
·
f
[
i
−
1] determines the constraint
q
=(
f,i >
0=
⇒
f
[
i
]=
i
1]).If
μ
[
f
]=(
0
,
1
), evaluating
q
for
i
=
0
introduces a new
map application at
0
−
·
f
[
i
−
2, and so on.
Boogaloo evaluates such recursive constraints using fair unrolling similarly to [24],
based on the notion of guard: a parametrized constraint is
guarded
if has the form
(
m,G
(
y
)=
1, which then introduces an application at
0
−
B
(
y
)). When Boogaloo's iterative evaluation picks an element
p
=
(
m,
e
,s
), it nondeterministically chooses a subset
D
of all guarded constraints for
m
and “disables” them in the evaluation determined by
p
: for a parametrized constraint
q
=(
m,G
=
⇒
B
otherwise.
For the “right” selection of
D
, recursive definitions are disabled, so that they do not
add new points to
μ
and evaluation terminates. In the factorial example, there are two
choices for
f
[
0
]: disabling or enabling the guarded constraint. Disabling it terminates
the finitization process, producing an execution with
0
=0; enabling the guarded
constraints produces one iteration (for
f
[
0
−
⇒
B
), it evaluates the constraint
¬
G
if
q
∈
D
,and
G
∧
1]), which in turn recursively leads to the
same two choices, and so on. Unlike [24], which works only with function definitions
and thus assumes that guards are mutually exclusive and cover all cases, Boogaloo's
fair enumeration applies to guards of any form and constraints other than equality; it
also provides an option to limit the number of unrollings, because recursive constraints
may be not well-founded (a sufficient condition for termination).
Nondeterminism.
There are four sources of nondeterminism in Boogaloo semantics:
evaluation of quantified expressions,
goto
s, and
pick
—involving the disabling of
guarded constraints in
Φ
and constraint solving to select a solution
Λ
. Boogaloo enumer-
ates nondeterministic choices using backtracking monads (e.g. [9]). The command-line
interface currently offers depth-first and fair exploration strategies, but the implementa-
tion easily accommodate others parametrically.
When executing
goto
statements, the order in which labels are tried may affect
progress: if the first chosen label leads back to the same statement, execution gets stuck
in a loop. To avoid this situation, Boogaloo keeps track of how often each label was
taken along the current execution path, and always tries labels in ascending order of
their frequencies (least frequent first). This strategy also has the nice effect of enumer-
ating shorter executions before longer ones in the long run. A similar strategy applies
to disabling parametrized constraints.
Since symbolic computation is speculative, it introduces the risk that long computa-
tions are constructed only to realize, when solving the symbolic constraints, that they
