Information Technology Reference
In-Depth Information
y=80
y=80
y=80
threshold=100
threshold=100
threshold=100
80>100
?
decrease=true decrease=false
decrease=false
decrease=false
|y-100| > eps
?
|y-100| > eps
?
|y-100| > eps
?
decrease
?
decrease
?
y=y-1
y=y+1
y=y-1
y=y+1
y=y+1
•
•
•
•
•
•
Fig. 3.
Partial evaluation example
3 Dynamic Logic with Updates
3.1 Program Logic
As program logic for
PL
we use a sorted first-order dynamic logic instantiated
by a given
PL
program
p
. We define formally the family of first-order dynamic
logics
DPL
used to reason about
PL
programs. Each concrete instance of this
family is associated to exactly one
program which is then referred to as the
context program
or sometimes the
program context
of that logic.
PL
Definition 1 (Signature).
For any
signature
Σ
p
is de-
fined as a tuple
(
Types
,
FSym
,
PSym
,
VSym
)
,where
Types
is a set of sort names
that contains at least
PL
program
p
a
DPL
classes
(
p
)
.Further,
FSym
is a set of function symbols,
PSym
a set of predicate symbols, and
VSym
a
set of logic variable symbols (we omit the subscript
p
in
Σ
p
whenever it can be
unambiguously derived from the context). Function, predicate, and logic variable
symbols have a fixed sorted signature. Sorts are ordered wrt a sort hierarchy
{
,
boolean
,
int
,
Object
,
Null
}∪
.
The order
models
p
's type hierarchy with maximum element
.
We distinguish between
rigid
and
non-rigid
function and predicate symbols.
Intuitively, the semantics of rigid symbols does not depend on the current state of
program execution while non-rigid symbols are state-dependent. (Local) program
variables, arrays, static, and instance fields are modeled as non-rigid function
symbols and together form a separate class of non-rigid symbols called
location
symbols. Specifically, local program variables and static fields are modeled as
non-rigid constants, instance fields as unary non-rigid functions, and array access
as a binary non-rigid function. For example, an instance field
size
of type
int
