Information Technology Reference
In-Depth Information
The rules for quantified expressions are non-deterministic. Consider an expression
Q
=
Q
1
x
1
···
Q
n
x
n
•
q
in prenex normal form, where
n>
0,
Q
k
is one of
∀
∃
and
for all
k
's, and
q
is quantifier-free. Rule
QUANT
-T evaluates
Q
to true and adds it to
the universal constraints
υ
after the following transformation. First,
Q
is Skolemized
as
q
1
,where
y
is the subsequence of
x
1
,...,x
n
including only those
x
k
's for
which
Q
k
is
∀
y
•
E
1
is the environment after Skolemization, which contains fresh logical
variables for the Skolem functions introduced by the process. Evaluating
q
1
in
∀
;
E
1
yields
some
q
2
where the bound variables
y
map to fresh logical variables
; after performing
the substitution
q
=
q
2
[
→
y
],
q
is added to
υ
.Rule
QUANT
-F, which evaluates
∀
y
•
to false, follows by duality (
∀
,and
∃
Q
∃
∀
denotes
denotes
).
Procedure Call Semantics.
The precise semantics of procedure calls involves several
details to support recursion—mainly, maintaining a stack of environments and corre-
spondingly keeping track of scope. We overlook these tedious aspects and focus on the
gist of the semantics of a call to a generic procedure
P
(before desugaring):
?
procedure
P(
a
)
returns
(
o
)
requires
p
ensures
q
modifies
(
m
)
{
B
}
with formal input
a
and output
o
parameters, modified global variables
m
, body
B
,and
pre- and postcondition
p
and
q
. The desugaring of Sec. 3.1 turns pre- and postcondition
into checks at the call site:
assert
p
[
a
→
u
]
;
call
v
:=
P
(
u
)
;
assume
q
[
a
,
o
→
u
,
v
]
;
(For brevity, we do not discuss the handling of
old
expressions in postconditions.) It
also generates a modified procedure body
B
to reflect the implementation or spec-
ification semantics, according to whether
P
has a body or not: if
B
is defined,
B
adds an
assert
q
before each
return
statement in
B
;if
B
is not defined,
B
con-
sists of the single statement
havoc
o
,
m
. The effect of the call statement is then given
by
B
[
a
→
u
]@
entry
where @
entry
denotes the basic block of statements at proce-
dure
P
's entry. Even though Boogaloo defaults to implementation semantics whenever
a body is available, one can always switch to the specification semantics for a particular
procedure by commenting out its body.
Operational Semantics.
Fig. 4 describes the operational semantics of statements other
than procedure calls, using the notation
E−
S
E
to denote that executing statement
E
. Rules are applicable only if
τ
=
S
changes the environment
,thatisif
the computation has not terminated yet; after rules
HALT
or
ABORT
have changed
τ
to
passing
E
into
✧
no rule is applicable and hence the computation terminates.
Rules
SEQ
for sequential composition,
GOTO
for branch, and
RETURN
for abrupt
termination are standard, using the notation @
caller
to denote the basic block beginning
after the current call in the caller procedure. Rule
GOTO
is clearly nondeterministic.
Rule
ASSUME
adds the assumed Boolean formula to the set
κ
of state constraints.
Rule
HAVOC
“forgets” the symbolic value of the variable
v
, as if uninitialized. Rule
ASS
updates the symbolic value in
σ
associated to the assigned variable
v
.
The most interesting rule is
PICK
, which details how
pick
concretizes symbolic
states. It extends
κ
into
κ
, adding map instance constraints
κ
μ
=
✓
or failing
✗
{
m
[
x
]=
y
|
