Specifications

Sun Services
Java™ Programming Language Module 8, slide 22 of 25
Copyright 2005 Sun Microsystems, Inc. All Rights Reserved. Sun Services, Revision F
Internal Invariants
The problem is:
1 if (x > 0) {
2 // do this
3 } else {
4 // do that
5}
The solution is:
1 if (x > 0) {
2 // do this
3 } else {
4 assert ( x == 0 );
5 // do that, unless x is negative
6}