Information Technology Reference
In-Depth Information
program
p
is a non-empty set of class declarations with at least one class
of name
Object
. The class hierarchy is a tree with class
Object
as root. A class
Cl
:= (
cname, scname
opt
,fld,mtd
) consists of (i) a classname
cname
unique in
p
, (ii) the name of its superclass
scname
(only omitted for
cname
=
Object
),
and (iii) a list of field
fld
and method
mtd
declarations.
The syntax for class declaration is the same as in
A
PL
. The only lacking
features are constructors and static/instance initialization blocks.
Java
knows
also the special reference type
Null
which is a singleton with
null
as the only
element. It may be used in place of any reference type and is the only type that
is a subtype of all class types.
To keep examples short we agree on the following convention: if not explicitly
stated otherwise, any given sequence of statements is seen as if it would be the
body of a static, void method declared in a class
Default
with no fields declared.
The syntax of the executable fragment needed for the purpose of this paper
as follows:
PL
Statements
stmnt
::=
stmnt stmnt
|
|
|
|
lvarDecl
locExp
'='
exp
';'
cond
loop
loop
::=
while '('
exp
')' '{'
stmnt
'}'
lvarDecl
::=
Type
IDENT ( '='
exp
)
opt
';'
cond
::=
if '('
exp
')' '{'
stmnt
'}' else '{'
stmnt
'}'
Expressions
exp
::=
(
exp
.)
opt
mthdCall
locExp
mthdCall
::=
mthdName'('
exp
opt
(','
exp
)
∗
')'
opExp
::=
f
(
exp
opt
(,
exp
)
∗
)
|
opExp
|
|
Z
|
TRUE
|
FALSE
|
null
f
::=
!
|
|
|
|
|
|
|
|
|
|
|
|
|
-
<
<=
>=
>
==
&
|
*
/
%
+
-
Locations
locExp
::=
IDENT
|
exp
.IDENT
Dynamic dispatch works in
as follows: we need to determine the implemen-
tation of a method on encountering a method invocation such as
o.m(a)
.Todo
so, first look up the dynamic type
T
of the object referenced by
o
.Thenscanall
classes between
T
and the static type of
o
for an implementation of a method
named
m
and the correct number of parameters. The first match is taken.
PL
2.2 Symbolic Execution
Symbolic execution is an idea from the 1960s [1], but it has only recently been
realized eciently for industrially relevant programming languages. Symbolic
execution is a central, very versatile program analysis technique that is used for
formal program verification [3,5,6], extended static checking and verification [7],
debugging [8], and automatic test case generation [9,10].
In the last decade a number of ecient symbolic execution engines for real
heap-based programming and intermediate languages were created including
KeY (for
, see [11]), Bogor/Kiasan (for
BIR, see [12]), Pex (for MSIL, see [9]), and VeriFast (for C,
Java
,C,Creol,see[3]),KIV(for
Java
Java
,see[13]).
