Testing And Verification

Chapter 6 Testing and verification

Software Engineering 

A program’s life cycle is the sequence of phases it goes through from its conception to its ultimate demise.



A new program is created in the development stage.



Software maintenance is the process of modifying a program in order to enhance it or fix problems.



Historically, computer scientists have developed and used various software development process models, including: 

Build-and-Fix



Waterfall model



Iterative process

Build-and-Fix 

The build-and-fix approach does not address the overall quality of a program.

Write program

Modify program

Release

Waterfall model 

The waterfall model is a linear process in which one stage is followed by the next. Establish requirements Create design Implement code Test system

Release

Iterative process 

An iterative process is one that allows a software developer to cycle through different development activities. Establish requirements



The iterative process allows backtracking to correct problems.

Create design Implement code Test system

Release

Evolutionary Development 

The iterative process leads to the following evolutionary development process. Establish requirements

General structure of the system

Architectural design

Establish refinement scope

Unit and Integration test

System test

Release

Identify classes & objects

Refinement cycle Identify relationships

Implementation

Specific methods and algorithms Detailed design

Testing 

The development of a class involves design, specification, implementation, and testing.



Testing is a fundamental part of building a software system.



Testing is an activity with the goal of determining whether or not an implementation functions as intended: 

Testing attempts to determine if the implementation is correct.

Testing (cont.) 

For any interesting problem, we cannot exhaustively test all cases.



Testing is effective at showing errors in your implementation, but really doesn’t show that the implementation is correct.



Testing consists of two phases: 

Test activities are determined and test data selected. 



Test design

The test is conducted and test results compared with expected results.

Testing (cont.) 

We will consider two forms of testing: 



Functional (or System) Testing 

Testing an entire system to make sure that it conforms to the customer’s requirements



Black box testing

Unit and Integration Testing 

Unit testing involves testing individual system components to verify that they perform correctly



Integration testing involves the interaction between individual system components to make sure that they interact correctly



White box testing and Gray box testing

Functional Testing 

Systems testing



Black box testing



Test design generally begins with the analysis of: 

functional specifications of the system 



system requirements

ways in which the system will be used 

“use cases”

Unit Testing    





The other form of testing is unit testing. Recall that we test a class we are implementing to increase our confidence that it behaves as expected. Testing is part of the job of implementing the class. Programmers often spend more time debugging than writing code. As such, the best way to improve productivity is to spend more effort on design. Once the design is implemented, the best way to reduce debugging time is to adopt an aggressive testing regimen. Incremental test-driven implementation is an effective means of reducing the time required to track down and correct bugs.

White Box Testing     

One form of unit testing is white box testing. White box testing derives its test cases based on the implementation. Test cases are defined by considering as many of the paths through the program as possible. The ultimate white box test is the execution of every possible path through the program. In general, it is not feasible to execute every path so we will consider some less complete testing criteria:   

Decision coverage Condition coverage Multiple condition coverage

Decision Coverage For each decision, you should add test cases, one for the true case and one for the false case. Unfortunately, this approach does not guarantee a complete set of test cases:

   

If a program has no decisions then this approach would produce no test cases. If a program has complex conditions then this approach may not be adequate. Consider the following if statement: if ((a < 0) && (b < 10)) { … }

Decision Coverage (cont.) 

Each decision outcome is exercised by the test cases:  



a = 2, b = 5 a = -1, b = 5

Note that this does not exercise the condition on b.

Condition Coverage 



For each decision, you should add test cases such that each condition in the decision takes on all possible outcomes at least once. If a program has complex conditions then this approach still may not be adequate. Consider the following if-else statement: if ((a < 0) && (b < 10)) { … } else { … }

Condition Coverage (cont.) 

Each condition in the decision is exercised by the test cases: 

a = -1, b = 11



a = 5, b = 5



Note that this does not cause the else clause to execute.



One way to avoid the problems with decision coverage and condition coverage is to combine these methods: 

Each condition in a decision takes on all possible outcomes at least once and each decision takes on all possible outcomes at least once.



But this still does not guarantee coverage of all possible outcomes of all possible combinations of conditions.

Multiple Condition Coverage 





Multiple condition coverage is a more general criteria which covers the problems with decision and condition coverage. Define enough test cases so that every possible combination of condition outcomes and all points of entry in a program are invoked at least once. Consider the following code segment: if ((a > 1) && (b == 0)) { statement1 } if ((a == 2) || (c > 1)) { statement2 }

Multiple Condition Coverage (cont.) 

All possible combinations of condition outcomes in each decision can be covered with the following eight cases: 1. 2. 3. 4. 5. 6. 7. 8.

a a a a a a a a

> 1, b == 0 > 1, b != 0 <= 1, b == 0 <= 1, b != 0 == 2, c > 1 == 2, c <= 1 != 2, c > 1 != 2, c <= 1



These cases come directly from truth tables: a > 1

b == 0

true

true

true

false

false

true

false

false

a == 2

c > 1

true

true

true

false

false

true

false

false

Multiple Condition Coverage (cont.) 

These eight cases can be covered by the following four cases: 1. a == 2, b == 0, c == 2 ⇒ Covers cases 1 and 5

2. a == 2, b == 1, c == 1 ⇒ Covers cases 2 and 6

3. a == 1, b == 0, c == 2 ⇒ Covers cases 3 and 7

4. a == 1, b == 1, c == 1 ⇒ Covers cases 4 and 8

1. 2. 3.

a > 1, b == 0 a > 1, b != 0 a <= 1, b == 0

4.

a <= 1, b != 0

5. 6.

a == 2, c > 1 a == 2, c <= 1

Multiple Condition Coverage (cont.) 

Notice that we still haven’t executed all paths through the segment: 1. a == 2, b == 0, c == 2 ⇒ Executes statement1 and executes statement2

2. a == 2, b == 1, c == 1 ⇒ Skips statement1 and executes statement2

3. a == 1, b == 0, c == 2 ⇒ Skips statement1 and executes statement2

4. a == 1, b == 1, c == 1 ⇒ Skips statement1 and skips statement2

The path “executes statement1 and skips statement ” is not executed.

Gray Box Testing  

Another form of unit testing is gray box testing. Gray box testing is also referred to as data-driven testing:   



Not concerned with the internal structure of the method. Test data is derived solely from method specifications. Look for circumstances in which the method does not behave according to its specifications.

Let’s consider 3 approaches for gray box testing:   

Equivalence Partitioning Boundary Value Analysis Error Guessing

Equivalence Partitioning  

 

Partition the domain of input values into groups called equivalence classes. Equivalence classes are chosen such that testing one element in the class is equivalent to testing any other element in the class. Valid equivalence classes represent valid inputs to the method. Invalid equivalence classes represent all other inputs (i.e., those that violate the precondition) 



Invalid inputs are program errors and should not be tested.

No rules for identifying equivalence classes, but there are some guidelines.

Equivalence Partitioning (cont.)  



 

If an input condition specifies a range of values, identify a valid equivalence class for that range. If an input condition specifically lists the number of values, identify one valid equivalence class for these values. If an input condition specifies a set of input values and there is reason to believe that each is handled differently by the program, identify one valid equivalence class for each element in the set. If an input condition specifies a “must be” situation, identify a valid equivalence class for it. If there is any reason to believe that elements in an equivalence class are not handled in an identical manner by the program, split the equivalence class into smaller equivalence classes.

Boundary Value Analysis  



Divide the input space into equivalence classes and select a test case from each class. Boundary value analysis focuses on selecting data near the edges of conditions on both input space and output space. General guidelines: 





If an input or output condition specifies a range of values, write test cases for the ends of the range. If an input or output condition specifies a number of values, write test cases for the minimum and maximum number of values. If the input or output of a procedure is an ordered set, focus attention on the first and last elements of the set.

Error Guessing  

Error guessing is largely based on intuition and experience as to frequently encountered errors. Examples of error guessing situations:   

  

Null strings 0 numeric values Numeric values nearly exceeding computer storage capability Collections or files that are empty or contain only one value Collections containing all the same value Collections in some ordered form

Combined Strategy 

Overall strategy for gray box testing: 1. Analyze preconditions and postconditions to make a list of the external conditions, both input and output. 2. Divide each of these external conditions into valid equivalence classes. 3. Use boundary value analysis to identify test cases for these equivalence classes. A test case may cover more that one equivalence class. 4. Use error guessing to add other classes and test cases. 5. For each test case, identify the expected output. 6. Test the procedure and compare the expected output with the actual output.

Testing Summary 

 

Now let’s try to apply some of the ideas we just discussed about testing to the design and implementation of our classes. We’ll focus on gray box testing. We’ll employ incremental test-driven implementation:     

Implementation proceeds in relatively small increments. Code a little, test a little. Each time you add a new bit of functionality, you test it immediately. Write a test for a feature before implementing the feature. Let’s consider the process of testing the TrafficSignal class.

Testing TrafficSignal    



We want to create a TrafficSignal instance and exercise it by querying it and giving it commands. To do this, we need another object to act as client to the TrafficSignal. We will call this class TrafficSignalTest and put it in the same package as the TrafficSignal class. Since it does not need to be accessed from outside the package, we do not need to make TrafficSignalTest public. The only property of TrafficSignalTest is the TrafficSignal to be tested.

Testing TrafficSignal (cont.) 

Stubbed implementation of  TrafficSignal public class TrafficSignal { public static final int public static final int public static final int private int light; public TrafficSignal () } public int light () { return 0; } public void change () { } }

GREEN = 0; YELLOW = 1; RED = 2; { Left blank

Dummy return value

Left blank

Testing TrafficSignal (cont.) 

We start by defining a new class named TrafficSignalTest: /** * A tester for the class TrafficSignal. */ class TrafficSignalTest { private TrafficSignal signal; /** * Create a TrafficSignalTest. */ public TrafficSignalTest () { signal = new TrafficSignal(); } /** * Run the test. */ public void runTest () { } }

// the object to test

Testing TrafficSignal (cont.) 

We’ll finish this class by completing runTest() later, but first let’s create a driver class Test: /** * A simple test system for the class TrafficSignal. */ class Test { /** * Run the test. */ public static void main (String[] argv) { TrafficSignalTest test; test = new TrafficSignalTest(); test.runTest(); } }

Testing TrafficSignal (cont.) 

We could eliminate the variable and assignment, and write the main() method as a single statement: /** * A simple test system for the class TrafficSignal. */ class Test { /** * Run the test. */ public static void main (String[] argv) { (new TrafficSignalTest()).runTest(); } }

Testing TrafficSignal (cont.) 

Let’s begin writing runTest() by testing the initial state. Although we could write all of our tests inline in runTest(), the testing task is much more manageable if we put each test in a separate method. /** * Run the test. */ public void runTest () { testInitialState(); } /** * Test the TrafficSignal's initial state. */ private void testInitialState () { System.out.println("testInitialState:"); System.out.println("Initial light: " + signal.light()); }

Testing TrafficSignal (cont.)

Testing TrafficSignal (cont.) 

Now let’s add a method to test the state changes. /** * Run the test. */ public void runTest () { testInitialState(); testChange(); } /** * Test the method change. */ private void testChange () { System.out.println("testChange:"); System.out.println("Starting light: " + signal.light()); signal.change(); System.out.println("After 1 change: " + signal.light()); signal.change(); System.out.println("After 2 changes: " + signal.light()); signal.change(); System.out.println("After 3 changes: " + signal.light()); }

Testing TrafficSignal (cont.) 

The TrafficSignal class is fairly trivial so there are not a lot of cases to consider.



Note that the methodology of designing the test cases (via the Test class) along with the TrafficSignal class promotes a test-driven incremental design.



Further note that by defining the test cases based on the specification before implementing the method, we can avoid being biased by the implementation.

Verification 

Consider the following simple Java method:

/** ** @require B >= 0 ** @ensure result == A * B **/ public int compute(int A, int B) { int x = 0; int m = A; int n = B; while (n > 0) { if ((n % 2) != 0) { x = x + m; } m = 2 * m; n = n / 2; } return x; }

Is this method correct?

Egyptian Numbering System Ahmes inscribed the “Rhind Papyrus” (~1850 BC) “… a thorough study of all things, insight into all that exists, knowledge of all obscure secrets …” Egyptian mathematics

Deciphering the Rhind Papyrus Rosetta Stone Contained a passage written in Greek, demonic, and hieroglyphics Thomas Young, a British physicist, and Jean Francois Champollion, a French Egyptologist, collaborated to decipher the hieroglyphic and demotic texts by comparing them with the known Greek text

Egyptian Multiplication “Halved” Multiplicand

“Doubled” Multiplier

Remainder

981

123 4

123 4

490

246 8

245

493 6

122

987 2

61

1974 4

30

3948 8

15

7897 6

7897 6

7

1579 52

1579 52

3

3159 04

3159 04

1

6318 08

6318 08

493 6 1974 4

12 105 54

Egyptian Multiplication (cont.) /** ** @require B >= 0 ** @ensure result == A * B **/ public int compute(int A, int B) { int x = 0; int m = A; int n = B; while (n > 0) { if ((n % 2) != 0) { x = x + m; } m = 2 * m; n = n / 2; } return x; }

Program Correctness  

Attempts to provide a more precise specification of the behavior of a method. Such a method specification includes two parts: • •

Any preliminary conditions that are required for the method to execute properly, known as the method’s precondition. The changes that result from executing the method, known the method’s postcondition.

Program Correctness (cont.) 

Taken together, the precondition and postcondition form a software contract. This contract states the following: IF

the calling code ensures the precondition is true at the time it calls the method

THEN the postcondition is guaranteed to be true at the time the method completes execution

Program Correctness (cont.) 

 

Preconditions and postconditions are logical expressions which describe states of the program variables. Given a method, the postcondition describes the expected outcome of its execution. The role of the precondition is to identify requirements for using the method so as to ensure that the postcondition is met. ►

Violating a precondition should be considered a logic error.

Program Correctness (cont.) 



To be valid, the precondition should define a state from which the method can produce the postcondition. It is reasonable to ask, what precondition will produce the desired postcondition? ►

To answer this, we will construct such a precondition starting with the postcondition.

Constructing Preconditions 

To construct a precondition for a method, we start with the postcondition and work backward to successively compute the precondition for each statement of the method. ►



At each step, we seek the broadest precondition that produces the desired postcondition.

The weakest precondition of a statement (or method) is the least restrictive precondition that will guarantee the validity of the associated postcondition for that statement (or method).

Constructing Preconditions (cont.) 

Consider the following code segment with postcondition: sum = 2 * x + 1; {sum > 1} The assertion {sum > 1} is the postcondition for the statement sum = 2 * x + 1; Possible preconditions are {x > 10}, {x > 50}, and {x > 1000}. The weakest precondition is {x > 0}.

The Assignment Axiom 

The basis for our technique is the assignment axiom, which allows us to perform a backward substitution.



Let V = E be a general assignment statement and Q be its postcondition. Formally, the assignment axiom is stated:

wp  V  E , Q   QV  E

which means that the constructed weakest precondition is Q with all instances of V replaced by E.

The Assignment Axiom (cont.) 

Consider the following assignment statement with postcondition:

a = b / 2 - 1; {a < 10} The weakest precondition is computed by substituting b / 2 – 1 for a into the assertion {a < 10}, thus b / 2 – 1 < 10 b / 2 < 11 b < 22 So {b < 22} is the constructed weakest precondition.

The Assignment Axiom (cont.) 

Consider the following assignment statement with postcondition: x = x - 3; {x > 0} Using the assignment axiom produces {x > 3} for the constructed weakest precondition.

Sequential Statements 



The weakest precondition for a block of statements can be constructed by successively backing over each of the statements in the block (starting with the last statement) and using the constructed weakest precondition of each statement as the postcondition to its preceding statement. The following Sequence Rule defines the constructed weakest precondition for a pair of statements: wp  C ; C , Q   wp C , wp  C , Q  1



2



1

2



Repeated applications of the Sequence Rule can be used for blocks containing more than 2 statements.

Sequential Statements (cont.) 

Consider the following sequence of statements with postcondition: y = 3 * x + 1; x = y + 3; {x < 10} The constructed weakest precondition for the last statement is: {y + 3 < 10} {y < 7}

Sequential Statements (cont.) 

This becomes the postcondition to the first statement: y = 3 * x + 1; {y < 7} The constructed weakest precondition for the last statement is: {3 * x + 1 < 7} {x < 2}

Sequential Statements (cont.) 

In practice, when deriving the precondition, we frequently write out the statements and the postcondition leaving blank lines between each statement. We work backwards to fill in the blank lines with the successive preconditions as shown below: y = 3 * x + 1; y = 3 * x + 1; {x < 2} x = y + 3; {y < 7} y = 3 * x + 1; {x < 10} x = y + 3; {y < 7} {x < 10} x = y + 3; {x < 10}

Sequential Statements (cont.) 

Consider the following code segment with postcondition: temp = x; x = y; y = temp; {x == b && y == a} It is supposed to swap the values of x and y.



Let’s verify that it does.

Sequential Statements (cont.) 

The construction would proceed as follows:

temp = x; temp = x; The constructed weakest x = y;precondition is: = x; temp {y == b && x == a} x ={yy;=={yb == == a} && bx && == temp a} temp = x; y = temp; {x == b && temp == a} = y; Comparingxthis with the {y that == b &&code temp == a} {x == postcondition, b y&&= ytemp; =={xa}== we bsee the && temp == a} x = values y; does, indeed, swap the of x {x == b y&& y == a} = temp; and y. {x == b && temp == a} {x == b && y == a} y = temp; {x == b && y == a}

Sequential Statements (cont.) 

Consider the following code segment with postcondition: y = 4; z = x + y; {z = 7} Let’s construct the weakest precondition that produces the stated postcondition. Working backward:

y = 4; {x == + 43} == 7} The constructed y = 4; weakest y7}= 4; {x + y == precondition is {x z = x + y;z = x + y;{x + y == 7} == 3}. {z == 7} {z == 7} z = x + y; {z == 7}

Conditional Statements 

Suppose we have the statement: {P} if (B) { S1 } else { S2 } {Q}

Conditional Statements (cont.) 

The if statement can take us from P to Q along either of two paths: truecase: P → B → S1 → Q falsecase: P → ~B → S2 → Q When working backward to construct P, we need to take into account each of these paths.

Conditional Statements (cont.) 

For truecase, backing over S1 leads to a precondition, call it P1. 





For execution to reach that point, the condition B must have been true. Backing over it gives us P1 ∧ B as a condition of executing the true path.

For falsecase, backing over S2 leads to a precondition, call it P2. 



For execution to reach that point, the condition B must have been false (i.e., ~B must have been true). Backing over ~B gives us P2 ∧ ~B as a condition of executing the false path.

Conditional Statements (cont.) 



To cover both paths, we want: P = (P1 ∧ B) ∨ (P2 ∧ ~B) as the precondition. The following Conditional Rule defines the constructed weakest precondition for a conditional statement:

wp  if  B  C1 else C2 , Q    wp  C1 , Q   B    wp  C2 , Q   B 

Conditional Statements (cont.) 

Let’s construct the weakest precondition for the following conditional: if (x > y) { y = x - 1; } else { y = x + 1; } {y > 0}

The truecase:

The falsecase: y = x - 1; {y > 0}

produces the precondition {x – 1 > 0} which simplifies to {x > 1}.

y = x + 1; {y > 0} produces the precondition {x + 1 > 0} which simplifies to {x > -1}.

disjoin of these is Backing over the The if condition, we get Backing over the negative of the if {((x > 1) && (x > y)) || ((x > -1) && y))} {(x > 1) && (x > y)}. condition, we(x get<={(x > -1) && (x <= which serves as a precondition of the if structure. y)}.

Conditional Statements (cont.) 

Let’s construct a precondition which ensures the correctness of the following code segment: Thus, the constructed precondition is {(n == 6) || false}, which simplifies to {n == 6}.

The truecase:

if (n >= 5) { y = n * n; } else { y = n + 1; } {y == 36}

The falsecase: y = n * n; {y == 36}

produces the precondition {n * n == 36} which simplifies to {n == 6 || n == -6}. Backing over the if condition, we get {(n == 6 || n == -6) && (n >= 5)} which simplifies to {n == 6}.

y = n + 1; {y == 36} produces the precondition {n + 1 == 36} which simplifies to {n == 35}. Backing over the negtive of the if condition, we get {(n == 35) && (n < 5)}. This is always false.

Conditional Statements (cont.) 

Show that the following code segment assigns the maximum of x and y to max: if (x >= y) { max = x; } else { max = y; }

We need to establish a postcondition that reflects the requirement that, after execution, the value of max is the larger of x and y. This can be stated as: (x >= y && max == x) || (x < y && max == y)

Conditional Statements (cont.) if (x >= y) { max = x; } else { max = y; } {(x >= y && max == x) || (x < y && max == y)}

The truecase: max = x; {(x >= y && max == x) || (x < y && max == y)} produces the precondition {(x >= y && x == x) || (x < y && x == y)} which simplifies to {(x >= y && true) || false} and further simplifies to {x >= y}. Backing over the if condition, we get {(x >= y) && (x >= y)} which simplifies to {x >= y}.

Conditional Statements (cont.) if (x >= y) { max = x; } else { max = y; } {(x >= y && max == x) || (x < y && max == y)}

The falsecase: max = y; {(x >= y && max == x) || (x < y && max == y)} produces the precondition {(x >= y && y == x) || (x < y && y == y)} which simplifies to {(y == x) || (x < y && true)} and further simplifies to {y >= x}. Backing over the negative of the if condition, we get {(y >= x) && (x < y)} which simplifies to {x < y}.

Conditional Statements (cont.) if (x >= y) { max = x; } else { max = y; } {(x >= y && max == x) || (x < y && max == y)}

Combining the results of each pass, we get: {(x >= y) || (x < y)} Since this is always true, it means that the code segment produces the postcondition for all values of x and y. We write the precondition as simply true.

Logical Pretest Loops 

Suppose we have the statement {P} while (G) { S } {Q}

where the guard G is a logical expression and S is the body of the loop. The while statement can take us from P to Q along any of a number of different paths, depending on how many times the condition G is true, including the path that goes directly from P to Q when the condition G is initially false.

Logical Pretest Loops (cont.) 





Executing a while loop involves repeatedly evaluating the guard G and executing the body S until the guard becomes false, at which time control passes to the statement after the loop. The condition that stops the loop is called the terminating condition and is normally more specific than the negative of the guard. Consider the code segment to the right. The negative of the guard is i >= 10, but the terminating condition is i == 10.

int i int s while { s = i = }

= 0; = 1; (i < 10) s * 2; i + 1;

The Reverse Execution Model 



To compute a precondition, we reverse execute the loop for several passes in an attempt to determine what must be true before the loop can be properly executed.  To begin the backward execution, we choose the condition that must be true after the loop has terminated. We know that after the loop has terminated, the postcondition Q and the terminating condition (which we call T) must be true.  Thus we start backing over the loop with the condition Q ∧ T.  Backing over the loop produces a condition that must be satisfied in order for the program to forward execute that pass of the loop.

The Reverse Execution Model (cont.) 

As a result of backing over the body of the loop, at the top of the body, the condition Q ∧ T will have been transformed into some other condition (which we will call A1). We know the guard G must also have been true in order for execution to have reached the top statement of the loop body, thus backing over the guard means the condition A1 ∧ G must have been true prior to that pass over the loop body. A1 ∧ G serves as a precondition for the last forward pass and a postcondition to the second backward pass over the loop. 



The Reverse Execution Model (cont.) 

Executing the second backward pass results in a condition A2 at the top of the body. Backing over the guard means A2 ∧ G must have been true prior to the program executing that forward pass over the loop. Repeated backward executions yields successive conditions A1 ∧ G , A2 ∧ G, A3 ∧ G , A4 ∧ G , A5 ∧ G , … 







Each of these conditions must have been true before the program could have executed the corresponding forward pass through the loop. From these conditions we determine the general pattern.

The Reverse Execution Model (cont.) 



The general pattern defines a condition which we call a loop invariant.  A loop invariant, I, is an assertion within a loop, evaluated prior to the loop guard, which is true every time execution reaches that position in the loop. The invariant must be true every time the while loop guard is encountered.  It is an assertion that is a precondition to each execution of the body and must also be true when the guard is encountered on the terminating pass.  That is, it must be true when the guard is true or the terminating condition is true.

Logical Pretest Loops (cont.) 

The following Loop Rule defines the precondition construction process for a conditional statement:

wp  while  B  C , Q     k  B    Q  B  

The following recursive definition defines the loop invariant Ik assuming the loop has a single terminating condition τ:

 wp  C , Q    n    wp  C ,  n 1  B 

if n  0 otherwise

Logical Pretest Loops (cont.) /** ** @require old.B B >= 0>= 0 ** @ensure result == A * B **/

(0 (old.B (0 == == (old.A 0) >= && 0) (old.B * old.B)–(old.A >= 0) * old.B)) && (B >= 0)

public int compute(int A, int B) { int x = 0;

(0 == (A*B)–(A*B)) && (B >= 0)

int m = A;

(x == (A*B)–(A*B)) && (B >= 0)

int n = B;

(x == (A*B)–(m*B)) && (B >= 0)

while (n > 0) {

(x == (A*B)–(m*n)) && (n >= 0)

if ((n % 2) != 0) { x = x + m; } m = 2 * m;

Loop invariant: (x == (A*B)–(m*n)) && (n >= 0)

n = n / 2; } return x; }

x == A * B result == A * B

Logical Pretest Loops (cont.) /** ** @require true ** @ensure result == N * N **/ true public int compute(int N) { if (N < 0) {

true ((N<<0) (N 0)|| &&(N (-N >=>= 0)0)) || (!(N < 0) && (N >= 0))

N = -N; }

true N >= && (N >= 0)&& (N && (0 == 0 (N*N–N*N) N*N–N–N*(N–1)) >= (N 0) >= 0)

int m = 0;

(0 == N*N–(N–m)–(N–m)*(N–m–1)) && (N >= m) (x == N*N–(N–m)–(N–m)*(N–m–1)) && (N >= m) (x == N*N–(N–m)*y–(N–m)*(N–m–1)) && (N >= m)

int x = 0; int y = 1; while (m < N) { x = x + y; y = y + 2;

Loop invariant: (x == N*N–(N–m)*y–(N–m)*(N–m–1)) && (N >= m)

m = m + 1; } return x; }

x == N * N result == N * N

How do we find an appropriate loop invaria