Void Safety
EECS3311: Software Design Fall 2017
CHEN-WEI WANG
1 2 3 4 5 6 7
1 2 3 4 5 6 7
Java Program: Example 2
1 2 3 4 5 6 7 8
class Point {
double x;
double y;
Point(double x, double y) {
this.x = x;
this.y = y; }
@Test
public void test2() {
PointCollector pc = new PointCollector(); Point p = null;
pc.addPoint(p);
p = pc.getPointAt(0);
assertTrue(p.x == 3 && p.y == 4); }
The above Java code compiles. But anything wrong?
L5 adds p (which stores null).
∴ NullPointerException when L7 calls p.x. 3 of 12
class PointCollector { ArrayList
points = new ArrayList<>(); } void addPoint(Point p) {
points.add(p); }
Point getPointAt(int i) {
return points.get(i); } }
Java Program: Example 1
11 22 33 44 55 66 77
The above Java code compiles. But anything wrong?
1 2 3 4 5 6
class Point {
double x;
double y;
Point(double x, double y) {
this.x = x;
this.y = y; }
@Test
public void test1() {
PointCollector pc = new PointCollector(); pc.addPoint(new Point(3, 4));
Point p = pc.getPointAt(0); assertTrue(p.x == 3 && p.y == 4); }
L3 calls PointCollector constructor not initializing points.
∴ NullPointerException when L4 calls L5 of PointCollector. 2 of 12
class PointCollector { ArrayList
points.add(p); }
Point getPointAt(int i) {
return points.get(i); } }
Java Program: Example 3
1 2 3 4 5 6 7
1 2 3 4 5 6 7 8 9
1 2 3 4 5 6 7 8
class PointCollector { ArrayList
points = new ArrayList<>(); } void addPoint(Point p) {
points.add(p); }
Point getPointAt(int i) {
return points.get(i); } }
class Point {
double x;
double y;
Point(double x, double y) {
this.x = x;
this.y = y; }
public void test3() {
PointCollector pc = new PointCollector();
Scanner input = new Scanner(System.in); System.out.println(“Ener an integer:”);
int i = input.nextInt();
if(i < 0) { pc = null; }
pc.addPoint(new Point(3, 4));
assertTrue(pc.getPointAt(0).x == 3 && pc.getPointAt(0).y == 4);
}
The above Java code compiles. But anything wrong?
NullPointerException when user’s input at L5 is non-positive. 4 of 12
Limitation of Java’s Type System
● A program that compiles does not guarantee that it is free from NullPointerExceptions :
○ Uninitialized attributes (in constructors).
○ Passing nullable variable as a method argument. ○ Calling methods on nullable local variables.
● The notion of Null references was back in 1965 in ALGO W.
● Tony Hoare (inventor of Quick Sort), introduced this notion of Null references “simply because it was so easy to implement”.
● But he later considers it as his “billion-dollar mistake”.
○ When your program manipulates reference/object variables whose
types include the legitimate value of Null or Void, then there is
always a possibility of having a NullPointerExceptions .
○ For undisciplined programmers, this means the final software
product crashes often! 5 of 12
Eiffel Program: Example 1
11 22 33 44 55 66 77 88 99
10 10 11 11 12 12 13 13
class
POINT
create
make
feature x: REAL y: REAL
feature
make (nx: REAL; ny: REAL)
do x := nx y := ny
end end
class
POINT_COLLECTOR_1
create
make
feature
points: LINKED_LIST[POINT]
feature
make do end
add_point (p: POINT)
do points.extend (p) end
get_point_at (i: INTEGER): POINT do Result := points [i] end
end
● Above code is semantically equivalent to Example 1 Java code. ● Eiffel compiler won’t allow you to run it.
∵ L8 does non compile
∴ It is void safe [Possibility of NullPointerException ruled out] 7 of 12
Eiffel’s Type System for Void Safety
● By default, a reference variable is non-detachable.
e.g., means that acc is always attached to some valid ACCOUNT point.
● VOID is an illegal value for non-detachable variables.
acc: ACCOUNT
⇒ Scenarios that might make a reference variable detached are considered as compile-time errors:
6 of 12
○ Variables can not be assigned to Void directly.
○ Non-detachable variables can only be re-assigned to
non-detachable variables.
e.g., ⇒
e.g., acc3: detachable ACCOUNT
compilable
acc2: ACCOUNT
acc := acc2
⇒
create acc.make
○ Creating variables (e.g.,
○ Non-detachable attribute not explicitly initialized (via creation or
) compilable assignment) in all constructors is non-compilable.
acc := acc3
non-compilable
Eiffel Program: Example 2
1 2 3 4 5 6 7 8 9
10 11 12 13
1 2 3 4 5 6 7 8 9
class
POINT
create
make
feature x: REAL y: REAL
feature
make (nx: REAL; ny: REAL)
do x := nx y := ny
end end
1 2 3 4 5 6 7 8 9
10 11 12 13
class
POINT_COLLECTOR_2
create
make
feature
points: LINKED_LIST[POINT] feature
make do create points.make end add_point (p: POINT)
do points.extend (p) end get_point_at (i: INTEGER): POINT
do Result := points [i] end end
test_2: BOOLEAN local
pc: POINT_COLLECTOR_2 ; p: POINT do
create pc.make
p := Void
p.add_point (p)
p := pc.get_point_at (0) Result := p.x = 3 and p.y = 4
end
10
● Above code is semantically equivalent to Example 2 Java code.
L7 does non compile ∵ pc might be void. [ void safe ] 8 of 12
Eiffel Program: Example 3
1 2 3 4 5 6 7 8 9
10 11 12 13
1 2 3 4 5 6 7 8 9
class
POINT
create
make
feature x: REAL y: REAL
feature
make (nx: REAL; ny: REAL)
do x := nx y := ny
end end
1 2 3 4 5 6 7 8 9
10 11 12 13
class
POINT_COLLECTOR_2
create
make
feature
points: LINKED_LIST[POINT] feature
make do create points.make end add_point (p: POINT)
do points.extend (p) end get_point_at (i: INTEGER): POINT
do Result := points [i] end end
test_3: BOOLEAN
local pc: POINT_COLLECTOR_2 ; p: POINT ; i: INTEGER do create pc.make
io.print ("Enter an integer:%N") io.read_integer
if io.last_integer < 0 then pc := Void end pc.add_point (create {POINT}.make (3, 4)) p := pc.get_point_at (0)
Result := p.x = 3 and p.y = 4
end
10
● Above code is semantically equivalent to Example 3 Java code.
L7 and L8 do non compile ∵ pc might be void. [ void safe ] 9 of 12
Beyond this lecture. . .
● Tutorial Series on Void Safety by Bertrand Meyer (inventor of Eiffel):
○ The End of Null Pointer Dereferencing ○ The Object Test
○ The Type Rules
○ Final Rules
● Null Pointer as a Billion-Dollar Mistake by Tony Hoare ● More notes on void safety
11 of 12
Lessons from Void Safety
● It is much more costly to recover from crashing programs (due to NullPointerException ) than to fix uncompilable programs.
e.g., You’d rather have a void-safe design for an airplane, rather than hoping that the plane won’t crash after taking off.
● If you are used to the standard by which Eiffel compiler checks your code for void safety , then you are most likely to write
Java/C/C++/C#/Python code that is void-safe (i.e., free from NullPointerExceptions).
10 of 12
Index (1)
Java Program: Example 1
Java Program: Example 2
Java Program: Example 3 Limitation of Java’s Type System Eiffel’s Type System for Void Safety Eiffel Program: Example 1
Eiffel Program: Example 2
Eiffel Program: Example 3
Lessons from Void Safety
Beyond this lecture. . . 12 of 12