int x = 0
{ x = 0 }
co x = x + 1 || x = x + 1 oc
{ x = 2 }
This code seems reasonable under some execution assumptions.
x = x + 1 interferes with { x = 0 }:
Establish
{ x = 0 and x = 0 } x = x + 1 { x = 0 }.
which equals
{ x = 0 } x = x + 1 { x = 0 }.
The Assignment Rule gives
{ x = 0 }[ x <- x + 1] x = x + 1 { x = 0 }
which equals
{ x + 1 = 0 } x = x + 1 { x = 0 }
or, with arithmetic
{ x = -1 } x = x + 1 { x = 0 }.
However { x = -1 } does not imply { x = 0 } and
{ x = 0 and x = 0 } x = x + 1 { x = 0 }
cannot be established.
int x = 0 co x = x + 1 || x = x + 1 oc
only one co branch will see x equal to zero.
x equal to one.
{ x = 0 } vs. { x = 0 or x = 1 }.
x is either zero or one for one branch.
{ x = 0 or x = 1 }.
Establish
{ (x0 = 0 or x0 = 1) and x1 = 0 }
x1 = x1 + 1
{ x0 = 0 or x0 = 1 }
The precondition
(x0 = 0 or x0 = 1) and x1 = 0
simplifies to { x = 0 }
By the Assignment rule, the precondition should be
{ x = 0 or x = 1 }[ x <- x + 1 ]
which simplifies to { x = -1 or x = 0 }.
If { x1 = 0 } is true (and it is), then so
is { x = -1 or x = 0}.
{ (x = 0 or x = 1) and x = 0 }
x = x + 1
{ x = 0 or x = 1 }
is established and there's no more interference.
co { P0 } S0 ... || { P1 } S1 ... oc
and S1 interfering with P0, which predicate should you weaken?
P0 in this case).
P1 instead.
{ x >= 0 } y = sqrt(x) { y*y = x }
the precondition can't be weakened any further.
{ x = 0 } x = x + 1 { x = 1 }
is weakened to { x = 0 or x = 1 }, the postcondition is
no longer valid and needs to be
re-established.
int a2b = 0, b2a = 0
while a2b >= 0 and b2a >= 0
co { b2a >= 0 } a2b = f(b2a) { ... }
|| { a2b >= 0 } b2a = g(a2b) { ... } oc
Arguments to f() and g() must be non-negative.
{ b2a >= 0 and a2b >= 0 } b2a = g(a2b) { b2a >= 0 }
nor
{ a2b >= 0 and b2a >= 0 } a2b = g(b2a) { a2b >= 0 }
holds.
int old_a2b = 0, old_b2a = 0
while old_a2b >= 0 and old_b2a >= 0
int new_a2b, new_b2a
co { old_b2a >= 0 } new_a2b = f(old_b2a) ...
|| { old_a2b >= 0 } new_b2a = g(old_a2b) ...
oc
old_b2a = new_b2a
old_a2b = new_a2b
{ I and L }.
I is the global invariant.
L is a local assertion.
int cnt = 0
co . . . { I and cnt = 3 } . . .
|| . . . { I and cnt = 3 } . . .
oc
co . . . { I } cnt++ . . .
|| . . . { I and cnt = 3 } . . .
oc
co . . . { I and cnt = 3 } cnt++
|| . . . { I } . . .
oc
{ x = y } x++ { x = y + 1 } y++ { x = y }
and thread t2 executes y = -y.
{ x = y + 1 }. But,
{ x = y + 1 } if it can't
execute between x++ and y++.
{ x = y + 1 } at other times, but
who cares?
{ x = y + 1 } only; t2 may interfere with
other predicates in t1, with { x = y }, for example.
{ x = y }.
x++ interferes with { x = y }, but
y++ un-interferes with { x = y }.
x++ and y++, { x = y
} is maintained.
S1, S2, ..., Sn
then no other thread executes from the time t starts executing
S1 until t finishes executing Sn.
<> enclose statements executed atomically.
< S1 ; S2 ; ... ; Sn >
< co [ i = 1 to n ] f(i) >
{ x = X and y = Y } < x++
{ x = X + 1 and y = Y }
y++ > { x = X + 1 and y = Y + 1 }
y = -y doesn't interfere with { x = y + 1 } in
< x++ { x = y + 1 } y++ >
< x++ ; y++ > doesn't interfere with { x = y }.
{ x = X and y = Y }
< x++ ; y++ >
{ x = X + 1 and y = Y + 1 }
interferes with { x <= 0 }.
This page last modified on 11 June 2003.