留学生作业代写 SWEN90010 - High Integrity

SWEN90010 – High Integrity
Systems Engineering Invariants
Toby MD 8.17 (Level 8, Doug McDonell Bldg)
http://people.eng.unimelb.edu.au/tobym @tobycmurray

INVARIANTS

While Loop Rule
P is called an invariant
3 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

While Loop Rule
P is called an invariant Must satisfy 3 properties:
3 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

While Loop Rule
P is called an invariant Must satisfy 3 properties:
1. Holds when the loop is encountered
3 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

While Loop Rule
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
P is called an invariant Must satisfy 3 properties:
1. Holds when the loop is encountered 2. Holds after each loop iteration

While Loop Rule
P is called an invariant Must satisfy 3 properties:
1. Holds when the loop is encountered
2. Holds after each loop iteration
3. Implies the postcondition when the guard is false
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
result = 0; while a > 0 do
result = result + B;
a = a – 1;
What does this program compute?

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
result = 0; while a > 0 do
result = result + B;
a = a – 1;
What does this program compute?
result = A * B;

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
result = 0; while a > 0 do
result = result + B;
a = a – 1;
{result = A * B}

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
result = 0; while a > 0 do
result = result + B;
a = a – 1;
{result = A * B} Let’s prove this

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
a = A; {?P1} result = 0; {?I}
(By sequence and consequence rules)
while a > 0 do result = result + B; a = a – 1;
{result = A * B}

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
a = A; {?P1} result = 0; {?I}
while a > 0 do {?I ∧ a > 0}
result = result + B; a = a – 1;
{?I ∧ a ≤ 0} {result = A * B}
(By iteration/while loop rule)

Choosing an Invariant
Invariant P must satisfy 3 properties:
1. Holds when the loop is encountered 2. Holds after each loop iteration
3. Implies the postcondition when the guard is false
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Choosing an Invariant
Invariant P must satisfy 3 properties:
1. Holds when the loop is encountered 2. Holds after each loop iteration
3. Implies the postcondition when the guard is false Usually must talk about the variables modified in the loop
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Choosing an Invariant
Invariant P must satisfy 3 properties:
1. Holds when the loop is encountered 2. Holds after each loop iteration
3. Implies the postcondition when the guard is false
Usually must talk about the variables modified in the loop
Usually must talk about things in the postcondition
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Iter a result
result = 0; while a > 0 do
result = result + B;
a = a – 1;
Copyright University of Melbourne 2016, provided under Creative
A -1 A -2 A -3
B B * 2 B * 3
Commons Attribution License

Iter a result
result = 0; while a > 0 do
result = result + B;
a = a – 1;
Copyright University of Melbourne 2016, provided under Creative
A -1 B A -2 B * 2
A -3 B * 3
Commons Attribution License

Iter a result
result = 0; while a > 0 do
result = result + B;
a = a – 1;
Copyright University of Melbourne 2016, provided under Creative
A -2 B * 2
A -3 B * 3
Commons Attribution License

Iter a result
result = 0; while a > 0 do
result = result + B;
a = a – 1;
Copyright University of Melbourne 2016, provided under Creative
A -3 B * 3
Commons Attribution License

Iter a result
result = 0; while a > 0 do
result = result + B;
a = a – 1;
2 A -2 B * 2
3 A -3 B * 3
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

result = 0; while a > 0 do
result = result + B;
a = a – 1;
{result = A * B}
Iter a result
10 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

result = 0; while a > 0 do
result = result + B;
a = a – 1;
Iter a result
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
{result = A * B}
Usually must talk about the variables modified in the loop

result = 0; while a > 0 do
result = result + B;
a = a – 1;
{result = A * B}
Iter a result
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Usually must talk about the variables modified in the loop result, a

result = 0; while a > 0 do
result = result + B;
a = a – 1;
Iter a result
{result = A * B}
A statement that relates: result, a, A, B ?
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

result = 0; while a > 0 do
result = result + B;
a = a – 1;
{result = A * B}
Iter a result
A statement that relates: result, a, A, B ? result + (a * B) = A * B
11 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

result = 0; while a > 0 do
result = result + B;
a = a – 1;
{result = A * B}
result + (a * B)
0 + (A * B)
B + ((A – 1) * B)
B*2 + ((A – 2) * B)
B*3 + ((A – 3) * B)
A statement that relates: result, a, A, B ? result + (a * B) = A * B
12 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Back to the Proof
{result + (a * B) = A * B} while a > 0 do
result = result + B;
a = a – 1;
{result = A * B}
13 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Back to the Proof
{result + (a * B) = A * B} while a > 0 do
result = result + B;
a = a – 1;
{result = A * B} {result + (a * B) = A * B
result = result + B;
a = a – 1;
{result + (a * B) = A * B}
13 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Back to the Proof
{result + (a * B) = A * B} while a > 0 do
result = result + B;
a = a – 1;
{result = A * B} {result + (a * B) = A * B
result + (a * B) = A * B
result = A * B
result = result + B;
a = a – 1;
{result + (a * B) = A * B}
13 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

result + (a * B) = A * B
result = A * B
14 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

result + (a * B) = A * B
result = A * B
Does this hold?
14 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

result + (a * B) = A * B
result = A * B
Does this hold?
Need to prevent a being negative
14 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Strengthen the Invariant
Need to prevent a being negative result + (a * B) = A * B
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Strengthen the Invariant
Need to prevent a being negative
result+(a*B)=A*B∧a≥0
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Strengthen the Invariant
Need to prevent a being negative
result+(a*B)=A*B∧a≥0 result + (a * B) = A * B ∧ a ≥ 0
result = A * B
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Strengthen the Invariant
Need to prevent a being negative
result+(a*B)=A*B∧a≥0 result + (a * B) = A * B ∧ a ≥ 0
result + (a * B) = A * B ∧ a = 0
result = A * B result = A * B
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Strengthen the Invariant
Need to prevent a being negative
result+(a*B)=A*B∧a≥0 result + (a * B) = A * B ∧ a ≥ 0
result + (a * B) = A * B ∧ a = 0
result = A * B result = A * B
Invariant and negated loop guard now imply postcondition
15 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

{result + (a * B) = A * B ∧ a ≥ 0 ∧ a > 0}
result = result + B;
a = a – 1;
{result + (a * B) = A * B ∧ a ≥ 0}
16 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

{result + (a * B) = A * B ∧ a ≥ 0 ∧ a > 0}
result = result + B;
a = a – 1;
{result + (a * B) = A * B ∧ a ≥ 0}
17 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

a = a – 1;
{result + (a * B) = A * B ∧ a ≥ 0}
18 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

{result + (a * B) = A * B ∧ a ≥ 0 ∧ a > 0}
result = result + B;
a = a – 1;
{(result + (a * B) = A * B ∧ a ≥ 0)[a-1/a]} {result + (a * B) = A * B ∧ a ≥ 0}
a = a – 1;
{result + (a * B) = A * B ∧ a ≥ 0}
18 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

{result + (a * B) = A * B ∧ a ≥ 0 ∧ a > 0}
result = result + B;
{result + ((a-1) * B) = A * B ∧ a-1 ≥ 0}
a = a – 1;
{result + (a * B) = A * B ∧ a ≥ 0}
19 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
{result + (a * B) = A * B ∧ a ≥ 0 ∧ a > 0}
{(result + ((a-1) * B) = A * B ∧ a-1 ≥ 0)[result+B/result]}
result = result + B;
{result + ((a-1) * B) = A * B ∧ a-1 ≥ 0}
a = a – 1;
{result + (a * B) = A * B ∧ a ≥ 0}

{result + (a * B) = A * B ∧ a ≥ 0 ∧ a > 0} {(result + B) + ((a-1) * B) = A * B ∧ a-1 ≥ 0}
result = result + B;
{result + ((a-1) * B) = A * B ∧ a-1 ≥ 0}
a = a – 1;
{result + (a * B) = A * B ∧ a ≥ 0}
result + (a * B) = A * B ∧ a ≥ 0 ∧ a > 0 →
(result+B) + ((a-1) * B) = A * B ∧ a-1 ≥ 0
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

{result + (a * B) = A * B ∧ a ≥ 0 ∧ a > 0} {(result + B) + ((a-1) * B) = A * B ∧ a-1 ≥ 0}
result = result + B;
{result + ((a-1) * B) = A * B ∧ a-1 ≥ 0}
a = a – 1;
{result + (a * B) = A * B ∧ a ≥ 0}
result + (a * B) = A * B ∧ a ≥ 0 ∧ a > 0
(result+B) + ((a-1) * B) = A * B ∧ a-1 ≥ 0
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

{result + (a * B) = A * B ∧ a ≥ 0 ∧ a > 0} {(result + B) + ((a-1) * B) = A * B ∧ a-1 ≥ 0}
result = result + B;
{result + ((a-1) * B) = A * B ∧ a-1 ≥ 0}
a = a – 1;
{result + (a * B) = A * B ∧ a ≥ 0}
result + (a * B) = A * B ∧ a ≥ 0 ∧ a > 0
True (result+B) + ((a-1) * B) = A * B ∧ a-1 ≥ 0
21 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Rest of the Program
a = A; {?P1} result = 0; {I}
while a > 0 do {I ∧ a > 0}
result = result + B; a = a – 1;
{I ∧ a ≤ 0} {result = A * B}
result + (a * B) = A * B ∧ a ≥ 0 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Rest of the Program
result = 0;
{result + (a * B) = A * B ∧ a ≥ 0}

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Rest of the Program
{(result + (a * B) = A * B ∧ a ≥ 0)[0/result]}
result = 0;
{result + (a * B) = A * B ∧ a ≥ 0}

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Rest of the Program
{(a * B) = A * B ∧ a ≥ 0}
result = 0;
{result + (a * B) = A * B ∧ a ≥ 0}

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Rest of the Program
{((a * B) = A * B ∧ a ≥ 0)[A/a]}
{(a * B) = A * B ∧ a ≥ 0}
result = 0;
{result + (a * B) = A * B ∧ a ≥ 0}

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Rest of the Program {true}
{(A * B) = A * B ∧ A ≥ 0} a = A;
{(a * B) = A * B ∧ a ≥ 0} result = 0;
{result + (a * B) = A * B ∧ a ≥ 0}

Rest of the Program {true}
{(A * B) = A * B ∧ A ≥ 0} a = A;
{(a * B) = A * B ∧ a ≥ 0} result = 0;
{result + (a * B) = A * B ∧ a ≥ 0} Holds if:
((A * B) = A * B ∧ A ≥ 0)
DOESN’T HOLD
Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Strengthen Precondition
result = 0; while a > 0 do
result = result + B;
a = a – 1;
{result = A * B}
28 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Strengthen Precondition
result = 0; while a > 0 do
result = result + B;
a = a – 1;
{result = A * B}
29 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Strengthen Precondition {A ≥ 0}
{(A * B) = A * B ∧ A ≥ 0} a = A;
{(a * B) = A * B ∧ a ≥ 0} result = 0;
while a > 0 do {I ∧ a > 0}
result = result + B;
{result + ((a-1) * B) = A * B ∧ a-1 ≥ 0}
a = a – 1;
{I ∧ a ≤ 0} {result = A * B}
result + (a * B) = A * B ∧ a ≥ 0
30 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Strengthen Precondition {A ≥ 0}
{(A * B) = A * B ∧ A ≥ 0} a = A;
{(a * B) = A * B ∧ a ≥ 0} result = 0;
while a > 0 do {I ∧ a > 0}
result = result + B;
{result + ((a-1) * B) = A * B ∧ a-1 ≥ 0}
a = a – 1;
{I ∧ a ≤ 0} {result = A * B}
result + (a * B) = A * B ∧ a ≥ 0 QED 30 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

while i != N do
sum = sum + A[i];
i = i + 1;
done N−1 {𝗌𝗎𝗆 = Σj=0 A[j]}
31 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

while i != N do
(By sequence and consequence rules)
sum = sum + A[i];
i = i + 1;
{𝗌𝗎𝗆 = ΣN−1A[j]} j=0
32 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

while i != N do
{?I /\ i != N}
sum = sum + A[i]; i = i + 1;
{?I ∧ i = N}
{𝗌𝗎𝗆 = ΣN−1A[j]}
33 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
(By iteration/while loop rule)

Postcondition:
𝗌𝗎𝗆 = ΣN−1A[j] j=0
34 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Before the loop (0th iteration): sum = 0
Postcondition:
𝗌𝗎𝗆 = ΣN−1A[j] j=0
34 Copyright University of Melbourne 2016, provided under Creative Commons Attribution License

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Before the loop (0th iteration): sum = 0 After First Iteration: sum = A[0], i = 1
Postcondition:
𝗌𝗎𝗆 = ΣN−1A[j] j=0

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Before the loop (0th iteration): sum = 0
After First Iteration: sum = A[0], i = 1
After Second Iteration: sum = A[0] + A[1], i = 2
Postcondition:
𝗌𝗎𝗆 = ΣN−1A[j] j=0

Copyright University of Melbourne 2016, provided under Creative Commons Attribution License
Before the loop (0th iteration): sum = 0

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

Related Posts