Invariants

After writing an application, a programmer typically tests it thoroughly. Creating an exhaustive set of tests often is quite difficult, and it is always possible that a particular case remains untested. One technique that can help you test your programs thoroughly is to use invariants. An invariant is an assertion (see Section 13.13) that is true before and after the a portion of your code executes. Invariants are mathematical in nature and their concepts are more applicable to the theoretical side of computer science.

The most common type of invariant is a loop invariant. A loop invariant is an assertion that remains true

  • before the execution of the loop,
  • after every iteration of the loop body, and
  • when the loop terminates.

A properly written loop invariant, can help you code a loop correctly. There are four steps to developing a loop from a loop invariant.

  1. Set initial values for any loop control variables.
  2. Determine the condition that causes the loop to terminate.
  3. Modify the control variable(s) so the loop progresses toward termination.
  4. Check that the invariant remains true at the end of each iteration.

As an example, we will examine method linearSearch from class LinearArray in Fig. 16.2. The invariant for the linear search algorithm is:


       for all k such that 0 <= k and k < index
            data[ k ] != searchKey

For example, suppose index equals 3. If we pick any non-negative number less than 3 such as 1 for the value of k, the element in data at location k in the array does not equal the searchKey. This invariant basically states that the portion of the array, called a subarray, from the start of the array up to but not including the element at index does not contain the searchKey. A subarray can have no elements, or it can encompass the entire array.

According to Step 1, we must first initialize control variable index. From the invariant, we see that if we set index to 0, then the subarray contains zero elements. Therefore, the invariant is true because a subarray with no elements cannot contain a value that matches the searchKey.

The second step is to determine the condition that causes the loop to terminate. The loop should end after searching the entire arraywhen index equals the length of the array. In this case, no element of array data matches the searchKey. Once the index reaches the end of the array, the invariant remains trueno elements in the subarray (which in this case is the entire array) equal the searchKey.

For the loop to proceed to the next element, we increment control variable index. The last step is to ensure the invariant remains true after each iteration. The if statement (lines 2627 of Fig. 16.2) determines whether data[ index ] equals the searchKey. If so, the method finishes and returns index. Because index is the first occurrence of searchKey in data, the invariant is still truethe subarray up to index does not contain the searchKey.

Introduction to Computers, the Internet and the World Wide Web

Introduction to Java Applications

Introduction to Classes and Objects

Control Statements: Part I

Control Statements: Part 2

Methods: A Deeper Look

Arrays

Classes and Objects: A Deeper Look

Object-Oriented Programming: Inheritance

Object-Oriented Programming: Polymorphism

GUI Components: Part 1

Graphics and Java 2D™

Exception Handling

Files and Streams

Recursion

Searching and Sorting

Data Structures

Generics

Collections

Introduction to Java Applets

Multimedia: Applets and Applications

GUI Components: Part 2

Multithreading

Networking

Accessing Databases with JDBC

Servlets

JavaServer Pages (JSP)

Formatted Output

Strings, Characters and Regular Expressions

Appendix A. Operator Precedence Chart

Appendix B. ASCII Character Set

Appendix C. Keywords and Reserved Words

Appendix D. Primitive Types

Appendix E. (On CD) Number Systems

Appendix F. (On CD) Unicode®

Appendix G. Using the Java API Documentation

Appendix H. (On CD) Creating Documentation with javadoc

Appendix I. (On CD) Bit Manipulation

Appendix J. (On CD) ATM Case Study Code

Appendix K. (On CD) Labeled break and continue Statements

Appendix L. (On CD) UML 2: Additional Diagram Types

Appendix M. (On CD) Design Patterns

Appendix N. Using the Debugger

Inside Back Cover



Java(c) How to Program
Java How to Program (6th Edition) (How to Program (Deitel))
ISBN: 0131483986
EAN: 2147483647
Year: 2003
Pages: 615

Flylib.com © 2008-2020.
If you may any questions please contact us: flylib@qtcs.net