{ pre } S { post } means
If the state predicate pre is true
and S executes to termination
then the state predicate post is true.
{ x = 2 } x = x + 1 { x = 3 }
pre is not true and S executes, the results are undefined.
post may be true or false.
{ post } can be established given the
{ pre } and the predicate rule for S.
{ x = 2 }, you can get { x + 1 = 2 + 1 = 3 }.
{ x + 1 = 3 } is identical to { x = 3}[ x <- x + 1 ].
{ x = 2 } x = x + 1 { x = 3
} is valid.
If the precondition is true
and every state predicate along the way is valid
then the postcondition will be true when execution ends.
swap(x, y)
{ x = X and y = Y }
t = x
{ x = X and y = Y and t = X }
x = y
{ x = Y and y = Y and t = X }
y = t
{ x = Y and y = X and t = X }
{ x = Y and y = X }
{ pre } S { post } again.
pre most be true before S starts executing.
pre is true, there's nothing to worry about. Right?
int x = 0 co x = x + 1 || x = 1 oc
|
int x = 0
{ x = 0 }
co
{ x = 0 }
x = x + 1
{ x = 1 }
||
{ x = 0 }
x = 1
{ x = 1 }
oc
{ x = 1 }
|
x = 2 is a possible result of executing the co statement.
Given
co { x = 0 } x = x + 1 { x = 1 }
|| { x = 0 } x = 1 { x = 1 }
oc
executing the statement x = 1
invalidates the predicate { x = 0 }.
S interferes with a predicate { P } when
executing S makes P evaluate to false.
x = 1 does not interfere with { y = 3 }.
S does not interfere with a predicate P if
executing S does not change the value of P.
{ pre } S { post }
and the property P, then S interferes with P if the
if the triple
{ pre and P } S { P }
is not valid.
{ pre and P } S { P } is valid, then S does not interfere
with P.
co { x = 0 } x = x + 1 { x = 1 }
|| { x = 0 } x = 1 { x = 1 }
oc
does x = 1 interfere with { x = 0 }?
x = 1 is { x = 0 }.
{ x = 0 and x = 0 } x = 1 { x = 0 } valid?
{ x = 0 and x = 0 } to { x = 0 }.
{ x = 0 } x = 1 { x = 0 } valid?
{ x = 0 }[ x <- 1] x = 1 { x = 0 } from the predicate rule for
assignment.
{ x = 0 }[ x <- 1] is identical to { 1 = 0 }, which is
identical to false.
{ false } x = 1 { x = 0 } can never establish { x = 0 }.
x = 1 interferes with { x = 0 }.
x = x + 1 interfere with { x = 0 }?
co { P0 } S0 ; . . . ; { Pm } Sm { Pm + 1 }
|| { Q0 } R0 ; . . . ; { Qn } Rn { Qn + 1 }
oc
how much interference analysis do you have to do, in the worst case?
int x = 0, y = 0
co int i = 2 { x = 0 and i = 2 } i++ ...
|| int i = 2 { y = 0 and i = 2 } y = y + i ...
oc
the statement i++ does not interfere with any predicate in the other
branch of the co statement.
i is local, and so distinct from all the others.
co int i0 = 2 { x = 0 and i0 = 2 } i0++ ...
|| int i1 = 2 { y = 0 and i1 = 2 } y = y + i1 ...
oc
make all variables as local as possible.
| ok: |
int i proc f() co i = ... // i = ... oc
|
| better: |
proc f() int i co i = ... // i = ... oc |
| best: |
proc f() co int i ; i = ... // int i ; i = ... oc |
This page last modified on 11 June 2003.