Suppose the task is to store and manipulate geometric shapes, like those used in drawing editors. A point may be represented by a pair of integers, the x and y-coordinate, and a rectangle by the x and y-coordinates together with the width and height, which is expressed by the types Point
and Rectangle
:
Point = integer × integer
Rectangle = integer × integer × integer × integer
The operation of moving geometric shapes is then expressed by two functions, both called move
but distinguished by their parameter types:
move: Point × integer × integer → Point
move((x, y), dx, dy) = (x + dx, y + dy)
move: Rectangle × integer × integer → Rectangle
move((x, y, w, h), dx, dy) = (x + dx, y + dy, w, h)
Classes group data together with operations on that data. A class declaration consists of number of fields declaring the data, an initialization, and a number of methods defining the operations. Class Point
suggests to have x
and y
as fields and move
as a method:
algorithm
class Point
var x, y: integer
initialization(x0, y0: integer)
x, y := x0, y0
method move(dx, dy: integer)
x, y := x + dx, y + dy
As objects are created from a class, they are provided with an identity (name, reference). Declaring variable p
of class Point
allows it to hold the identity of a Point
object; classes are used as if they are types:
var p: Point
Above declaration implies that p
will always refer to a Point
object, but that object does not exist yet upon declaration. For this, an object has to be created, which executes the initialization with the supplied parameters:
p ← Point(3, 5)
The fields of an object are accessed and the methods are called using the dot notation. Continuing above, we have:
algorithm
{p.x = 3 ∧ p.y = 5}
p.move(–1, 1)
{p.x = 2 ∧ p.y = 6}
Methods, like procedures, can have result parameters:
algorithm
class Point
...
method distance(other: Point) → (d: integer)
d := abs(other.x – x) + abs(other.y – y)
Continuing from the statep.x = 2 ∧ p.y = 6
and assuming a: integer, q: Point
, we have:
algorithm
q ← Point(0, 7)
a ← p.distance(q)
{a = 3}
Methods calls are always of the form x.m(E)
or y ← x.m(E)
; the object x
is referred to as the receiver of the call.
By convention, in classes self
refers to the receiver and self.a
refers to field a
of the receiver. The fact that fields refer to the receiver object can be made explicit by prefixing them with self
:
algorithm
class Point
var x, y: integer
initialization(x0, y0: integer)
self.x, self.y := x0, y0
method move(dx, dy: integer)
self.x, self.y := self.x + dx, self.y + dy
method distance(other: Point) → (d: integer)
d := abs(other.x – self.x) + abs(other.y – self.y)
{d ≥ 0}
Thus the call p.move(3, 4)
assigns p
, 3
, 4
to self
, dx
, dy
before executing the method body. We leave out the prefix self
, to keep the syntax of field access like that of parameters.
Question: Why is d ≥ 0
a postcondition of method distance
?
Consider a class for rectangles with coordinates, width, and height such that width and height are "always" positive. This is expressed by a class invariant, written as an annotation in the class:
algorithm
class Rectangle
var x, y, w, h: integer
{w > 0 ∧ h > 0}
initialization(x0, y0, w0, h0: integer)
{w0 > 0 ∧ h0 > 0}
x, y, w, h := x0, y0, w0, h0
method move(dx, dy: integer)
x, y := x + dx, y + dy
method mirror()
w, h := h, w
method area() → (a: integer)
a := w × h
{a > 0}
Question: Assuming a Rectangle
object is created and its methods are called. How can you argue that area
always returns a positive result?
The class invariant is like a contract among the methods:
move
and mirror
guarantee w > 0 ∧ h > 0
at exit as they do not change w
, h
; method mirror
guarantees w > 0 ∧ h > 0
finally provided w > 0 ∧ h > 0
holds initially as it exchanges w
, h
.w > 0 ∧ h > 0
holds at exit as w
and h
are assigned values for which this is assumed.
</div>
This requires that the fields cannot be changed from the outside, i.e. the fields are read-only: they can still be read, as in:
algorithm
procedure equal(r, s: Rectangle) → (r: boolean)
r := (r.x, r.y, r.w, r.h) = (s.x, s.y, s.w, s.h)
Rule for correctness of classes:
Suppose class C
has fields f
, invariant I
over f
, and an initalization and methods mᵢ
, each with pre- and postconditions,
algorithm
class C
var f
{I}
initialization(v₀)
{P₀} S₀ {Q₀}
method mᵢ(vᵢ) → (rᵢ)
{Pᵢ} Sᵢ {Qᵢ}
where
P₀
is over v₀
Q₀
is over v₀
, f
Pᵢ
are over vᵢ
, f
Qᵢ
are over vᵢ
, rᵢ
, f
Class C
is correct if
I
,algorithm
{P₀} S₀ {I ∧ Q₀}
mᵢ
preserves I
:algorithm
{I ∧ Pᵢ} Sᵢ {I ∧ Qᵢ}
Here, I
is an object invariant as it ranges only over the fields of a single object.
Let RI ≡ w > 0 ∧ h > 0
be the object invariant of Rectangle
. Class Rectangle
is correct if
algorithm
{w0 > 0 ∧ h0 > 0} x, y, w, h := x0, y0, w0, h0 {RI}
move
, mirror
, area
preserve the invariant:algorithm
{RI} x, y := x + dx, y + dy {RI}
algorithm
{RI} w, h := h, w {RI}
algorithm
{RI} a := w × h {RI ∧ a > 0}
Exercise: Prove these four conditions!
Java has an assert statement that allows run-time checks to be included in programs:
assert B;
These can be turned on with the -ea
flag when running a program, e.g. java -ea classfile
; by default, assertion checking is turned off. Assertions can be split for readability,
assert B1 && B2;
is the same as
assert B1; assert B2;
Annotations and assertions are different:
It is good programming practice to have all or some annotations checked through assertions.
%%writefile Rectangle.java
class Rectangle {
private int x, y, w, h;
boolean invariantOK() {
return w > 0 && h > 0;
}
Rectangle(int x0, int y0, int w0, int h0) {
assert w0 > 0 && h0 > 0;
x = x0; y = y0; w = w0; h = h0;
assert invariantOK();
}
void move(int dx, int dy) {
x += dx; y += dy;
assert invariantOK();
}
void mirror() {
int t = w; w = h; h = t;
assert invariantOK();
}
int area() {
int a = w * h;
assert invariantOK();
assert a > 0;
return a;
}
}
!javac Rectangle.java
Question: Is it necessary to check the invariant at the beginning of each method?
In Rectangle
, all fields are private: if the invariant holds after the initialization and after each method, it is guaranteed to hold before each method as well.
Question: What is the class invariant of IntStack
? What are the required preconditions of the initialization and the methods? Add assertions for all relevant annotations!
%%writefile IntStack.java
class IntStack {
int n = 0; // 0 <= n <= a.length
int[] a; // a != null
IntStack(int capacity) {
a = new int[capacity];
}
void put(int x) {
// n < a.length
a[n] = x; n += 1;
}
int get() {
// n > 0
n -= 1; return a[n];
}
int size() {
return n;
}
}
!javac IntStack.java
Question: To ensure that the invariant is not invalidated, is it necessary to check the parameter of the initialization? Is it necessary to add assertions that the stack does not overflow or underflow? Is it recommendable to insert if
statements when the stack would overflow or underflow?
In a robust programming style, class invariants should always be maintained, even in the presence of exceptions.
capacity
is negative, new
will raise an exception and a
will not be assigned an array, i.e., it will remain null
, to which it is implicitly initialized. Thus an object with an invalid invariant is created. A solution would be to initialize a
to an array of length 0
before raising an assertion exception or to weaken the invariant to allow a
to be null
.put
is called, the assignment to a[n]
will raise an exception, but the invariant will still be maintained.get
is called, the assignment n -= 1
will invalidate the invariant before a[n]
raises an exception. A solution would be to rewrite get
asint get() {
int r = a[n]; n -= 1; return r;
}
if
statement, as invoid put(int x) {
if (n < a.length) {a[n] = x; n += 1;}
}
nil
Value¶If a variable may not refer to an object or some other value, it can be declared as optional and take the additional value nil
var p: opt Point
p := nil
Optional types can be expressed by disjoint union types, i.e. opt T = T | nil
. Optional field types allow recursive class declarations to be expressed, where one field is of the optional class itself (there is no recursion among methods involved):
class Polygon
var x, y: integer
var next: opt Polygon
initialization(x0, y0: integer)
x, y, next := x0, y0, nil
method add(x, y: integer)
next ← Polygon(x, y)
For example, C# uses the shorthand int? x
for a nullable integer type. Optional types can be found in Scala, F#. In Java, C/C++, and Python all object references always include a null
value, allowing recursive declarations as above without optional types. However, in that case, the type-system cannot guarantee the absence of dereferencing null
:
integer distance(Point p, Point q) {
return (q.x - p.x) + (q.y - p.y)
}
Above method can be called with p
or q
being null
, which leads to an exception. Java also has optional types, but they don't address this issue.
The declaration of class C
can abstractly be explained by variables and procedures. The statement v :∈ s
sets v
nondeterministically to an element of s
; the statement v :∉ s
set v
to an element not in s
. This is used to explain creating of an object as selecting a reference that is not already in use:
Let x: C
be an object of class C
. Accessing a field is just function application:
x.f = f(x)
A method call is a procedure call, where the type of the object (receiver) determines the procedure and the object becomes the self
parameter:
y ← x.m(E) = y ← C.m(x, E)
Above, C
has three roles:
x: C
as a type of variablesvar C: set of Object
as the set of created objects of class CC.m
for prefixing its methods, in case these names are used in other classes as well.This formal definition can be used to justify the rule for correctness of classes.
Question: In the following design, a line is meant to be pair of "different" points. What is the problem?
%%writefile TestLine.java
class Point {
int x, y;
Point(int x0, int y0) {
x = x0; y = y0;
}
void move(int dx, int dy) {
x += dx; y += dy;
}
}
class Line {
Point start, end;
boolean invariantOK() {
return start.x != end.x || start.y != end.y;
}
Line(Point s, Point e) {
assert s.x != e.x || s.y != e.y;
start = s; end = e;
assert invariantOK();
}
void move(int dx, int dy) {
start.move(dx, dy); end.move(dx, dy);
assert invarian` tOK();
}
}
class TestLine {
public static void main(String[] args) {
Point p = new Point(1, 3); Point q = new Point(2, 4);
Line l = new Line(p, q); p.move(1, 1);
assert l.invariantOK();
}
}
!javac TestLine.java; java -ea TestLine
Although the fields of line l
are not modified from outside, the class invariant is broken as the fields refer to objects that can be modified from outside l
.
Question: Making the fiels of Line
private will not help. How can breaking the class invariant be avoided?
boolean invariantOK() {
return start != null && end != null;
}
Line(Point s, Point e) {
assert s.x != e.x || s.y != e.y;
start = Point(s.x, s.y); end = Point(e.x, e.y);
assert invariantOK();
}
Class invariants can be over the fields of a class and over other objects provided that the other objects are owned.
Rule for correctness of classes:
Suppose class C
has fields f
, invariant I
over f
and owned objects, and an initalization and methods mᵢ
, each with pre- and postconditions,
algorithm
class C
var f
{I}
initialization(v₀)
{P₀} S₀ {Q₀}
method mᵢ(vᵢ) → (rᵢ)
{Pᵢ} Sᵢ {Qᵢ}
where
P₀
is over v₀
Q₀
is over v₀
, f
, and owned objectsPᵢ
are over vᵢ
, f
, and owned objectsQᵢ
are over vᵢ
, rᵢ
, f
, and owned objectsClass C
is correct if
I
,algorithm
{P₀} S₀ {I ∧ Q₀}
mᵢ
preserves I
:algorithm
{I ∧ Pᵢ} Sᵢ {I ∧ Qᵢ}
While ownership imposes a hierarchical structure on all objects, this does not preclude arbitrary structures among objects, as in the next example.
The Observer Pattern is one of the 23 design patterns of Design Patterns: Elements of Reusable Object-Oriented Software by Gamma, Helm, Johnson, Vlissides, 1994. Code for the pattern can be found in the standard Java and .Net libraries; templates for Python exist as well. Examples are:
In the Java example below, a subject has a state, here just an integer. One observer is interested in the whole state and another observed only if that integer is even.
%%writefile Observers.java
import java.util.*;
interface Observer {
void update();
}
class Subject {
int state = 0;
Set<Observer> obs = new HashSet<Observer>();
void attach(Observer o) {
obs.add(o);
}
void notifyObservers() {
for (Observer o: obs) o.update();
}
void modify() {
state += 1;
notifyObservers();
}
}
class ObserveAll implements Observer {
int state;
Subject sub;
ObserveAll(Subject s) {
sub = s; state = s.state;
}
public void update() {
state = sub.state;
System.out.println("state is " + state);
}
}
class ObserveEven implements Observer {
boolean even;
Subject sub;
ObserveEven(Subject s) {
sub = s; even = s.state % 2 == 0;
}
public void update() {
even = sub.state % 2 == 0;
if (even) System.out.println("state is even");
}
}
class TestObservers {
public static void main(String[] args) {
Subject sub = new Subject();
Observer oa = new ObserveAll(sub);
Observer oe = new ObserveEven(sub);
sub.attach(oa); sub.attach(oe);
sub.modify(); sub.modify(); sub.modify(); sub.modify();
}
}
!javac Observers.java; java TestObservers
As a set of observers is used, there is no guarantee in which order the observers are being notified.
Intuitively, establishing
oa.state == sub.state
is the goal of oa
,oe.even == (sub.state % 2 == 0)
is the goal of oe
.However,
even == (sub.state % 2 == 0)
is not an invariant of oa
, as at entry to update
, it does not holdsub
, as sub
does "not know" the fields of all of its observers.To express the goal as an invariant, a third class needs to be introduced:
%%writefile Controller.java
class Controller {
Subject sub = new Subject(); // owned
ObserveAll oa = new ObserveAll(sub); // owned
ObserveEven oe = new ObserveEven(sub); // owned
boolean invariantOK() {
return oa.state == sub.state &&
oe.even == (sub.state % 2 == 0);
}
Controller() {
sub.attach(oa); sub.attach(oe); assert invariantOK();
}
void modify() {sub.modify(); assert invariantOK();}
}
class TestController {
public static void main(String[] args) {
Controller c = new Controller();
c.modify(); c.modify(); c.modify(); c.modify();
}
}
!javac Controller.java; java -ea TestController