Testing vs Verification

Resources

C251 text: Discrete Mathematics and Its Applications by Kenneth Rosen

C311 notes: Chapter 23 on Formal Semantics

Software Flaws are identified at three levels

1. A failure is an unacceptable behavior exhibited by a system

The frequency of failures measures software reliability

Low failure rate = high reliability

Failures result from violation of a requirement (e.g. a precondition is violated, a pop operation performed on an empty stack causing memory fault, out-of-index bounds fault)

2. A defect is a flaw that contributes to a failure

   For example, did not check for empty stack before pop.

   It might take several defects to cause one failure.

    

3. An error is a software decision that leads to a defect.

   Example: did not establish valid pre and postconditions.

   Example: did not ensure that precondition met (e.g. did not check that stack not empty before calling pop).

Eliminating Failures: Testing vs Verification

Testing = running the program with a set of inputs to gain confidence that the software has few defects (in this case, the program is said to be “tested”)

Goal: reduce the frequency of failures

When done: after the programming is complete

Methodology: develop test cases, normally including boundary conditions; run the program with each test case

Verification = formally proving that the software has no defects (in this case, the program is said to be “correct”)

Goal: detect errors and eliminate failures

When done: before, during and after the programming is complete

Methodology:

1. write separate specifications for the code
   
2. prove that the code and the specifications are mathematically equivalent

Program Correctness

The correctness of a program is based on a specific standard. That standard is called a specification.

// Maximum of two integers int max (int a, int b) {   int m;   if (a >= b)      m = a;   else      m = b;   return m; }

An informal specification for the above program might be that it “finds the maximum value of any two integers.”

Formalizing a Specification

A formal specification is written as a logical expression called an assertion.

An assertion describes the state of the program’s variables.

Two key assertions are the program’s precondition and its postcondition; P and Q respectively.

A domain is a set of values over which a variable is well defined.

The primitive types (int, float, boolean, etc.) and standard Java classes (String, Vector, HashMap, etc.) provide domains for reasoning about programs.

Pre and Postconditions

Preconditions describe minimum requirements for the program to run.

For max, the precondition is P = true because a and b can be any integers.

Postconditions describes what it will be computed when the precondition holds.

For max, a postcondition is Q = m ≥ a and m ≥ b, defining m to be greater than or equal both a and b.

Before proving a program’s correctness, we first write its specifications:

{P is true} int max (int a, int b) {   int m;   if (a ≥ b)      m ← a;   else      m ← b;   return m; } {Q is m ≥ a and m ≥ b}

Proof must show that preconditions imply postconditions for the code of max:

P → Q

true  → m ≥ a and m ≥ b

Truth table
P → Q

P	Q	P → Q
F	F	T
F	T	T
T	F	F
T	T	T

Example

{ P is x = 1, y = 2} int sum (int x, int y) {   z ← x + y;   return z; } { Q is z = 3 }

Proof

x = 1, y = 2	P is true
z ← x + y	Definition of z
z ← 1 + 2	Substitution for x and y
z ← 3	Addition 1 + 2
z ← 3	Q is true by z ← 3
z = 3	∴ P → Q

 

Example: Factorial - computing n!

{ P is n ≥ 1} int Factorial (int n) {   int f ← 1;   int i ← 1;   while (i < n) {     i ← i + 1;     f ← f * i;   }   return f; } { Q is f = n!}

Example raises several issues. What happens if:

1. preconditions hold - does that guarantee the postcondition holds?
   
2. the program has a loop that never terminates?
   
3. the program terminates abnormally (e.g., an exception is raised such as overflow)?
   

Short Detour - Assertions for runtime checking of conditions

Assertions test a condition that should be true at runtime, if the condition is false an exception is thrown.

Example tests that the precondition is true: { P is n ≥ 1}

{ P is n ≥ 1} int Factorial (int n) {   assert n >= 1;

Question 2.1

1. Our precondition assertion was easy. What is the problem with defining an assertion for the postcondition: { Q is f = n!}?
   
2. How is the assert different from a proof?

Partial Correctness

Let's assume that nothing bad ever happens

• programs always terminate after a finite number of steps
  
• termination is always normal.

Then such a program is partially correct if:

for every set of input values that satisfies precondition P, the program computes a result that satisfies postcondition Q.

E.g., Factorial is partially correct if for every value of n that satisfies n ≥ 1, it computes result f = n!

P → Q

n ≥ 1  →  f = n!

(Partial) Correctness Proofs

Let’s think generally about any program or sequence of statements s, whose precondition is P and postcondition is Q.

A “Hoare triple” is a predicate of the form:

{P} s {Q}

which asserts that:

“beginning in a state that satisfies P, execution of statements s, results in a state that satisfies Q.”

If we can prove that this Hoare triple is valid, (i.e., it is true for all assignments of values to variables in P, Q, and s) then the program s is said to be correct.

 

Constructing a Correctness Proof

If the program is a series of statements:

s₁; s₂; …; s_n

We start with the Hoare triple

{P} s₁; s₂; …; s_n {Q}

and use inference rules for programs to derive an intermediate triple:

{P_i} s_i {P_i+1}

for every statement s_i in this sequence.

When done, we also ensure that:

P → P₁ and P_n+1 → Q

Note: This process is similar to a direct proof in logic, where we use inference rules to derive a series of assertions that logically link the premises to the conclusion.

Review (weakest precondition)

Generally we expect a specific result or postcondition from an algorithm but need to prove that the precondition for which the algorithm produces the postcondition.

The weakest precondition is one having the largest domain (e.g. the most values for which the algorithm produces correct results).

For example, the precondition x ≥ 0 is said to be weaker than x ≥ 1 since the domain includes more values (i.e. 0).

 

Assignment statements

x := E an assignment statement and Q its postcondition

Precondition, P, defined by the axiom: P = Q_x←E

means P is computed as Q with all instances of x replaced by E.

Example

statement	postcondition
a := b/2	{a < 10}

P = Q_x←E

x is a

E is b/2

Q is { a < 10 }

Weakest precondition (wp) computed by substituting b/2 in postcondition assertion {a < 10} for a as follows:

{ a < 10 }		Q
{ b/2 < 10 }		a ← b/2
{ b < 20 }		P

Thus wp:

{b < 20} a := b/2 {a < 10}

General notation for precondition P, statement S, and postcondition Q is:

{P} S {Q}

 For assignment statement with P = Q_x←E, notation is: {Q_x←E} S {Q}

Question 2.2 - Give the wp for each of the following:

1. x := y           { x < 5 }
2. x := y - 6      { x < 5 }
3. x := x + 1     { x < 5 }
4. x := x + y     { x < 5 }

 

Logical Inference Rules

Because programs consist of more than one statement, need logical inference rules for each program construct to prove correctness.

Written in the form:

conditions
conclusion

Example: commutative property of addition

a + b = c
b + a = c

Axiom: Inference rule with no condition, always holds

________
a + 0 = a

 

Proof Rules of Inference

Statement Type	Proof Rule
Assignment    x=E	_______________      {Qx←E} S {Q}
Sequence    S1; S2	{P1} S1 {P2}, {P2} S2 {P3}         {P1} S1; S2 {P3}
Conditional    if(test) then S1 else S2	{test && P} S1 {Q}, {(!test) && P} S2 {Q}            {P} if (test) then S1 else S2 {Q}
Loop invariant    while(test) S	{test && P} S {P}          {P} while (test) S {!test && P}
Rule of consequence	{P} S {Q}, P' ⇒ P, Q ⇒ Q' {P'} S {Q'}

 

Sequences

• Weakest precondition for a sequence of statements cannot be described by an axiom
• Precondition depends on particular kinds of statements in sequence
• Precondition can only be described with an inference rule

Let S1 and S2 be adjacent statements

If S1 and S2 have following preconditions and postconditions, P1, P2 and P3

{P1} S1 {P2}

{P2} S2 {P3}

inference rule for two-statement sequence is:

{P1} S1 {P2}, {P2} S2 {P3}
        {P1} S1; S2 {P3}

Example

y := 3 * x + 1;                                     -- S1
x := y + 3;                    {x < 10}         -- S2

wp for last statement

{y < 7}   x := y + 3;     {x < 10}

By inference rule, {y < 7} is precondition for S2 and postcondition for S1:

                y := 3 * x + 1;          {y < 7}

{y < 7}   x := y + 3;                {x < 10}

wp can now be computed for S1:

{ 3 * x + 1 < 7 }
{ x < 2 }

yielding:

{x < 2}  y := 3 * x + 1;    {y < 7}

{y < 7}  x := y + 3;          {x < 10}

by inference on:

{x < 2}  y := 3 * x + 1 {y < 7} , {y < 7}  x := y + 3 {x < 10}
        {x < 2}  y := 3 * x + 1,  x := y + 3 {x < 10}

 

Question 2.3 - Give the wp for each of the following:

1. y := x
   x := y           { x < 5 }
   
2. y := x + 3
   x := y - 6      { x < 5 }

 

Rule of consequence

{P} S {Q}, P' ⇒ P, Q ⇒ Q'
       {P'} S {Q'}

States:

if logical statement {P} S {Q} is true and

P' implies assertion P

Q implies assertion  Q’

then it can be inferred that {P'} S {Q'}

Example   

{P} S {Q}, P' ⇒ P, Q ⇒ Q'
        {P'} S {Q'}

• P  {x > 3}
• P' {x > 3}
• S  x:=x-3
• Q  {x > 0}
• Q' {x > -1}

yields:

{x>3} x:=x-3 {x>0}, {x>3} ⇒ {x>3}, {x>0} ⇒ {x>-1}
                  {x > 3} x := x - 3 {x > -1}

completing the proof.

Postcondition weakened.

Question 2.4 - Is this correct? How is the postcondition weakened?

 

Example

{P} S {Q}, P' ⇒ P, Q ⇒ Q'
        {P'} S {Q'}

• P  {x > 3}
• P' {x > 5}
• S  x:=x-3
• Q  {x > 0}
• Q' {x > 0}

yields:

{x>3} x:=x-3 {x>0}, {x>5} ⇒ {x>3}, {x>0} ⇒ {x>0}
                  {x > 5} x := x - 3 {x > 0}

completing the proof.

Precondition strengthened.

Question 2.5 - Is this correct? How is the precondition strengthened?

 

Conditionals

Consider only if-else conditions.

{test && P} S1 {Q}, { !test && P} S2 {Q}
           {P} if (test) then S1 else S2 {Q}

Both S1 and S2 must be proven (the true and false case) to hold for precondition P, producing the same postcondition.

true (then): {test && P} S1 {Q}

false (else): { !test && P} S2 {Q}

 

Example

if (x > 0)
   then y := y – 1
   else y := y + 1 { y > 0 }

Use assignment axiom to find preconditions:

then {y > 1}  y := y – 1 {y > 0}

else {y > -1} y := y + 1 { y > 0 }

{y > 1} ⇒ {y > -1}

By the Rule of Consequence use {y > 1} for selection statement precondition (i.e. holds for both statements).

Strengthen precondition.

{P} S {Q}, P' ⇒ P, Q ⇒ Q'
        {P'} S {Q'}

• P   {y > -1}
• P’{y > 1}
• S   y:=y+1
• Q  {y > 0}
• Q' {y > 0}

yields:

{y > -1} y:=y+1 {y>0}, {y > 1} ⇒ {y > -1}, {y>0} ⇒ {y>0}
                  {y > 1} y:=y+1 {y > 0}

Conditional rule of inference

{test && P} S1 {Q}, { !test && P } S2 {Q}
    {P} if (test) then S1 else S2 {Q}

yields:

{x > 0 && y > 1} y := y - 1 { y > 0 }, { !(x > 0) && y > 0} y := y + 1 {y > 0}
           {y > 1} if (x > 0) then y := y - 1 else y := y + 1 {y > 0}

and the conditional's precondition:

{y > 1}  if (x > 0)
                 then y := y - 1
                 else y := y + 1 { y > 0 }

 

Question 2.6 - Determine the conditionals' preconditions.

1. if (x < 5)
       then y := y - 7;
       else y := y + 8; {y > 10}
   
   
2. if (x < 5)
       then x := y - 7;
               y := x / 2;
       else y := y + 8; {y > 10}

 

Proof of Correctness - maxOf

Determining weakest preconditions from postconditions is useful but not always practical.

Directly proving postconditions are true given the preconditions are true also determines algorithm correctness.

The algorithm below determines the maximum of two values.

Precondition is true (assuming two integers are supplied).

Because the algorithm consists of an if-else condition, we must prove postcondition Q is true to use the Conditional Rule of Inference:

{test && P} S1 {Q}, { !test && P} S2 {Q}
     {P} if (test) then S1 else S2 {Q}

-- P:  true procedure maxOf( x, y : integers) if  x > y then maxOf ← x       else maxOf ← y -- Q: maxOf  ≥ x ^ maxOf  ≥ y

P	true
test	x > y
S1	maxOf ← x
S2	maxOf ← y
Q	maxOf  ≥ x ^ maxOf  ≥ y

Substituting P, S1, S2, and Q of the if-else conditional, we get:

{x > y && true} maxOf ← x { maxOf  ≥ x ^ maxOf  ≥ y}, { !(x > y) && true} maxOf ← y { maxOf  ≥ x ^ maxOf  ≥ y }
           {true} if (x > y) then maxOf ← x else maxOf ← y { maxOf  ≥ x ^ maxOf  ≥ y}

 

Recall that both S1 and S2 must be proven (the true and false case) to hold for precondition P, producing the same postcondition.

true: {x > y && true} maxOf ← x { maxOf  ≥ x ^ maxOf  ≥ y }

false: { !(x > y) && true} maxOf ← y { maxOf  ≥ x ^ maxOf  ≥ y }

 

Proof of true case:

x > y && true	True on then
x > y	Simplification Rule of Inference
maxOf = x	From assignment: maxOf ← x
maxOf  ≥ x ^ maxOf  ≥ y	x > y && maxOf = x
	∴ Q is true, maxOf  ≥ x ^ maxOf  ≥ y

Proof of false case:

!(x > y) && true	True on else
!(x > y)	Simplification Rule of Inference
maxOf = y	From assignment: maxOf ← y
maxOf  ≥ x ^ maxOf  ≥ y	!(x > y) && maxOf = y
	∴ Q is true, maxOf  ≥ x ^ maxOf  ≥ y

 

-- P:  true procedure maxOf( x, y : integers) if  x > y then maxOf ← x       else maxOf ← y -- Q: maxOf  ≥ x ^ maxOf  ≥ y

 

See Loop Invariant Tracing before reading further

 

Loop invariant

Invariant means unchanged The loop contains an invariant which describes what remains unchanged when loop executed Permits understanding what the loop does without having to understand (at the same time) how it does it. Can reason about the loop's effect without hand tracing each loop iteration. The loop invariant is always true: before the loop, initialization   at the end of each loop, maintenance   and after the loop completes, termination.

Loop invariant Rule of Inference for while:

        {test && P} S {P}          
{P} while (test) S {!test && P}

where S is repeatedly executed until test condition becomes false.

P must remain true prior to each execution loop of S and after the loop terminates.

P is a loop invariant if {test && P} S {P} is true.

 

Induction Proofs

Induction proofs used for loop invariants are constructed differently from those studied in discrete mathematics.

Loop invariant proofs can use induction as part of the proof that the loop invariant holds.

The following is an induction proof from discrete math that a summation is equal to a closed form solution.

Summation = Closed form solution proof

∀i, 1 ≤ i ≤ n, ∑i = (n*(n+1))/2

Induction proof

Base case:                        P₁:  1 = (1*(1+1))/2

Induction Hypothesis:        P_k: ∀k, 1 ≤ i ≤ k, ∑i = 1+2+...+k = (k*(k+1))/2

Definition:                         P_k+1: 1+2+...+k+(k+1)

Show:                                P_k+1: ((k+1)*((k+1)+1))/2 = ((k+1)*(k+2))/2

Pk+1	= 1+2+...+k+(k+1)
	= Pk + k+1
	= (k*(k+1))/2 + k+1
	= (k2+k)/2 + (2k+2)/2
	= (k2+3k+2)/2
∴	= ((k+1)*(k+2))/2

Loop Invariant Summation

The following is an induction proof that the loop invariant holds in algorithm to compute the summation.

Loop invariant proofs must show three parts:

1. Initialization - the loop invariant holds prior to executing the loop, after initialization.
2. Maintenance - the loop invariant holds at the end of executing the loop.
3. Termination - the loop eventually terminates.

pre: n ≥ 1 Pn(n) k := 1 Pk := 1 Pk = 1+2+...+k ^ k ≤ n while k < n         Pk+1 := Pk + k + 1         k := k + 1         Pk := Pk+1 post: Pn(n) = 1+2+...+n

Show loop invariant: P_k = 1+2+...+k ^ k ≤ n is always true

 

Proof of Correctness - Loop Invariant - Factorial

Loop invariant proofs can be more or less formal.

First is a less formal proof demonstrating the loop invariant of a factorial function holds.

{ Precondition: n ≥ 1 } fact(n) i ← 1 fact ← 1 { Invariant P: fact = i! && i ≤ n } while (i < n) do         i ← i + 1         fact ← fact * i { Postcondition: fact = n! }

Loop invariant proofs must show three parts:

1. Initialization - the loop invariant holds prior to executing the loop, after initialization.
2. Maintenance - the loop invariant holds at the end of executing the loop.
3. Termination - the loop eventually terminates.

1. Initialization: Prove assertion P true at start of loop: i ← 1 ≤ n                     -- by { Precondition: n ≥ 1 } fact ← 1 = 1! = i!        -- by definition of 1! { P: fact = i! && i ≤ n } is true before while.   Loop invariant for while loops:         {test && P} S {P}           {P} while (test) S {!test && P}

2. Maintenance: Prove P is true at end of loop: Assume: { P: fact = i! && i ≤ n } is true test condition while (i<n) is true. New values inew and factnew of i and fact are: inew ← i + 1 factnew ← fact * (i+1) = (i+1)! = inew! Since i < n also have: inew ← i + 1 ≤ n { P: fact = i! && i ≤ n } is true at end of loop since fact = i! && i ≤ n.

3. Termination: Prove that loop terminates At beginning: i ←1 Assuming the precondition n ≥ 1 holds, after n-1 loop traversals of:       i ← i + 1 the new value of i will be: i = n terminating the loop. Loop terminates given that precondition holds: n ≥ 1 { P: fact = i! && i ≤ n } is then a loop invariant.

4. Postcondition met Since P is a loop invariant, by:        {test && P} S {P}           {P} while (test) S {!test && P} If the while terminates, { P: fact = i! && i ≤ n } is then true fact = i! i ≤ n and i < n is false, from 3. Termination. Hence at loop termination: i = n fact = i! = n!

 

Induction Proof of loop invariant - Factorial

More formal loop invariant proofs can also be performed by induction.

Note below use of P_k and P_k+1 not necessary but helpful in thinking about the induction.

The loop invariant is:

Pk = k! ^ k ≤ n

pre: n ≥ 1 Pn(n) k := 1 Pk := 1 Pk = k! ^ k ≤ n while k < n         Pk+1 := Pk * k+1         k := k + 1         Pk := Pk+1 post: Pn = n!

P_k = k! ^ k ≤ n is always true (P_k = k! means that P₅ = 5! = 120, etc.):

 

Example - Maximum of a sequence

The loop result is the maximum of a sequence of numbers.

maxOf preconditions have been modified to be more rigorous.

-- P:  ∃x ^ ∃y procedure maxOf( x, y : integers) if  x > y then maxOf ← x       else maxOf ← y -- Q: maxOf  ≥ x ^ maxOf  ≥ y

The loop invariant is:

∀k: 1 ≤ k < i, ak ≤ max

-- Precondition:  ∃a1 procedure max( a1, a2, a3, ..., an : integers) max ← a1 i ← 2 { invariant P: ∀k: 1 ≤ k < i, ak ≤ max } while  i ≤ n max ← maxOf(max, ai)    -- P:  ∃max ^ ∃ai i ← i + 1 -- Postcondition: ∀j: 1 ≤ j ≤ n, aj ≤ max    Question 2.7.1        max( { 7, 5, 19, 8 } )

i n max ai 2 4 7 1 2 3 4 7 5 19 8 3 4 7 1 2 3 4 7 5 19 8 4 4 19 1 2 3 4 7 5 19 8 5 4 19 1 2 3 4 7 5 19 8

What is n?   Are maxOf preconditions meet?   What does the loop invariant say in English?          ∀k: 1 ≤ k < i, ak ≤ max   Loop invariant true before the while loop?             i?      max? ∀k: 1 ≤ k < i, ak ≤ max   Unroll all iterations of the loop invariant:                i?      max? ∀k: 1 ≤ k < i, ak ≤ max   Loop invariant true after the loop completes?          i?      max? ∀k: 1 ≤ k < i, ak ≤ max

Preconditions specify conditions that must be true to ensure postconditions.

Loop invariant accomplishes the work of the max algorithm.

Postconditions specify result of loop invariant when preconditions hold.

Precondition:     ∃a1                                        loop invariant:   ∀k: 1 ≤ k < i, ak ≤ max Postcondition:    ∀j: 1 ≤ j ≤ n, aj ≤ max

Must have at least one element in sequence. All k elements, those before i, ak ≤ max. All aj elements are ≤ max

 

Proof of Correctness - Loop Invariant

Loop invariant for while loops:

        {test && P} S {P}          
{P} while (test) S {!test && P}

 

1. Initialization: Prove assertion P true at start of loop: max ← a1                             -- by { Precondition: ∃a1 } i ← 2                                    -- by definition ∀k: 1 ≤ k < 2, a1 ≤ max        -- max = a1 { P: ∀k: 1 ≤ k < i, ak ≤ max } is true before while -- Precondition:  ∃a1 procedure max( a1, a2, a3, ..., an : integers) max ← a1 i ← 2 { invariant P: ∀k: 1 ≤ k < i, ak ≤ max } while  i ≤ n max ← maxOf(max, ai) i ← i + 1 -- Postcondition: ∀j: 1 ≤ j ≤ n, aj ≤ max

2. Maintenance: Prove P is true at end of loop: Assume: { P: ∀k: 1 ≤ k < i, ak ≤ max } is true i ≤ n while test condition is true. Values inew and maxnew of i and max are: maxnew ← maxOf(max, ai) inew ← i + 1 {  P: ∀k: 1 ≤ k < inew, ak ≤ maxnew } is true since { P: ∀k: 1 ≤ k < i, ak ≤ max } is true a1 ≤ max, ..., ai-1 ≤ max maxnew = maxOf(max, ai) is true { ∀k: 1 ≤ k < i + 1, ak ≤ maxnew } is then true max ≤ maxnew a1 ≤ maxnew, ..., ai-1 ≤ maxnew, ai ≤ maxnew { ∀k: 1 ≤ k < inew, ak ≤ maxnew } is true inew = i + 1 is true { P: ∀k: 1 ≤ k < inew, ak ≤ maxnew } is true at end of loop.   { P: ∀k: 1 ≤ k < i, ak ≤ max } is true at end of loop. Replacing i = inew and max = maxnew

3. Termination: Prove that loop terminates At beginning: i ←2 Assuming the precondition ∃a1 holds, n ≥ 1. After n-1 loop traversals of:       i ← i + 1 the new value of i will be: i > n terminating the loop. Loop terminates given that precondition ∃a1 holds: n ≥ 1 { P: ∀k: 1 ≤ k < i, ak ≤ max } is then a loop invariant.

4. Postcondition met Since P is a loop invariant, by:        {test && P} S {P}           {P} while (test) S {!test && P} If the while terminates, { P: ∀k: 1 ≤ k < i, ak ≤ max } is true { invariant P: ∀k: 1 ≤ k < i, ak ≤ max } while  i ≤ n max ← maxOf(max, ai) i ← i + 1 and i ≤ n is false, hence at loop termination: i > n Loop postcondition is therefore true: ∀k: 1 ≤ k < i, ak ≤ max max postcondition is therefore true (there are no other statements): ∀k: 1 ≤ k ≤ n < i, ak ≤ max

Note:

This is not a rigorious proof of correctness.

We skipped details of pre and postconditions for each statement in the loop.

But does provide some confidence that the loop code functions as intended and postconditions are met.

 

Induction Proof of loop invariant - Maximum of a sequence

Note

maxOf(P_k, a_i+1) is maximum of P_k and a_i+1

Use of P_k and P_k+1 not necessary but helpful in thinking about the induction.

The loop invariant is:

∀j: 1 ≤ j ≤ i, aj ≤ Pk ^ i ≤ n

-- Precondition:  ∃a1 procedure Pn( a1, a2, a3, ..., an : integers) Pk ← a1 i ← 1 { invariant ∀j: 1 ≤ j ≤ i, aj ≤ Pk ^ i ≤ n} while  i < n Pk+1 ← maxOf(Pk, ai+1)     -- P:  true i ← i + 1 Pk ← Pk+1 -- Postcondition: ∀j: 1 ≤ j ≤ n, aj ≤ Pk

Show ∀j: 1 ≤ j ≤ i, a_j ≤ P_k ^ i ≤ n is always true

 

Induction Proof of loop invariant - Summation of a sequence

Question 2.7.2 

a. What is the postcondition?   

b. What is the loop invariant?   

-- Precondition:  ∃a1 procedure Pn( a1, a2, a3, ..., an : integers) Pk ← a1 i ← 1 ∀j: 1 ≤ j ≤ i, ∑aj = Pk ^ i ≤ n while  i < n Pk+1 ← Pk + ai+1 i ← i + 1 Pk ← Pk+1

i n Pk ai 1 4 7 1 2 3 4 7 5 9 8 2 4 12 1 2 3 4 7 5 9 8 3 4 21 1 2 3 4 7 5 9 8 4 4 29 1 2 3 4 7 5 9 8

Show ∀j: 1 ≤ j ≤ i, ∑a_j = P_k ^ i ≤ n is always true

Postcondition results from loop invariant at termination.

Solution

 

Induction Proof of loop invariant - Sorting a sequence

Practical programs consist of modules called by other modules.

Implementing verified programs require that all modules be verified for correctness.

Verified modules, for which preconditions are true, can be assumed to produce true postconditions.

The insert module below inserts a value into an array of n+1 elements that is already sorted through the nth element.

∃a_n+1^∀j: 1 ≤ j < n, a_j ≤ a_n

insert( a₄, {a₁, a₂, a₃})

results in an array a₁, a₂, a₃, a₄ that is sorted through the n+1 element.

insert( 5, {3, 6, 9})

results in an array {3, 5, 6, 9}.

-- Precondition:  ∃an+1^∀j: 1 ≤ j < n, aj ≤ an procedure insert( x, a1, a2, a3, ..., an, an+1 : integers) i ← 1 while  i < n ^ x > ai i ← i + 1 x ⇔ ai while  i ≤ n i ← i + 1 x ⇔ ai -- Postcondition:  ∀j: 1 ≤ j ≤ n, aj ≤ an+1

insert( 5, {3, 6, 9}) i n+1 x ai 1 4 5 1 2 3 4 3 6 9 5 2 4 5 1 2 3 4 3 6 9 5 3 4 6 1 2 3 4 3 5 9 6 4 4 9 1 2 3 4 3 5 6 9

Insertion sort is relatively simple using insert module.

-- Precondition:  ∃a1 procedure insertionSort( a1, a2, a3, ..., an : integers) i ← 1 ∀j: 1 ≤ j < i,  aj ≤ ai ^ i ≤ n while  i < n i ← i + 1 a ← insert( ai , a) -- Postcondition:  ∀j: 1 ≤ j < n, aj ≤ an

Question 2.7.3 

a. What is the postcondition?   

b. What is the loop invariant?