Information Technology Reference
In-Depth Information
the integration. In Sect. 4 we introduce a version of a program specialization
operator that is suitable for logic-based verification and we extend the symbolic
execution calculus with sound rules that permit intermittent partial evaluation.
In Sect. 5 we show the context in which the resulting calculus is applied, and
in Sect. 6 we evaluate the integrated system using formal verification tasks for
anumberof
Java
programs. This is followed by a discussion of related work
(Sect. 7). We stress that the particular combination of symbolic execution and
partial evaluation explored in the present paper is by far not the only possible
one. We sketch further possibilities in the final section on future work.
2 Background
2.1 A Simple Programming Language
The object-oriented programming language
PL
described in this section is basi-
cally a simplified
variant and closely related to the language defined in [4].
We briefly sketch the differences to
Java
Java
:
Unsupported Features.
Multi-threading, graphics, dynamic class loading, generic
types or floating point datatypes are
not
supported by
nor by the actual
implementation in the KeY tool. Formal specification and verification of these
features is a topic of ongoing research, therefore, left out completely.
PL
Restricted Features.
For ease of presentation
PL
imposes some additional re-
strictions compared to
. The KeY tool and the prototype implementation
of our ideas evaluated in Sect. 6 do not impose these restrictions, but model and
respect the
Java
Java
semantics faithfully. The following restrictions apply to PL:
Inheritance and Polymorphism.
For the sake of a simple semantics for dynamic
dispatch of method invocations
PL
abstains from
Java
-like interfaces and method
overloading. Likewise, with exception of the
Null
type, the type hierarchy induced
by user-defined class types has a tree structure with class
Object
as root.
Prohibiting method overloading allows to identify a method within a class unam-
biguously by its name and number of parameters. We allow polymorphism (i.e.
methods can be overwritten in subclasses) but require that their signature must
be exactly the same, otherwise it is a compile-time error.
Visibility.
All classes, methods and fields are publicly visible. This restriction con-
tributes also to a simpler dynamic dispatch semantics.
No Exceptions.
PL
has no support for exceptions. Instead of runtime exceptions like
NullPointerException
s the program will simply not terminate in these cases.
No class/object Initialization.
In
Java
the first active usage of a type or creation
of a new instance triggers complex initialization.
PL
supports only instance cre-
ation, but does not initialize fields upon creation. In particular,
PL
does not sup-
port static or instance initializers. Constructors are also missing in
PL
,anew
instance is simply created by the expression
new
T
().
Primitive Types.
Only
boolean
and
int
are available. To keep the semantics of
standard arithmetic operators simple,
int
is an unlimited datatype representing
the whole numbers
Z
rather than a finite datatype with overflow.
