DOC PREVIEW
CORNELL CS 211 - Program Correctness

This preview shows page 1-2 out of 5 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 5 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 5 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 5 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

CS211 Computers and ProgrammingMatthew Harris and Alexa Sharp July 25, 2002Program CorrectnessDefensive programming is like defensive driving: you take the attitude that younever know what the other drivers – or methods – are going to do, so you do whatyou can to prevent other people’s mistakes from hurting you. When programming,this means checking that parameters passed to your methods are valid and that theresults of your methods are reasonable.InvariantsRecall that a predicate is any statement that can be true or false. An invariant is apredicate that expected to be true at a particular point in your program but is notdirectly guaranteed by the language. For example, in the following code we expecti % 3 == 2 to be true in the last else block of the if statement, but that’s notguaranteed in the same way that the first two blocks have guarantees. If we want toincrease our confidence about our program’s correctness (and narrow down the setof possible bugs), we’d like to have Java check our invariants for us, at least untilwe’re satisfied in the correctness of our code. (In fact, this invariant is violated if i isever negative.)if (i % 3 == 0) {...} else if (i % 3 == 1) {...} else { // i % 3 == 2 here...}There are several kinds of invariants, and Java provides different mechanisms tocheck them.Preconditions of Public MethodsA precondition is an invariant that says something is true immediately before amethod (or some other unit of code) runs. Although we haven’t been requiringit in this course, preconditions of public methods should be carefully specified inthe documentation of a function. For example, in our implementation of HashSet,a precondition of add(o) was that o != null. The proper way to enforce pre-conditions of public methods in Java is to throw a runtime exception (such asIllegalArgumentException, IndexOutOfBoundsException, or NullPointerException).Recall that a runtime exception is a subclass of RuntimeException and that such ex-ceptions do not need to be declared in the throws clause of a method.For example, our HashSet add method looked like:public boolean add(Object o) {if (o == null) throw new NullPointerException("nulls disallowed");if (size == capacity)throw new RuntimeException("hash table full");...}1CS211 Computers and ProgrammingMatthew Harris and Alexa Sharp July 25, 2002Class InvariantsA class invariant (the name isn’t important) is an invariant that applies to all in-stances of a class at all times, except when an instance is transitioning from onestate to another. For example, in a priority queue implemented as a sorted list, aclass invariant is that the list is always sorted in increasing order by the keys of theelements.Exercise: Make a list of other class invariants we’ve seen. Think of lists, binarytrees, binary search trees, hash tables, stacks, queues, and heaps.Exercise: For each of the invariants you’ve listed, would you be able to write amethod that determines whether the invariant is properly satisfied? Write pseu-docode for a method to check the invariant of a binary seach tree.Although we’re using Java 1.3 in this course, Java 1.4 provides an assert state-ment that can be used to verify such invariants. The basic syntax isassert e;where e is a boolean expression. If the expression evaluates to false, the assertstatement will throw an AssertionError. Recall that Errors, as opposed to Exceptions,are normally not caught. This is appropriate here; if your queue implementation ex-pects the list to be sorted, and you suddenly discover that the list isn’t sorted, there’sreally no graceful way to recover because you don’t know when the problem oc-curred.Preconditions and PostconditionsNaturally, a postcondition is an invariant that is expected to be true at the end of amethod (or other unit of code). For example, in a method written to sort an array, apostcondition would be that the array is sorted.Any class invariants would normally be both preconditions and postconditions ofall of the public methods in your class. For example, the heap order property shouldbe satisfied before and after every enqueue and dequeue operation of our heap im-plementation. To check this I would write a method isOrderPropertySatisfied,and then at the beginning and end of enqueue and dequeue I would writeassert isOrderPropertySatisfied();I would also place this assertion at the end of the constructor.Exercise: Why would it be less appropriate to throw runtime exceptions when sucha class invariant is found violated?For the same reason, assert statements are the proper way to handle precondi-tions of private methods and postconditions (of any methods).If your language lacks built-in assertions, you can always fake it with an ifand a throw. But an important feature of the assertion facilities provided by mostlanguages is that they can be turned off. Some assertions can be very expensiveto check (such as checking that your list is sorted). Once you are satisfied thatyour program works, you can disable assertions, and then they won’t take any timeat runtime. In Java 1.4, you can disable assertions with the -disableassertionsoption to the Java runtime. (More advanced usage lets you selectively enable anddisable assertions.)2CS211 Computers and ProgrammingMatthew Harris and Alexa Sharp July 25, 2002Better than disabling assertions when you’re done is to comment out trivial orexpensive assertions but leave others in the code so that if a bug remains the programat least won’t continue running blindly.Because assertions can be disabled, you should never place in an assert state-ment any code that affects the correctness of your method.How does this relate to the unit testing we did?The purpose of unit testing is to verify the externally visible behavior of a class (ora larger unit of code). Unit testing is also called functional testing. Recall that wewrote unit tests in another class (such as BoggleBoardTest), so it didn’t have accessto private variables. All a unit test can do is call public constructors and publicmethods. Unit testing is also called black-box testing because the test doesn’t careabout how the class is implemented; we could completely change the implementationof BoggleBoard so that different class invariants apply, and our BoggleBoardTestshould still work.Assertions and other defensive programming techniques are a finer level of testingbecause we use them to verify the state of the program at individual lines within aclass.


View Full Document

CORNELL CS 211 - Program Correctness

Documents in this Course
B-Trees

B-Trees

10 pages

Hashing

Hashing

3 pages

Load more
Download Program Correctness
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Program Correctness and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Program Correctness 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?