Information Technology Reference
In-Depth Information
P
::=
D
∗
D
::=
type
tid |
var
V
:
T
∗
)
returns
(
∗
)
modifies
(
V
∗
)
∗
∗
}
?
|
procedure
pid
(
V
:
T
V
:
T
V
:
T
lid
:
S
{
S
::=
S
;
S |
havoc
V
+
| V
+
:=
E
+
|
call
V
∗
:=
pid
(
E
+
)
|
assume
E |
goto
lid
+
|
return
| R
R
::=
halt
|
abort
|
pick
T
::=
bool
|
int
|
[
T
+
]
T | tid
E
::=
C
E
[
E
+
]
E
[
E
+
:=
E
]
|
V
|
|
|
old
E
+
|
UOp E | E BOp E |
if
E
then
E
else
E | QOp V
:
T
• E
V
::=
vid
C
::=
true
|
false
|
0
|
1
|
2
|···
UOp
::=
−|¬
BOp
::= +
|−|···|< |≤|
=
|···|∧|∨|···
QOp
::=
∃|∀|λ
Fig. 2.
Desugared language supported by Boogaloo, consisting of programs
P
, declarations
D
,
statements
S
, types
T
, and expressions
E
. Angular brackets
are part of the grammar metalan-
guage, used to mark optional (?) or repeated (
∗
, +) expressions.
square brackets denote map applications. Whenever convenient, we see
m
as a set
of (
n
+1)-tuples:
m
m
iff
m
[
d
1
,...,d
n
]=
d
0
. dom(
m
) and rng(
m
) denote the
domain
and
range
of
m
;
m
is
total
if dom(
m
)=
D
1
×···×
⊂
D
1
×···×
D
n
×
D
0
such that (
d
1
,...,d
n
,d
0
)
∈
d
]
denotes a map
m
identical to
m
except that
m
[
d
1
,...,d
n
]=
d
. We overload this no-
tation to denote variable substitution: if
e,y
1
,...,y
n
are expressions, and
x
1
,...,x
n
,
are variable names,
e
[
x
1
,...,x
n
→
D
n
,and
finite
if
|
dom(
m
)
|∈
Z
;
m
[
d
1
,...,d
n
→
y
1
,...y
n
] denotes
e
with all occurrences of
x
k
replaced by
y
k
,for
k
=1
,...,n
.
3.1
Input Language
Boogaloo desugars generic Boogie programs [17] into the simpler language described
in Fig. 2. Programs
P
are lists of declarations
D
, whose order is immaterial. Dec-
larations include uninterpreted
type
s, global
var
iables, and
procedure
s with input
parameters, output parameters (
returns
), global variables the procedure may mod-
ify (
modifies
clause), and body (between braces). Procedure bodies consist of local
variable declarations followed by a list of labeled statements
S
. The latter include se-
quential composition, regular and nondeterministic assignment (:= and
havoc
, possibly
in parallel to multiple variables), procedure
call
,
assume
, nondeterministic
goto
aset
of label identifiers, and abrupt
return
to the caller procedure, as well as
directives
R
described shortly. Expressions must be properly typed as
bool
eans,
int
egers, maps
[
T
1
,...,T
n
]
T
0
from arbitrary domain (
T
1
,...,T
n
) and codomain
T
0
types, and user-
defined uninterpreted types
3
. Expressions
E
include literal constants
C
, variables
V
,
map applications
m
[
t
1
,...,t
n
], map updates
m
[
t
1
,...,t
n
:=
t
],
old
expressions which
refer to the value of an expression when the procedure was entered, plus the usual
applications of unary operators
UOp
, binary operators
BOp
,aternary
if
/
then
/
else
operator, and quantifications and lambda expressions
QOp
.
The
directives
halt
,
abort
,and
pick
are Boogaloo-specific and characterize sym-
bolic executions:
halt
terminates the current execution with success (marking
pass-
3
While Boogaloo supports Boogie's type constructors with arguments, as well type parameters
in procedures and maps, we do not include them in the discussion for simplicity.
