Java程序辅导

Weakest Precondition Calculus
COMP2600 — Formal Methods for Software Engineering
Rajeev Gore´
Australian National University
Semester 2, 2016
(Most lecture slides due to Ranald Clouston)
COMP 2600 — Weakest Preconditions 1
COMP 2600 — Weakest Preconditions 2
Hoare Logic = Syntax and (Semantics or Calculus)
Syntax Semantics WP Calculus
CPL predicates CPL semantics No ND!
variables x,y,z · · · arith-
metic expressions 1 +
2,x < y, · · · and predi-
cates built from them
states map variables
and expressions to val-
ues and predicates to
true/false
rules of arithmetic e.g
1+2= 3, 22 = 4, 6/3=
2 etc
programming language
:= ; if.then. while
as usual
one rule for each
(seen rule for :=,
;, if.then.else.,
prestr, postwk)
Hoare Triple {P} S {Q}
if pre-state satisfies P
and S terminates then
post-state satisfies Q
proo f s (much harder!)
COMP 2600 — Weakest Preconditions 3
Edsger W. Dijkstra (1930 – 2002)
The originator of this week’s material (in 1976), and a good source of quotes:
Program testing can be quite effective for showing the presence of
bugs, but is hopelessly inadequate for showing their absence.
The question of whether Machines Can Think... [is] about as relevant
as the question of whether Submarines Can Swim.
He also had some pretty uncompromising views on how introductory com-
puter science should be taught:
In order to drive home the message that this introductory program-
ming course is primarily a course in formal mathematics, we see to
it that the programming language in question has not been imple-
mented on campus so that students are protected from the tempta-
tion to test their programs.
COMP 2600 — Weakest Preconditions 4
Introduction
Dijkstra’s Weakest Precondition Calculus is another technique for proving
properties of imperative programs.
Hoare Logic presents logic problems:
• Given a precondition P, code fragment S and postconditionQ, is {P}S{Q}
true?
WP is about evaluating a function:
• Given a code fragment S and postcondition Q, find the unique P which is
the weakest precondition for S and Q.
COMP 2600 — Weakest Preconditions 5
The wp Function
If S is a code fragment and Q is an assertion about states, then the weakest
precondition for S with respect to Q is an assertion that is true for precisely
those initial states from which:
• S must terminate, and
• executing S must produce a state satisfying Q.
That is, the weakest precondition P is a function of S and Q:
P = wp(S,Q)
( wp is sometimes called a predicate transformer, and the Weakest Precon-
dition Calculus is sometimes called Predicate Transformer Semantics. )
COMP 2600 — Weakest Preconditions 6
Relationship with Hoare logic
Hoare Logic is relational:
• For each Q, there are many P such that {P}S{Q}.
• For each P, there are many Q such that {P}S{Q}.
WP is functional:
• For each Q there is exactly one assertion wp(S,Q).
WP does respect Hoare Logic: {wp(S,Q)} S{Q} is true.
COMP 2600 — Weakest Preconditions 7
Relationship with Hoare logic ctd.
Hoare Logic is about partial correctness:
• We don’t care about termination.
WP is about total correctness:
• We do care about termination.
COMP 2600 — Weakest Preconditions 8
A Diagrammatic View of Weakest Preconditions
1
2
3
Qwp(S,Q)
Initial States Final States
Each arc shows the code S acting on a different initial state:
• Arc 1 produces a final state not satisfying Q ×
• Arc 2 produces a final state satisfying Q X
• Arc 3 gets into a loop and produces no final state ×
COMP 2600 — Weakest Preconditions 9
Intuition Example 1
Consider code x:=x+1 and postcondition (x> 0)
One valid precondition is (x> 0), so in Hoare Logic the following is true:
{x> 0} x:=x+1 {x> 0}
Another valid precondition is (x>−1), so:
{x>−1} x:=x+1 {x> 0}
(x>−1) is weaker than (x> 0) (. . . because (x> 0)⇒ (x>−1))
In fact, (x>−1) is the weakest precondition:
wp(x:=x+1, x> 0) ≡ (x>−1)
COMP 2600 — Weakest Preconditions 10
Intuition Example 2
Consider code a:=a+1; b:=b-1 and postcondition a×b= 0
A very strong precondition is (a=−1)∧ (b= 1):
{(a=−1)∧ (b= 1)}a:=a+1; b:=b-1{a×b= 0}
A weaker precondition is a=−1.
The weakest precondition is (a=−1)∨ (b= 1)
wp(a:=a+1; b:=b-1, a×b= 0) ≡ (a=−1)∨ (b= 1)
COMP 2600 — Weakest Preconditions 11
Intuition Example 3
The assignment axiom of Hoare Logic gives us (for any postcondition Q):
{Q(y+ z)} x:= y+z {Q(x)}
Intuitive justification:
• Let v be the value arrived at by computing y+z.
• If Q(y+ z) is true initially, then so is Q(v).
• Since the variable x has value v after the assignment (and nothing else
changes in the state), It must be that Q(x) holds after that assignment.
COMP 2600 — Weakest Preconditions 12
Intuition Example 3 ctd.
In fact Q(y+ z) is the weakest precondition.
Intuitive justification:
• Let v be the value arrived at by computing x:= y+z.
• If Q(x) is true after the assignment, so is Q(v).
• If Q(v) is true after the assignment, then it must also be true before the
assignment, because x does not appear in Q(v) and nothing else has
changed.
• Thus, Q(y+ z) was true initially.
• So (combined with previous slide), Q(x) holds after the assignment if and
only if Q(y+ z) held before it.
COMP 2600 — Weakest Preconditions 13
Weakest Precondition of Assignment (Rule 1/4)
We have argued that the Assignment axiom of Hoare Logic is designed to
give the “best” — i.e. the weakest — precondition:
{Q(e)} x:=e {Q(x)}
Therefore we should expect that the rule for Assignment in the weakest pre-
condition calculus corresponds closely:
wp(x:=e, Q(x)) ≡ Q(e)
COMP 2600 — Weakest Preconditions 14
Assignment Examples
wp(x:=y+3, (x> 3)) ≡ y+3> 3 (substitute y+3 for x)
≡ y> 0 (simplify)
wp(n:=n+1, (n> 5)) ≡ n+1> 5 (substitute n+1 for n)
≡ n> 4 (simplify)
COMP 2600 — Weakest Preconditions 15
Weakest Preconditions for Sequences (Rule 2/4)
As in Hoare Logic, we expect the rule for sequencing to compose the effect
of the consecutive statements. The rule is:
wp(S1;S2, Q) ≡ wp(S1, wp(S2, Q))
Example:
wp(x:=x+2; y:=y-2, (x+ y= 0))
≡ wp(x:=x+2, wp(y:=y-2, (x+ y= 0)))
≡ wp(x:=x+2, (x+(y−2) = 0))
≡ ((x+2)+(y−2) = 0)
≡ (x+ y= 0)
COMP 2600 — Weakest Preconditions 16
Weakest Preconditions for Conditionals (Rule 3a/4)
wp(if b then S1 else S2,Q) ≡ (b⇒wp(S1,Q)) ∧ (¬b⇒wp(S2,Q))
Proof:
By cases on condition b,
• b is true: RHS≡ (True⇒wp(S1,Q)) ∧ (False⇒wp(S2,Q))
wp for the conditional is the weakest precondition for S1 guaranteeing
postcondition Q – that is, LHS is wp(S1,Q).
The right hand side reduces to the same thing if we replace b with True.
• b is false:
Similarly, both left hand and right hand sides reduce to wp(S2,Q)
COMP 2600 — Weakest Preconditions 17
Conditional Example:
wp(if b then S1 else S2,Q) ≡ (b⇒wp(S1,Q)) ∧ (¬b⇒wp(S2,Q))
wp(if x>2 then y:=1 else y:=-1, (y> 0))
≡ ((x> 2)⇒wp(y:=1,(y> 0)) ∧ (¬(x> 2)⇒wp(y:=-1,(y> 0))
≡ ((x> 2)⇒ (1> 0)) ∧ (¬(x> 2)⇒ (−1> 0))
≡ ((x> 2)⇒True) ∧ ((x≤ 2)⇒False)
≡ x> 2
(If you are unhappy with the last step, draw a truth table.)
COMP 2600 — Weakest Preconditions 18
Alternative Rule for Conditionals (Rule 3b/4)
The conditional rule tends to produce complicated logical expressions which
we then have to simplify.
It is often easier to deal with disjunctions and conjunctions than implications,
so the following equivalent rule for conditionals is usually more convenient.
wp(if b then S1 else S2,Q) ≡ (b∧wp(S1,Q)) ∨ (¬b∧wp(S2,Q))
COMP 2600 — Weakest Preconditions 19
Conditional Example Again:
wp(if b then S1 else S2,Q) ≡ (b∧wp(S1,Q)) ∨ (¬b∧wp(S2,Q))
wp(if x>2 then y:=1 else y:=-1, (y> 0))
≡ ((x> 2)∧wp(y:=1,(y> 0)) ∨ (¬(x> 2)∧wp(y:=-1,(y> 0))
≡ ((x> 2)∧ (1> 0)) ∨ (¬(x> 2)∧ (−1> 0))
≡ ((x> 2)∧True) ∨ (¬(x> 2)∧False)
≡ (x> 2) ∨ False
≡ x> 2
(Again, any step you are unhappy with can be confirmed via truth table.)
COMP 2600 — Weakest Preconditions 20
Why The Rules are Equivalent
All that has changed is the form of the proposition. Rather than
(b⇒ p)∧ (¬b⇒q)
we have
(b∧ p)∨ (¬b∧q) :
b p q (b⇒ p) ∧ (¬b⇒q) (b∧ p) ∨ (¬b∧q)
T T T T T T T T F
T T F T T T T T F
T F T F F T F F F
T F F F F T F F F
F T T T T T F T T
F T F T F F F F F
F F T T T T F T T
F F F T F F F F F
COMP 2600 — Weakest Preconditions 21
A Diagrammatic View of Conditionals
wp(if b then S1 else S2,Q)≡ (b⇒wp(S1,Q)) ∧ (¬b⇒wp(S2,Q))
≡ (b∧wp(S1,Q)) ∨ (¬b∧wp(S2,Q))
b ¬b
wp(S1,Q)
wp(S2,Q)
Q
Initial States Final States
COMP 2600 — Weakest Preconditions 22
Conditionals Without ‘Else’
It is sometimes convenient to have conditionals without else, i.e.
if b then S
recalling that this is just a compact way of writing
if b then S else x := x
We can derive wp rules for this case:
wp(if b then S,Q)≡ (b⇒wp(S1,Q)) ∧ (¬b⇒Q)
≡ (b∧wp(S1,Q)) ∨ (¬b∧Q)
COMP 2600 — Weakest Preconditions 23
Loops
(The thing to do now is hang on tightly . . . )
Suppose we have a while loop and some postcondition Q.
The precondition P we seek is the weakest that:
• establishes Q
• guarantees termination
We can take hints for the first requirement from the corresponding rule for
Hoare Logic. That is, think in terms of loop invariants.
But termination is a bigger problem...
COMP 2600 — Weakest Preconditions 24
Summary of Lecture I
Weak and Strong Conditions: P stronger than Q if P⇒Q in first-order logic
Hoare Logic Rules: used this notion in rules precon equivalence, precond
strengthening, postcond equivalence, postcond weakening
wp(S,Q): Given S and Q, the assertion wp(S,Q) is the weakest precondi-
tion that is true for precisely those initial states from which:
• S must terminate, and
• executing S must produce a state satisfying Q
wp(S,Q) : is a function ... so we can give the rules as equations
COMP 2600 — Weakest Preconditions 25