T (true) or F (false), or
==, !=, <=, odd(), ... over
state, or
P1 and P2, P1 or
P2, P1 imp P2, or not P, where P, P1, and
P2 are predicates, or
forall i : P1 : P2, where P1 and
P2 are predicates, or
forsome i : P1 : P2, where P1 and
P2 are predicates.
i < 10, a[i] <= a[i + 1], divides(i, j).
T and T = T | T or T = T | ||
T and F = F | T or F = T | ||
F and T = F | F or T = T | ||
F and F = F | F or F = F |
T imp T = T | not T = F | ||
T imp F = F | not F = T | ||
F imp T = T | | ||
F imp F = T | |
imp, also ->, also =>) is similar to if-then.
P1 imp P2' is equal to not P1 or P2.
forall i : P1 : P2; is
true when
every value of i that makesP1 true also makesP2 true.
P1 and P2 are usually functions if the index i.
forall i, j : 0 <= i <= j < v.size() : v[i] <= v[j]
P1 is never true?
P1 also satisfies P2.
forall i : P1 : P2
is identical to
forall i : true : P1 imp P2
forsome i : P1 : P2 is
true when
there is some value ofithat makes bothP1 andP2 true.
P1 and P2 are usually functions if the index i.
forsome i : 0 <= i < v.size() : v[i] == x
P(si).
P(si) is either true or false.
P defines a set of state instances { si such that
P(si) is true }.
P1 is weaker than a state predicate P2 if the
set associated with P1 is larger than the set associated with P2.
P1 is stronger than a state predicate P2 if
the set associated with P1 is smaller than the set associated with P2.
P1 is weaker than P2, then P2 is stronger than P1.
{ pre } S { post }, where
pre and post are state predicates.
s is a statement.
{ pre } S { post } holds if
preis true, and
sexecutes to completion, and
postis true.
{ pre } S { post }, what happens if pre is false?
s is undefined.
s should only execute when pre is true.
s never terminates?
s is undefined.
{ pre } P(...) { post }.
pre is known as P()'s precondition.
pre is true before calling.
P()'s behavior is undefined if pre is false.
post is known as P()'s post-condition.
P() will ensure that post is true when it returns to the caller.
P() terminates (partial correctness.
true.
(i > -1 and a[i] = x) or <br>
(i = -1 and forall j : 0 < j < |a| : a[j] != x)
{ pre } x = e { post }.
post to be true after x = e executes.
x = e replaces the old value of x with e.
x in post with e;post[x <- e] .
post[ x <- e ] is true{ post[ x <- e ] } x = e { post }x = 3;(x = 3)[x <- x + 1].
(x = 3)[x <- x + 1] simplifies tox + 1 = 3 simplifies to x = 2.
{ x = 2 } x = x + 1 { x = 3 }
{ pre1 } S1 { post1 }{ pre2 } S2 { post2 }S1 ; S2?
S1 ; S2 is clear.
pre1.
S1 ; S2 is clear.
post2.
S1 and S2?
post1 is true after S1 is done.
pre2 must be true before S2 starts.
post1 equal pre2.
{ pre } if B then S { post }.
pre and B is true true before S executes.
post must be true after S executes.
S does not execute, then pre and not B must be true.
post to be true, it must be that pre and not B imp post.
{ pre and B } S { post } holdspre and not B imp post is true{ pre } if B then S { post } holds too.
{ pre } while B do S { post }.
S never executes.
pre must equal post.
not B must be true.
S executes, pre and B must be true.
S executes, pre must be true.
{ pre and B } S { pre } holds{ pre } while B do S { pre and not B } holds too.
x > 0 vs. x > 0 and odd(x).
P1 imp P2P1 is stronger than P2.
P1 imp P2 is true { P2 } S { post } holds{ P1 } S { post } holds too.
mammal(p) vs. human(p).
P1 imp P2P2 is weaker than P1.
P1 imp P2 is true { pre } S { P1 } holds{ pre } S { P2 } holds too.
This page last modified on 7 August 2003.