Information Technology Reference
In-Depth Information
val
K,s,β
(
f
(
t
1
,...,t
n
)) =
I
(
f
)(
val
K,s,β
(
t
1
)
,...,val
K,s,β
(
t
1
))
val
K,s,β
(
q
(
t
1
,...,t
n
)) =
tt
iff (
val
K,s,β
(
t
1
)
,...,val
K,s,β
(
t
1
))
∈ I
(
q
)
val
K,s,β
(
φ ∧ ψ
)=
tt,
if
val
K,s,β
(
φ
)=
tt
and
val
K,s,β
(
φ
)=
tt
ff , otherwise.
...
val
K,s,β
([
s
](
φ
)) =
val
K,s
,β
(
φ
)
,
if
∃ s ∈S
such that
ρ
(
p
)(
s, s
)
tt,
otherwise
Fig. 4.
Definition (excerpt) of evaluation function
val
reasons we do not give a formal semantics of updates and refer to [3] for details
on updates. Instead we explain the meaning intuitively along some examples:
-
Elementary updates
i
:=
j
have exactly the same meaning as assignments:
in a
DPL
-Kripke structure
K
and state
s
, an update application
{
i
:=
j
}
ξ
,s
where
s
is identical to
s
except at
i
which is evaluated to
val
K,s,β
(
j
)in
s
.
-
Parallel updates
u
1
||
on a term/formula
ξ
yields the same value as if evaluating
ξ
in
K
u
2
are evaluated simultaneously and do not interfere
with each other. Content swapping of two program variables can thus be
expressed by
i
:=
j
||
j
:=
i
.
-
Quantified updates
for
Tx
;
φ
;
u
allow to update arbitrarily many locations
simultaneously. The update “
for int
i
;
i
i<a.length
;
a
[
i
] := 0”, for
example, assigns all array components the value 0.
-
In case of parallel and quantified updates conflicts may arise when the same
location is assigned different values as in
i
:=
0
≥
0
∧
i
:=
1
. Conflict resolution
for parallel updates utilizes a last-wins semantics where the previous update
is equivalent to
i
:=
1
. Conflict resolution for quantified updates requires
a well-founded order on
T
and the update with the smallest value for the
quantified variable wins [3].
||
To summarize, updates are similar to explicit substitutions and allow to express
state changes concisely at the syntactic level.
Definition 4 (Satisfiability and Validity).
ADPL-formula
φ
is
-
satisfiable
iff there exists a
DPL
-Kripke structure
K
=(
D, I,
S
,ρ
)
,astate
s
∈S
and a variable assignment
β
such that
val
D,I,s,β
(
φ
)=
tt
(or in short:
=
φ
);
-
valid in a
K
,s,β
|
DPL
-Kripke structure
K
(we also say that
K
is a
model
for
φ
and
write
K|
=
φ
) iff for all states
s
∈S
and variable assignments
β
we have
=
φ
;
-
logically valid
iff all
K
,s,β
|
DPL
-Kripke structures
K
are models for
φ
.
We introduce two notions which we will need later on. For technical reasons we
must have the possibility to extend a logic's signature.
Definition 5 (Signature Extension).
Let
Σ,Σ
denote two signatures.
Σ
is
called a
signature extension
of
Σ
if there is an embedding
σ
(
Σ
)
Σ
that is
⊂
unique up to isomorphism and enjoys the following properties:
