程序代写 SWEN90010 - High Integrity

SWEN90010 – High Integrity
Systems Engineering Hoare Logic

DMD 8.17 (Level 8, Doug McDonell Bldg)
http://people.eng.unimelb.edu.au/tobym @tobycmurray

HOARE LOGIC (PROVING PROGRAMS CORRECT)

If I prove my program is correct, does that guarantee it will have no bugs?
3 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
If I prove my program is correct, does that guarantee it will have no bugs?
Incorrect specification. (you proved the wrong thing)
Program differs from what was proved. (proofs are always over mathematical models)

Misconception
Proving is hard.
(Not if you understand programming carefully.)
4 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Programming Language
5 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

6 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

“main” program:
6 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Proof Structure
Follows the program structure, top-down
To prove something about X,
we reason about X’s internal components.
7 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Hoare Triples
8 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Hoare Triples
precondition
8 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Hoare Triples
precondition
postcondition
8 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Hoare Triples
precondition
{ x = 2 } x := x + 1 { x = 3 }
8 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
postcondition

Hoare Triples
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
precondition
{ x = 2 } x := x + 1 { x = 3 }
postcondition
(strongest postcondition)

Hoare Triples
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
precondition
{ x = 2 } x := x + 1 { x = 3 }
{ x = 0 } x := x + 1 { x = 1 }
postcondition
(strongest postcondition)

Hoare Triples
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
precondition
{ x = 2 } x := x + 1 { x = 3 }
(weakest precondition)
{ x = 0 } x := x + 1 { x = 1 }
postcondition
(strongest postcondition)

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Logic (Refresher)
We use standard propositional symbols:
“not”, “negation”
“and”, “conjunction”
“or”, “disjunction”
if A is true then B is also true A is not true
A is true and B is true
at least one of A or B is true
the proposition that is always true
the proposition that is never true

Inference Rules
Some trivial examples:
modus ponens
A structural rule:
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Assignment Statements
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Assignment Statements
{ x = 2 } x := x + 1 { x = 3 }
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Assignment Statements
{ x = 2 } x := x + 1 { x = 3 }
{ x ≥ 0 } x := x + 1 { x – 1 ≥ 0 }
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Assignment Statements
{ x = 2 } x := x + 1 { x = 3 }
{ x ≥ 0 } x := x + 1 { x – 1 ≥ 0 }
{ x ≥ 0 } x := sha256(x) { ? }
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Assignment Statements
{ x = 2 } x := x + 1 { x = 3 }
{ x ≥ 0 } x := x + 1 { x – 1 ≥ 0 }
{ x ≥ 0 } x := sha256(x) { ? }
{ x = 0 } x := x + 1 { x = 1 }
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Assignment Statements
{ x = 2 } x := x + 1 { x = 3 }
{ x ≥ 0 } x := x + 1 { x – 1 ≥ 0 }
{ x ≥ 0 } x := sha256(x) { ? }
{ x = 0 } x := x + 1 { x = 1 }
{ x + 1 = 1 } x := x + 1 { x = 1 }
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Assignment Statements
{ x = 2 } x := x + 1 { x = 3 }
{ x ≥ 0 } x := x + 1 { x – 1 ≥ 0 }
{ x ≥ 0 } x := sha256(x) { ? }
{ x = 0 } x := x + 1 { x = 1 }
{ x + 1 = 1 } x := x + 1 { x = 1 }
{ x + 1 ≥ 0 } x := x + 1 { x ≥ 0 }
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Assignment Statements
{ x = 2 } x := x + 1 { x = 3 }
{ x ≥ 0 } x := x + 1 { x – 1 ≥ 0 }
{ x ≥ 0 } x := sha256(x) { ? }
{ x = 0 } x := x + 1 { x = 1 }
{ x + 1 = 1 } x := x + 1 { x = 1 }
{ x + 1 ≥ 0 } x := x + 1 { x ≥ 0 }
{ sha256(x) ≥ 0 } x := sha256(x) { x ≥ 0 }
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Assignment
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Assignment
{ (x = 1)[x + 1/x] } x := x + 1 { x = 1 }
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Assignment
{ (x = 1)[x + 1/x] } x := x + 1 { x = 1 } { x + 1 = 1 } x := x + 1 { x = 1 }
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Assignment
{ (x = 1)[x + 1/x] } x := x + 1 { x = 1 } { x + 1 = 1 } x := x + 1 { x = 1 } { x = 0 } x := x + 1 { x = 1 }
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Assignment
{ (x = 1)[x + 1/x] } x := x + 1 { x = 1 } { x + 1 = 1 } x := x + 1 { x = 1 } { x = 0 } x := x + 1 { x = 1 }
{ (x ≥ 0)[x + 1/x] } x := x + 1 { x ≥ 0 }
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Assignment
{ (x = 1)[x + 1/x] } x := x + 1 { x = 1 } { x + 1 = 1 } x := x + 1 { x = 1 } { x = 0 } x := x + 1 { x = 1 }
{ (x ≥ 0)[x + 1/x] } x := x + 1 { x ≥ 0 } { x + 1 ≥ 0 } x := x + 1 { x ≥ 0 }
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Consequence
13 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Consequence
{ x = 0 } x := x + 1 { x = 1 }
13 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Consequence
{ x = 0 } x := x + 1 { x = 1 } { x = 0 } x := x + 1 { x > 0 }
13 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Consequence
{ x = 0 } x := x + 1 { x = 1 } { x = 0 } x := x + 1 { x > 0 }
{ x ≥ 0 } x := x + 1 { x > 0 }
13 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Consequence
{ x = 0 } x := x + 1 { x = 1 } { x = 0 } x := x + 1 { x > 0 }
{ x ≥ 0 } x := x + 1 { x > 0 } { x = 0 } x := x + 1 { x > 0 }
13 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Combining the Two Rules
Assignment axiom Consequence rule
14 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Combining the Two Rules
Assignment axiom Consequence rule
Suppose we wish to prove:
14 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Combining the Two Rules
Assignment axiom Consequence rule
Suppose we wish to prove:
{ x = 0 } x := x + 1 { x > 0 }
14 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Combining the Two Rules
Assignment axiom Consequence rule
Apply consequence rule first
Suppose we wish to prove:
{ x = 0 } x := x + 1 { x > 0 }
14 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Combining the Two Rules
Assignment axiom Consequence rule
{ x = 0 } x := x + 1 { x > 0 }
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Combining the Two Rules
Assignment axiom Consequence rule
{ ?P } x := x + 1 { x > 0 }
{ x = 0 } x := x + 1 { x > 0 }
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Combining the Two Rules
Assignment axiom Consequence rule
x = 0 ⇒ ?P { ?P } x := x + 1 { x > 0 }
{ x = 0 } x := x + 1 { x > 0 }
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Combining the Two Rules
Assignment axiom Consequence rule
Now apply the assignment axiom
x = 0 ⇒ ?P { ?P } x := x + 1 { x > 0 }
{ x = 0 } x := x + 1 { x > 0 }
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Combining the Two Rules
Assignment axiom Consequence rule
x = 0 ⇒ x + 1 > 0 { x + 1 > 0 } x := x + 1 { x > 0 }
{ x = 0 } x := x + 1 { x > 0 }
16 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Combining the Two Rules
Assignment axiom Consequence rule
This is a general pattern:
apply consequence rule first to generalise precondition, then apply other rules
x = 0 ⇒ x + 1 > 0 { x + 1 > 0 } x := x + 1 { x > 0 }
{ x = 0 } x := x + 1 { x > 0 }
17 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Assignment Rule as Weakest Precondition Rule
Given some concrete postcondition P,
the assignment rule says how to calculate
the weakest precondition to guarantee P holds afterwards:
The rules we will see for the other kinds of statements (if, while, skip, sequencing etc.) will also be of this form, allowing us to calculate weakest preconditions from
a concrete postcondition.
18 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Weakest Precondition Reasoning
Given concrete preconditions P’ and Q and some program S, to prove:
{P′} S {Q}
19 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Weakest Precondition Reasoning
Given concrete preconditions P’ and Q and some program S, to prove:
{P′} S {Q}
First apply the consequence rule to generalise the
precondition, giving us two goals to prove:
{?P} S {Q}
19 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Weakest Precondition Reasoning
Given concrete preconditions P’ and Q and some program S, to prove:
{P′} S {Q}
First apply the consequence rule to generalise the
precondition, giving us two goals to prove:
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
{?P} S {Q}
Then, calculate what ?P is by applying the weakest precondition rules

Weakest Precondition Reasoning
Given concrete preconditions P’ and Q and some program S, to prove:
{P′} S {Q}
First apply the consequence rule to generalise the
precondition, giving us two goals to prove:
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
{?P} S {Q}
Then, calculate what ?P is by applying the weakest precondition rules
Once ?P has been calculated, finally check this implication holds

NEXT LECTURE BEGINS

Rule of Sequencing
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Sequencing
Theorem: {x = 0} x := x+1; x := x+1 {x=2}
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Sequencing
Theorem: {x = 0} x := x+1; x := x+1 {x=2} Proof:
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Sequencing
Theorem: {x = 0} x := x+1; x := x+1 {x=2} Proof:
{x = 0} x := x+1; x := x+1 {x=2}
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Sequencing
Apply consequence rule first
Theorem: {x = 0} x := x+1; x := x+1 {x=2}
{x = 0} x := x+1; x := x+1 {x=2}
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Sequencing
Apply consequence rule first
Theorem: {x = 0} x := x+1; x := x+1 {x=2} Proof:
{x = 0} x := x+1; x := x+1 {x=2}
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Sequencing
Apply consequence rule first
Theorem: {x = 0} x := x+1; x := x+1 {x=2} Proof:
x = 0 ⇒ ?P {?P} x := x+1; x := x+1 {x=2}
{x = 0} x := x+1; x := x+1 {x=2}
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Sequencing
Theorem: {x = 0} x := x+1; x := x+1 {x=2} Proof:
x = 0 ⇒ ?P {?P} x := x+1; x := x+1 {x=2}
{x = 0} x := x+1; x := x+1 {x=2}
22 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Sequencing
Theorem: {x = 0} x := x+1; x := x+1 {x=2} Proof:
{?P} x := x+1 {?R} {?R} x := x+1 {x=2} x = 0 ⇒ ?P {?P} x := x+1; x := x+1 {x=2}
{x = 0} x := x+1; x := x+1 {x=2}
22 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Sequencing
Theorem: {x = 0} x := x+1; x := x+1 {x=2} Proof:
{?P} x := x+1 {x+1=2} {x+1=2} x := x+1 {x=2} x = 0 ⇒ ?P {?P} x := x+1; x := x+1 {x=2}
{x = 0} x := x+1; x := x+1 {x=2}
23 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rule of Sequencing
Theorem: {x = 0} x := x+1; x := x+1 {x=2} Proof:
{x+2=2} x := x+1 {x+1=2} {x+1=2} x := x+1 {x= x=0 ⇒ x+2=2 {x+2=2} x := x+1; x :=

程序代写 CS代考加微信: powcoder QQ: 1823890830 Email: powcoder@163.com

Related Posts