Transcript Slides

Pre- and postconditions
Using assertions and exceptions
Pre- and postconditions, Using
assertions and exceptions
1
Design by contract
• Idea
– A program is correct if given correct input the program
produces correct output.
• Correct input → PROGRAM → correct output
• A program is considered a kind of “black box”
• Same idea applies to parts of a program
– Methods, functions, etc.
– Correct input → METHOD → correct output
• Precondition
– Specification of correct input
• Postcondition
– Specification of correct output
Pre- and postconditions, Using
assertions and exceptions
2
Pre- and postconditions
• Statement that evaluates to true or false
• Many Java methods have a precondition
– Class.forName(String className)
• Assumes className != null
– Integer.parseInt(String s)
• Assumes s contains a number
– If you don’t respect the precondition the methods will most likely
throw some kind of (runtime) exception
• NullPointerException
• NumberFormatException
– A subclass of IllegalArgumentException
• In Java pre- and postconditions are not part of method
signatures
– You can specify pre- an postconditions as comments
Pre- and postconditions, Using
assertions and exceptions
3
Pre- and postconditions used with
method overriding
class S {
// pre: A; post: B
method(int p) { … }
}
• X can be less strong the A
• Y can be stronger than B
• Example
– A: p > 0 disallows 0
– X: p ≥ 0 allows 0
class T extends S {
// pre: X; post: Y
method(int p) { … }
}
– B
• result is true or false
• Example: Collection.add()
– Y
• result is always true
• Example: List.add()
Pre- and postconditions, Using
assertions and exceptions
4
Invariant
• An invariant is a statement that is
invariably true.
• Class invariant
– Statement about the objects state between
method invocation
• Loop invariant
– Statement about the state of variables in a
loop
Pre- and postconditions, Using
assertions and exceptions
5
Proof of post condition
• The idea of introducing pre- and postconditions
is to formally (mathematically) prove the
postcondition from the preconditions
– Postcondition & program implies post condition
• An invariant may help doing the proof.
– However, often the proof can be quite hard to do.
• Usually only done in critical systems
– Controlling hospital equipment, satellites, etc.
• Usually more errors in the proof than in the program
– But gives you a chance to rethink you program.
Pre- and postconditions, Using
assertions and exceptions
6
Assertions in Java
• Assertions is a relatively new feature if Java
– Since Java 1.4
– Prior to Java 1.4 programmers had to program their own
assertion facility. That is no longer necessary or advisable.
• New keyword: assert
– assert booleanExpression;
– assert booleanExpression : errorMessage;
• Example
if (direction == LEFT) { doLeft(); }
else if (direction == RIGHT) { doRight(); }
else
{ assert false : ”Bad direction”; }
Pre- and postconditions, Using
assertions and exceptions
7
Enabling assertions
• The Java compiler must be explicitly informed that you
have assertions in your program
– javac –source 1.4 SomeClass.java
• You tell the compiler that your source code is Java version 1.4
– Reason
• Assert is a new keyword. Some older program may have used
assert to name a variable or a method.
• The Java virtual machine (JVM) must be explicitly
informed to check assertions
– java –ea SomeClass
• -ea means “enable assertions”
– Reason
• Checking assertions takes time. You only want to check assertions
during testing and debugging, not when the program is running at
the customers site.
Pre- and postconditions, Using
assertions and exceptions
8
Enabling assertions in NetBeans
Pre- and postconditions, Using
assertions and exceptions
9
When not to use assertions
• Checking parameters to public methods
– Don’t use assertions to check parameters on public
methods
– Assertion checking disabled when the program is
running at the customers site.
– You cannot otherwise control the validity of
parameters to public methods.
– Check (using an if-statement) that the parameters are
valid. If not throw
• NullPointerException
• IllegalArgumentException, or one of its subclasses
Pre- and postconditions, Using
assertions and exceptions
10
When to use assertions
• Checking parameters to private methods
– You control who calls private methods.
– When things work (you are no longer
debugging) then you can safely disable
assertion checking.
• Checking conditions in methods
– Where parameters have been checked
without using exceptions.
Pre- and postconditions, Using
assertions and exceptions
11
References
• Ken Arnold et al The Java Programming
Language, 4th edition, Addison Wesley 2006
– 12.8 Assertions, page 296-303
• Sun Microsystems Programming with
Assertions
– http://java.sun.com/j2se/1.4.2/docs/guide/lang/assert.
html
• Qusay H. Mahmoud Using Assertions in Java
Technology, Sun Microsystems 2005
– http://java.sun.com/developer/technicalArticles/JavaL
P/assertions/
Pre- and postconditions, Using
assertions and exceptions
12