Information Technology Reference
In-Depth Information
required is to check whether a given atomic formula has a positive or negative
polarity
within
'
, where the polarity of a sub-formula
p
is determined according
to whether the number of negations enclosing
is even (positive polarity) or odd
(negative polarity). Additional considerations apply to sub-formulas involving
the
if-then-else
construct.
p
Example 2.
Let us illustrate these concepts on program DEC whose validity we
wish to check.
Since our main algorithm checks for satisability, we proceed by calculating
the polarity of each comparison in
:'
:
(FB
0
c
=FB
c
)
(N
0
c
=FB
c
)
(N
0
c
=
(ZN
0
c
=N
c
)
A
=
=
1
−
f
;
;
v
)
;
;
(
v
1
−
=
v
2
−
)
g
(N
0
c
6
=FB
c
)
(N
0
c
6
(ZN
0
c
6
=N
c
g
A
6
=
=
f
;
=
v
2
−
)
;
For example, the comparison (N
0
c
=
v
1
−
'
is contained within one negation
(implied by appearing on the left hand side of the implication). Since we are
considering
)in
, this amounts to 2 negations, and since 2 is even, we add (N
0
c
=
:'
v
1
−
)to
A
=
.
This example would require a state-space in the order of 10
5
if we used the full
[1
] range. The range allocation algorithm of [17] will nd ranges adequate for
this formula, with a state space of 32.
::n
n
0
c
fb
0
c
zn
0
c
fb
c
v
2
−
v
1
−
Fig. 5.
The Graph
G
:
G
6
=
[ G
=
representing
:'
5.4
A Graph-Theoretic Representation
The sets
A
6
=
and
A
=
can be represented by two graphs,
G
=
and
G
6
=
dened as
follows:
(
x
i
;x
j
)isanedgeon
G
=
,the
equalities graph
,i(
x
i
=
x
j
)
2A
=
.
(
x
i
;x
j
)isanedgeon
G
6
=
,the
inequalities graph
,i(
x
i
6
=
x
j
)
2A
6
=
.
We refer to the joint graph as
G
.
An inconsistent subset
B A
will appear, graphically, as a cycle consisting
of a single
G
6
=
-edge and any positive number of
G
=
-edges. We refer to these
cycle as
contradictory cycles.
Search WWH ::
Custom Search