Information Technology Reference
In-Depth Information
-
σ
(
Types
Σ
)=
Types
Σ
-
σ
(
FSym
Σ
)
FSym
Σ
where for any arity countably infinite additional func-
tion symbols exist (analogously for predicates and logic variables)
-
σ
(
Π
Σ
)
⊆
⊆
Π
Σ
An important property of signature extensions is the following:
Lemma 1.
Let
Σ
⊇
Σ
denote a signature extension in the sense of Def. 5.
If a
DPL
-formula
φ
over
Σ
has a counter example, i.e., a
DPL
-Kripke structure
K
Σ
,
s
∈S
Σ
with
K
,s
|
=
φ
then
σ
(
K
,s
)
|
=
φ
. In words, signature extensions are
counter example preserving.
Finally, we define the notion of an
anonymizing update
. The motivation behind
anonymizing updates is to erase knowledge about the values of the fields included
in the set
mod
of locations that can be modified by a program. This is achieved
by assigning fresh constant or function symbols to those locations. For example,
the anonymizing update for the modifier set
mod
Σ
=
j
:=
c
j
where
c
i
,c
j
are constants freshly introduced in the extended signature
Σ
.
{
i, j
}
is
i
:=
c
i
||
Definition 6 (Anonymizing Update).
Let
mod
denote a set of terms built
from location symbols in
Σ
.An
anonymizing update for
mod
is an update
V
mod
over an extended signature
Σ
assigning each location
l
(
t
1
,...,t
n
)
∈
mod
aterm
f
l
(
t
1
,...,t
n
)
where
f
l
∈
Σ
\
Σ
.
3.2 Sequent Calculus
DPL
The calculus for reasoning in
is a
sequent calculus
. A sequent is an expres-
sion of the form
Γ
=
-formulas. We call
Γ
the
antecedent
and
Δ
the
succedent
of the sequent. A sequent has the same meaning
as the formula
⇒
Δ
with
Γ, Δ
being sets of
DPL
φ
→
ψ.
φ
∈
Γ
ψ
∈
Δ
Sequent rules
have the general form
s
1
···
s
n
name
s
where
s, s
1
,...,s
n
aresequents.Thesequentsabovethelinearetherule's
premises
while sequent
s
is called the rule's
conclusion
. A sequent without any
premises is an
axiom
.
A
sequent proof
is a tree whose nodes are labelled with sequents and with a
sequent whose validity is to be proven at its root. This
proof tree
is constructed
by applying sequent rules
r
to leaf nodes
n
whose sequent matches the conclusion
r
. The premises of
r
are then added as children of
n
. A branch of a proof tree is
closed
iff it contains an application of an axiom. A proof tree is closed iff all its
branches are closed.
