Specifications

Sun Services
Java™ Programming Language Module 8, slide 24 of 25
Copyright 2005 Sun Microsystems, Inc. All Rights Reserved. Sun Services, Revision F
Postconditions and Class Invariants
For example:
1 public Object pop() {
2 int size = this.getElementCount();
3 if (size == 0) {
4 throw new RuntimeException("Attempt to pop from empty stack");
5 }
6
7 Object result = /* code to retrieve the popped element */ ;
8
9 // test the postcondition
10 assert (this.getElementCount() == size - 1);
11
12 return result;
13 }