CSSE2002 — Week 12 Notes

Correct Programming

See csse2002 for course logistics. Lecture by Dr. Brae Webb.

Correctness is the prime quality. If a system does not do what it is supposed to do, everything else about it […] matters little.

— Bertrand Meyer, Object-Oriented Software Construction, §1.2 p.4, 1997

Today’s outline

Specification — what does it mean for a program to be correct?
Deriving preconditions — propagating a postcondition backward through code
Loop invariants — reasoning about (and designing) loops
Pragmatic considerations — when is this worth the effort?

All content is in java-hoare-logic and java-loop-invariants.

Applied class

See week12-tutorial-lambdas-and-streams — more practice with lambdas and streams, extending java-lambdas-and-streams (Week 11).

Practical

See week12-lab-generics — more practice with bounded generics and wildcards, extending java-generics (Week 9).

Next steps

CSSE3100 — Reasoning About Programs
Floyd, 1967 — Assigning Meanings to Programs
Hoare, 1969 — introduced the triple \(\{P\}\,S\,\{Q\}\)
Dijkstra, 1975 — weakest-precondition reasoning

Generics

Practical for 2026-05-21-correct-programming (Week 12). Extends java-generics (Week 9) with practice designing generic classes and using bounded wildcards.

Setup

A simple Bus domain models a class hierarchy of things that can ride a bus:

Bus <>--- Passenger
              ^
      +-------+-------+
      |               |
     Pet             Person
                       ^
              +--------+--------+
              |                 |
       TransportWorker   GeneralPublic
              ^                 ^
      +-------+-------+         |
      |               |         |
MaintenanceStaff   BusDriver  Concession

Passenger is the common supertype every rider implements/extends; Pet and Person are its two direct subtypes; TransportWorker (with subtypes MaintenanceStaff, BusDriver) and GeneralPublic (with subtype Concession) are both Persons. A Bus holds a collection of Passengers up to some capacity.

§1 Generic Bus

Task 0. The starting Bus class is not generic — it stores plain Passengers, so a single Bus instance could hold a mix of Pets and BusDrivers with no way to restrict it further:

public class Bus {
    private final List<Passenger> passengers;
    private final int capacity;

    public Bus(int capacity) {
        this.capacity = capacity;
        this.passengers = new ArrayList<>();
    }

    /**
     * @requires passenger != null
     * @ensures passenger is added to this bus and true is returned,
     *          unless this bus is already at capacity, in which case
     *          nothing changes and false is returned
     */
    public boolean addPassenger(Passenger passenger) {
        if (passengers.size() >= capacity) {
            return false;
        }
        passengers.add(passenger);
        return true;
    }

    public List<Passenger> getPassengers() {
        return passengers;
    }
}

Rewrite Bus to be generic, so a single Bus instance can be restricted to carrying just one kind of passenger (e.g. Bus<Pet>, Bus<BusDriver>).

Working

public class Bus<T> {
    private final List<T> passengers;
    private final int capacity;

    public Bus(int capacity) {
        this.capacity = capacity;
        this.passengers = new ArrayList<>();
    }

    /**
     * @requires passenger != null
     * @ensures passenger is added to this bus and true is returned,
     *          unless this bus is already at capacity, in which case
     *          nothing changes and false is returned
     */
    public boolean addPassenger(T passenger) {
        if (passengers.size() >= capacity) {
            return false;
        }
        passengers.add(passenger);
        return true;
    }

    public List<T> getPassengers() {
        return passengers;
    }
}

Task 1. As written, Bus<T> accepts any type argument at all — including types with nothing to do with Passenger (e.g. Bus<String>). Add a bound to T that restricts it to Passenger and its subtypes.

Working

public class Bus<T extends Passenger> {
    // ...unchanged from Task 0...
}

Bounding T extends Passenger restricts Bus’s type argument to Passenger or one of its subtypes (Pet, Person, TransportWorker, …), while a particular Bus instance still only carries one such type (e.g. Bus<Pet> can’t also hold a BusDriver). It also means code inside Bus<T> could safely call any Passenger method directly on a T value, if needed.

Task 2. Write a NoPetsBus<T> subclass of Bus<T> that statically (at compile time, not with a runtime check) excludes Pet as a valid type argument.

Working

public class NoPetsBus<T extends Person> extends Bus<T> {
    public NoPetsBus(int capacity) {
        super(capacity);
    }
}

Bounding the subclass’s type parameter to T extends Person (rather than Passenger) is stricter than Bus’s own bound. Since Pet is a Passenger but not a Person, NoPetsBus<Pet> simply doesn’t compile — the exclusion is enforced entirely by the type system, with no instanceof checks needed anywhere.

§2 Bus Stop

Task 3. Write a trainingBus method that takes a Bus<BusDriver> and a list of TransportWorkers, and adds every BusDriver among them to the bus (stopping early if the bus becomes full):

public static void trainingBus(Bus<BusDriver> bus, List<? extends TransportWorker> trainees) {
    ...
}

Working

/**
 * @requires bus != null && trainees != null
 * @ensures every BusDriver in trainees (in order) is added to bus,
 *          stopping as soon as bus is full
 */
public static void trainingBus(Bus<BusDriver> bus, List<? extends TransportWorker> trainees) {
    for (TransportWorker trainee : trainees) {
        if (trainee instanceof BusDriver busDriver) {
            boolean added = bus.addPassenger(busDriver);
            if (!added) {
                return;
            }
        }
    }
}

trainees only needs to be read from (never written to), so it takes the upper-bounded wildcard List<? extends TransportWorker> — this lets callers pass a List<TransportWorker>, List<BusDriver>, or List<MaintenanceStaff> alike, at the cost of the compiler only guaranteeing each element is at least a TransportWorker (hence the instanceof check before adding).

Task 4. Write a transferStudents method that moves every passenger out of a Bus<Concession> and into another bus that’s allowed to carry Concession passengers (or any of their supertypes):

public static void transferStudents(Bus<Concession> from, Bus<? super Concession> to) {
    ...
}

Working

/**
 * @requires from != null && to != null
 * @ensures passengers are moved from `from` into `to`, in order, until either
 *          `from` is empty or `to` is full (any remaining passengers stay in `from`)
 */
public static void transferStudents(Bus<Concession> from, Bus<? super Concession> to) {
    Iterator<Concession> iterator = from.getPassengers().iterator();
    while (iterator.hasNext()) {
        Concession passenger = iterator.next();
        boolean added = to.addPassenger(passenger);
        if (!added) {
            return;
        }
        iterator.remove();
    }
}

to only needs to be written to, so it takes the lower-bounded wildcard Bus<? super Concession> — this lets callers pass a Bus<Concession>, Bus<GeneralPublic>, Bus<Person>, or Bus<Passenger> alike, since all of them can legally accept a Concession passenger via addPassenger.

Task 5. transferStudents only works for exactly Bus<Concession> as its source. Generalise it into a fully generic method that works for Bus<T> for any T that’s at least a Concession.

Working

/**
 * @requires from != null && to != null
 * @ensures passengers are moved from `from` into `to`, in order, until either
 *          `from` is empty or `to` is full (any remaining passengers stay in `from`)
 */
public static <T extends Concession> void transferAllConcession(Bus<T> from, Bus<? super T> to) {
    Iterator<T> iterator = from.getPassengers().iterator();
    while (iterator.hasNext()) {
        T passenger = iterator.next();
        boolean added = to.addPassenger(passenger);
        if (!added) {
            return;
        }
        iterator.remove();
    }
}

Introducing the type parameter <T extends Concession> on the method itself (rather than fixing T = Concession) means from can be Bus<Concession> or any more specific subtype-bus (e.g. a hypothetical Bus<StudentConcession>), while to’s wildcard bound ? super T is resolved relative to whatever T the call site infers — transferStudents from Task 4 is just the special case where T is fixed to Concession.

Lambdas and Streams

Applied class for 2026-05-21-correct-programming (Week 12). Extends java-lambdas-and-streams (Week 11) with practice reading λ-function traces and standard functional interfaces (Function, BiFunction, Predicate, Supplier, Consumer, BiConsumer, UnaryOperator).

On the HTML site, fill in each blank with your answer, then click Run Code to check it. In the PDF, the Working callout is shown as a static answer key instead (interactive checking needs a browser).

§1 \(\lambda\)-functions

Task 0. What is printed by:

Function<Integer, Integer> f = x -> 2 * x;
System.out.println(f.apply(3));

Working

6

Task 1. What is printed by:

Supplier<String> c = () -> "Hello World";
System.out.println(c.get());

Working

Hello World

Task 2. What is printed by:

int power = 3;
Function<Integer, Double> g = x -> Math.pow(x, power);
System.out.println(g.apply(5));

Working

125.0 (\(5^3\))

Task 3. What is printed by:

int power = 3;
Function<Integer, Double> g = x -> Math.pow(x, power);
power = 2;
System.out.println(g.apply(5));

Working

Does not compile — power is reassigned after the lambda captures it, so it is not effectively final, which lambdas require of any local variable they capture.

Task 4. What is printed by:

Predicate<Integer> p = x -> x % 2 == 0;
System.out.println(p.test(4));

Working

true

Task 5. What is printed by:

BiFunction<Integer, Integer, Integer> add = (x, y) -> x + y;
System.out.println(add.apply(3, 5));

Working

8

Task 6. What is printed by:

Function<String, Integer> strLength = String::length;
System.out.println(strLength.apply("Hello"));

Working

5 — String::length is a method reference, equivalent to s -> s.length().

Task 7. What is printed by:

UnaryOperator<Integer> square = x -> x * x;
System.out.println(square.apply(4));

Working

16

Task 8. What is printed by:

int base = 2;
Function<Integer, Double> exp = x -> Math.pow(base, x);
System.out.println(exp.apply(3));

Working

8.0 (\(2^3\))

Task 9. What is printed by:

Function<Integer, Integer> factorial = n -> {
    int result = 1;
    for (int i = 2; i <= n; i++) {
        result *= i;
    }
    return result;
};
System.out.println(factorial.apply(4));

Working

24 (\(4! = 4 \\times 3 \\times 2 \\times 1\))

Task 10. What is printed by:

Function<Integer, Integer> f1 = x -> x + 1;
Function<Integer, Integer> f2 = x -> x * 2;
Function<Integer, Integer> composed = f1.andThen(f2);
System.out.println(composed.apply(3));

Working

8 — andThen runs f1 first (3 + 1 = 4), then f2 on that result (4 * 2 = 8).

Task 11. What is printed by:

List<Integer> numbers = new ArrayList<>();
Consumer<Integer> addTo = (number) -> numbers.add(number);

addTo.accept(24);
addTo.accept(42);
System.out.println(numbers);

Working

{24, 42}

Task 12. What is printed by:

Supplier<StringBuilder> supplier = StringBuilder::new;
BiConsumer<StringBuilder, String> appender = StringBuilder::append;
Consumer<StringBuilder> printer = System.out::println;

StringBuilder sb = supplier.get();
appender.accept(sb, "cher");
appender.accept(sb, "ryp");
appender.accept(sb, "ick");
printer.accept(sb);

Working

cherrypick

Task 13. What code snippet replaces ??? so this prints 10?

BiFunction<Integer, Function<Integer, Integer>, Supplier<Integer>> g =
    (i, f) -> ??? ;
System.out.println(g.apply(5, x -> x * 2).get());

Working

() -> f.apply(i) — g returns a Supplier<Integer>, a zero-argument lambda that, when later called via .get(), applies f to i (5 * 2 = 10).

Task 14. What is printed by:

Function<Integer, Integer> f = x -> x * 2;
UnaryOperator<Integer> g = x -> x + 1;
Function<Integer, Integer> h = f.andThen(g).andThen(f).andThen(g);
System.out.println(h.apply(3));

Working

15 — chained left to right: f(3)=6, g(6)=7, f(7)=14, g(14)=15.

§2 Streams

Task 15. What is the value of:

Stream.of(1, 2, 3, 4, 5, 6, 7, 8).filter(x -> x % 2 == 0).toList();

Working

{2, 4, 6, 8}

Task 16. What is the value of:

Stream.of(1, 2, 3, 4, 5, 6, 7, 8).map(x -> x * x).toList();

Working

{1, 4, 9, 16, 25, 36, 49, 64}

Task 17. What is the value of:

List<String> list = Arrays.asList("apple", "banana", "cherry");
list.stream()
    .map(String::toUpperCase)
    .filter(s -> s.startsWith("A"))
    .forEach(System.out::println);

Working

APPLE — only "apple" survives the startsWith("A") filter once upper-cased.

Task 18. What is the value of:

Stream<Integer> stream = Stream.iterate(1, n -> n * 2).limit(5);
Integer result = stream.reduce(0, (a, b) -> a + b);
System.out.println(result);

Working

31 — Stream.iterate(1, n -> n * 2).limit(5) produces 1, 2, 4, 8, 16, and \(1+2+4+8+16 = 31\).

Task 19. Convert the following method into streams:

static int sumOfSquareNumbers(List<String> words) {
    int sum = 0;
    for (String word : words) {
        if (word.matches("[0-9]+")) {
            int number = Integer.parseInt(word);
            if (Math.sqrt(number) == Math.floor(Math.sqrt(number))) {
                sum += number;
            }
        }
    }
    return sum;
}

Working

static int sumOfSquareNumbers(List<String> words) {
    return words.stream()
        .filter(word -> word.matches("[0-9]+"))
        .mapToInt(Integer::parseInt)
        .filter(number -> Math.sqrt(number) == Math.floor(Math.sqrt(number)))
        .sum();
}

Task 20. What does this print?

List<String> words = Arrays.asList("cat", "dog", "elephant", "giraffe");
String details = words.stream()
        .reduce("", (word1, word2) -> word1 + "-" + word2);
System.out.println(details);

Working

-cat-dog-elephant-giraffe — the identity "" is the first word1, so even the first element gets a leading - prepended.

Task 21. What does this print?

Stream<String> stream = Stream.of("hello", "world", "java");
stream.map(String::toUpperCase)
      .forEach(System.out::print);

Working

HELLOWORLDJAVA — print (not println) concatenates every element with no separator.

Reference material

Java Generics

Introduced in 2026-04-30-generics-in-java (Lecture, Week 9).

Why generics?

Prior to Java 1.5, collection classes could hold any type of object — ArrayList.add(Object o) accepted anything, allowing types to be mixed, but required an explicit cast when retrieving elements:

List list = new ArrayList();
list.add("Hello");
list.add(123);           // allowed
String str = (String) list.get(0);   // OK, but no compile-time guarantee
Integer num = (Integer) list.get(1);

There was no guarantee only one type would end up in the collection, since add accepted any Object — a String could silently get mixed into a list that was only ever meant to hold Cars. Generics let a class/interface/method declare which type(s) it works with, giving:

List<Car> carList = new ArrayList<Car>(); // or new ArrayList<>() - the diamond operator
carList.add("Not a product"); // compile-time error, not a runtime surprise
Car c = carList.get(0);       // no cast needed - the compiler already knows it's a Car

This is called type safety — catching and preventing type-related errors early (at compile time), rather than allowing unintended bugs (a stray ClassCastException) to surface at runtime.

Generic classes

A generic class parameterises a type across its whole body:

public class Print<T> {
    T i;
    Print(T i) { this.i = i; }
    public void print() { System.out.println(i); }
}

Print<Integer> p1 = new Print<>(1);
Print<Double> p2 = new Print<>(1.1);
Print<String> p3 = new Print<>("1.1");

By convention, type parameters are single letters: T (Type), E (Element — used throughout the Collections Framework), K (Key), V (Value), N (Number), and S/U/V… for a 2nd/3rd/4th type parameter.

Generic methods

A single method (rather than a whole class) can be made generic, independently of whether its enclosing class is generic:

public <T> void print(T data) {
    System.out.println("Lets shout " + data + "!!!");
}
// print(124);              // T inferred as Integer
// print("I love CSSE2002"); // T inferred as String

The compiler determines T from the argument’s type automatically — this is type inference. Multiple type parameters can be declared together: public <T, S, R> R genericMethod(T value1, S value2) { ... }.

Bounded generics

A type parameter can normally accept any reference type. Bounded generics restrict it to a specific type (or one of its subtypes) using extends:

public <T extends Number> void print(T data) {
    System.out.println("Lets shout " + data + "!!!");
}
// print(123);    // OK, Integer is a Number
// print(123.2);  // OK, Double is a Number
// print("123");  // compile-time error, String is not a Number

<T extends X> means T can only accept data that are subtypes of X (despite the keyword, this works the same way whether X is a class or an interface).

Bounds through wildcards

Wildcards (?) bound what types can be substituted for a generic type parameter at the use site (e.g. in a method parameter), rather than when a generic class/method is declared.

Unbounded wildcard: `List<?>`

List<?> means “a list of some unknown type”. Since Java doesn’t know whether it’s actually List<String>, List<Integer>, or something else, it prevents writes:

public static void addSomething(List<?> list) {
    list.add("Hello"); // compile-time error - could break whatever the real element type is
}

Use <T> when the method needs to work with the type; use <?> when the method only needs to read values (e.g. a printList that only calls .get()/iterates never needs to know the concrete type).

Upper bounded wildcard: `? extends T`

Represents T or any subclass of T. Used mainly to read data — you can’t safely add to it, because the method doesn’t know the exact subtype:

List<? extends Number> nums = new ArrayList<Integer>();
Number n = nums.get(0); // OK: read as Number
nums.add(10);           // compile-time error - could be a List<Double>, etc.

This matters because generics in Java are invariant: even though Double is a subclass of Number, List<Double> is not a subclass of List<Number> (Effective Java, Item 31: parameterized types are invariant — List<Type1> is neither a subtype nor a supertype of List<Type2>). So a method that should accept a List<Integer> or a List<Double> and only needs to read Numbers from it must be written as:

public static double sum(List<? extends Number> list) {
    double sum = 0;
    for (Number n : list) {
        sum += n.doubleValue();
    }
    return sum;
}

Lower bounded wildcard: `? super T`

Represents T or any of its superclasses. Used when you want to write to a generic collection while keeping some flexibility in what type of collection is accepted:

public static void addNumbers(List<? super Integer> list) {
    list.add(1);
    list.add(2);
}
// addNumbers(new ArrayList<Number>());  // OK, Number is a superclass of Integer
// addNumbers(new ArrayList<Object>());  // OK, Object is a superclass of Integer
// addNumbers(new ArrayList<Double>());  // compile-time error, Double isn't a superclass of Integer

Wildcards are usually bounded (? extends T, ? super T) rather than left fully unbounded, to reduce flexibility just enough to improve type safety.

Type erasure

Generics only provide type checking at compile time — Java implements them via type erasure, which removes all type parameter information during compilation. Each type parameter is replaced with:

its upper bound (e.g. Number, if declared <T extends Number>), or
Object, if unbounded.

As a result, generic type information is not available at runtime — a compiled List<String> and a compiled List<Integer> are the same erased List class. This is why the compiler needs to insert a hidden cast for you:

// Source (compile time)
List<String> list = new ArrayList<>();
list.add("Hello");
String s = list.get(0);

// After erasure (what actually runs)
List list = new ArrayList();
list.add("Hello");
String s = (String) list.get(0); // compiler inserts this cast

For a bounded type parameter, the compiler substitutes the bound itself:

// Source
class SomeClass<T extends Number> {
    private T t;
    public void add(T t) { this.t = t; }
    public T get() { return t; }
}
// After erasure
class SomeClass {
    private Number t;
    public void add(Number t) { this.t = t; }
    public Number get() { return t; }
}

Practical example: a bookshop

A bookshop sells books across genres (Fiction, Action, Fantasy, …), stored on shelves; the shop needs to store and retrieve books of these different genres.

Without generics

A single BookShelf storing the abstract Book type loses genre information on retrieval — every getItem() call needs an explicit (unsafe) cast back to the specific genre:

public class BookShelf {
    private List<Book> inventory = new ArrayList<>();
    public void addItem(Book item) { inventory.add(item); }
    public Book getItem(int index) { return inventory.get(index); }
}
// Fiction f = (Fiction) shelf.getItem(0); // risk of ClassCastException, not type safe

Writing separate FictionShelf/ActionShelf classes fixes the type safety but duplicates the whole class for every genre.

With generics

A single generic BookShelf<T extends Book> gives type safety and reuse in one class:

public class BookShelf<T extends Book> {
    private List<T> inventory = new ArrayList<>();
    public void addItem(T item) { inventory.add(item); }
    public T getItem(int index) { return inventory.get(index); }
    public void displayBooks() {
        for (T book : inventory) {
            System.out.println(book + "(" + book.getGenre() + ")");
        }
    }
}

BookShelf<Fiction> fictionShelf = new BookShelf<>();
BookShelf<Action> actionShelf = new BookShelf<>();
fictionShelf.addItem(new Fiction("The Hobbit", "J.R.R. Tolkien"));
actionShelf.addItem(new Action("Die Hard", "Roderick Thorp"));
fictionShelf.displayBooks(); // getItem() on fictionShelf now returns Fiction directly, no cast

Java Hoare Logic

Introduced in 2026-05-21-correct-programming (Lecture, Week 12). Formalises reasoning about java-specification’s preconditions/postconditions.

What does it mean for a program to be correct?

A correct program satisfies its specification.

Correctness is only meaningful relative to a specification — asking “is this program correct?” without one is unanswerable:

public int indexOf(int[] numbers, int number) {
    for (int i = 0; i < numbers.length; i++) {
        if (numbers[i] == number) {
            return i;
        }
    }
    return -1;
}

With no spec at all: maybe correct, maybe not — we can’t say without knowing what it’s meant to do.
Spec’d as /** Returns how many times number occurs in numbers. */: incorrect — counter-example indexOf({1, 1, 1, 1}, 1) == 0, but a correct implementation of that spec should return 4.
Spec’d as /** Returns the index of number within numbers, if number is in numbers. */: correct, but the spec is underspecified — it says nothing about what happens when number isn’t in numbers.

A specification restricts the space of acceptable implementations: think of all possible input/output pairs as arrows crossing an Implementation/Specification boundary — an implementation is correct exactly when every arrow it draws stays within the region the specification permits. A @requires/@ensures Javadoc comment (see java-specification) states the precondition and postcondition that bound this region.

Hoare triples

Preconditions and postconditions aren’t just for whole methods — every block of code has them. We write this as a Hoare triple:

\[\{P\}\ S\ \{Q\}\]

meaning: if precondition \(P\) holds before statement(s) \(S\) run, postcondition \(Q\) holds afterwards. E.g.:

// {true}
if (x > y) {
    max = x;
} else {
    max = y;
}
// {max >= x && max >= y}

Deriving preconditions by propagating backward

Given a method’s postcondition, we can work out its precondition (or verify a block of code) by propagating the postcondition backward through each statement, substituting as we go.

Straight-line code

/**
 * @requires numbers != null && 2 < numbers.length && numbers[2] == number
 * @ensures numbers[\result] == number
 */
public int indexOf(int[] numbers, int number) {
    // {numbers[0 - 10 + 12] == number}
    int result = 0;
    // {numbers[result - 10 + 12] == number}
    result = result + 12;
    // {numbers[result - 10] == number}
    result = result - 10;
    // {numbers[result] == number}
    return result;
    // {numbers[\result] == number}
}

Each line’s precondition is obtained by substituting the assigned expression into the next line’s already-derived precondition, working from the @ensures postcondition backward to the top of the method — the resulting @requires is whatever’s left once you reach the very first line.

Through `if`/`else`

Each branch is handled separately, and the two derived preconditions are combined into a single condition depending on which branch executes:

/**
 * @requires numbers != null && 12 < numbers.length
 *               && numbers[12] == number && number % 2 == 0
 * @ensures numbers[\result] == number
 */
public int indexOf(int[] numbers, int number) {
    // {number % 2 == 0 ==> numbers[0 + 12] == number
    //  && number % 2 != 0 ==> numbers[0 - 10] == number}
    int result = 0;
    if (number % 2 == 0) {
        // {numbers[result + 12] == number}
        result = result + 12;
    } else {
        // {numbers[result - 10] == number}
        result = result - 10;
    }
    // {numbers[result] == number}
    return result;
}

Proving a block correct

The same backward-propagation technique proves an arbitrary block of code satisfies a given Hoare triple — substitute back through each branch/statement and confirm the starting precondition (true, in these examples) is actually implied:

// {true}
if (x > y) {
    // {x > y} ==> {x >= x && x >= y}
    max = x;
    // {max >= x && max >= y}
} else {
    // {y >= x} ==> {y >= x && y >= y}
    max = y;
    // {max >= x && max >= y}
}
// {max >= x && max >= y}

A three-statement swap works the same way, substituting each assignment’s right-hand side backward through \old(...) references:

// {true}
// {y == \old(y) && x == \old(x)}
int tmp = x;
// {y == \old(y) && tmp == \old(x)}
x = y;
// {x == \old(y) && tmp == \old(x)}
y = tmp;
// {x == \old(y) && y == \old(x)}

A trickier variant swaps x/y using only arithmetic (no temporary variable), which still propagates the same way:

// {true}
// {y == \old(y) && x == \old(x)}
// {y - (y - x) + (y - x) == \old(y) && y - (y - x) == \old(x)}
x = y - x;
// {y - x + x == \old(y) && y - x == \old(x)}
y = y - x;
// {y + x == \old(y) && y == \old(x)}
x = y + x;
// {x == \old(y) && y == \old(x)}

(A similar swap is possible using bitwise XOR instead of subtraction, exploiting \(a \oplus b = b \oplus a\), \((a \oplus b) \oplus c = a \oplus (b \oplus c)\), \(a \oplus 0 = a\), \(a \oplus a = 0\).)

Java Lambdas and Streams

Introduced in 2026-05-14-lambdas-streams-and-events (Guest lecture, Week 11).

Lambdas (anonymous functions)

A lambda is a function treated as a value — it isn’t declared with a name, and can be passed around like any other reference value (similar to anonymous functions in Python or JavaScript).

Scope: like in most languages, a Java lambda can hold references to things accessible in scope at the point it’s created.

Functional interfaces

Because Java is statically typed, a lambda can’t exist without a clearly-defined type — the JVM needs to know its shape. Java provides a family of generic functional interfaces (in java.util.function) to describe common lambda shapes; four commonly used ones:

Interface	Signature	Purpose
`Consumer<T>`	takes a `T`, returns nothing	has some side effect (returning nothing and having no side effect would mean doing nothing at all)
`Predicate<T>`	takes a `T`, returns `boolean`	useful for filtering
`Function<T, R>`	takes a `T`, returns an `R`	general transform
`BiFunction<T, U, R>`	takes a `T` and a `U`, returns an `R`	deriving one value from two, e.g. distance between two positions, or a custom comparator/sort key

Consumer<String> print = s -> System.out.println(s);
Predicate<Integer> isEven = n -> n % 2 == 0;
Function<String, Integer> length = s -> s.length();
BiFunction<Integer, Integer, Integer> add = (a, b) -> a + b;

Streams

Added in Java 8 to enable a more declarative style of programming — particularly effective when you need to run multiple operations over data sequentially, or reduce a sequence of operations down to a single resulting value (a very common real-world task). Streams are Java’s answer to the same idea as JavaScript’s .filter()/.map()/.reduce(): an alternative to writing many near-identical for loops.

int totalHpFromFireEnemies =
    enemies.stream()
        .filter(enemy -> enemy.faction.equals("Fire"))
        .mapToInt(enemy -> enemy.hp)
        .sum();

Anatomy of a stream pipeline

Start a stream from a collection: .stream().
Chain any number of intermediate operations, each producing a new stream: .filter(), .map(), .distinct(), .sorted(), .mapToInt(), …
Resolve the stream into a final value with exactly one terminal operation: .sum(), .count(), .toList(), .collect(), .reduce(), …

In the example above: enemies.stream() starts the pipeline; .filter(...) keeps only Fire-faction enemies; .mapToInt(...) transforms each remaining Enemy into its int hp; .sum() (terminal) reduces the stream of hp values down to a single total.

Java Loop Invariants

Introduced in 2026-05-21-correct-programming (Lecture, Week 12). Extends java-hoare-logic’s backward-reasoning technique to loops, where the number of iterations isn’t known up front.

…proving the correctness of algorithms has another aspect that is even more important: it mirrors the way we understand an algorithm.

— Donald Knuth, The Art of Computer Programming (Vol. 1), 1997

What is an invariant?

An invariant is a property of a system that does not change.

Motivating puzzle

A jar contains 100 red and 100 blue beans. Repeatedly: pick two random beans; if they’re the same colour, discard both; if they’re different colours, discard the blue one. What colour is the last bean?

Let \(r, b\) be the current counts of red/blue beans. Each step does exactly one of:

Pick	Action	Effect
two reds	discard both	\(r \mapsto r - 2,\ b \mapsto b\)
two blues	discard both	\(r \mapsto r,\ b \mapsto b - 2\)
one of each	discard blue	\(r \mapsto r,\ b \mapsto b - 1\)

What never changes? The parity of \(r\) — every action either leaves \(r\) unchanged or decreases it by exactly 2, so \(r\) stays even throughout (it starts at 100, itself even). When one bean remains, \(r + b = 1\); since \(r\) must be even, \(r \neq 1\), so \(r = 0\) and \(b = 1\) — the last bean is blue.

The property “\(r\) is even” is an invariant of the process: it (1) holds before any step, (2) is preserved by every step, and (3), combined with the termination condition (\(r + b = 1\)), implies what we wanted to prove. This is exactly the structure of a loop invariant.

Loop invariants

A loop invariant is a condition that: (1) holds before the loop is entered, (2) is preserved by each iteration, and (3) combined with the negation of the guard, implies the postcondition.

int count = 0;
while (count < n) {
    // invariant: count >= 0
    count = count + 1;
}

// {0 >= 0}
int count = 0;
// {count >= 0}                    <-- invariant holds before the loop
while (count < n) {
    // invariant: count >= 0
    // {count + 1 >= 0}
    count = count + 1;
    // {count >= 0}                <-- preserved by the body
}
// {count >= 0 && count >= n}

Deriving an invariant for `power`

/**
 * @requires ????
 * @ensures \result == base^exp
 */
int power(int base, int exp) {
    int result = 1;
    int i = 0;
    while (i < exp) {
        result = result * base;
        i = i + 1;
    }
    return result;
}

Step 1 — guess an invariant. Replace exp in the postcondition with the loop variable i: \(I : \text{result} = \text{base}^i\).

Step 2 — verify. Three checks:

Does \(I\) hold before the loop first executes? result = base^i \(\equiv 1 = \text{base}^0 \equiv\) true. ✓
Assuming \(I\) holds at the top of the loop body, does it still hold after? result * base = base^i * base = base^{i+1}, and after i = i + 1, that’s exactly result = base^i again. ✓
Does \(I\) combined with the negated guard (\(i \geq \text{exp}\)) imply the postcondition? result = base^i \(\land\ i \geq \text{exp} \Rightarrow \text{result} = \text{base}^{\text{exp}}\)? Not quite — we can only conclude \(i \geq \text{exp}\), but we need \(i = \text{exp}\).

Step 3 — strengthen. Add the bound \(i \leq \text{exp}\) to the invariant: \(I : \text{result} = \text{base}^i \land i \leq \text{exp}\). Re-checking: \(I\) now holds initially iff \(\text{exp} \geq 0\) (giving us our precondition), is still preserved by the loop body, and combined with \(i \geq \text{exp}\) now forces \(i = \text{exp}\) exactly, giving the postcondition:

/**
 * @requires exp >= 0
 * @ensures \result == base^exp
 */
int power(int base, int exp) {
    // {0 <= exp}
    // {1 == base^0 && 0 <= exp}
    int result = 1;
    int i = 0;
    // {result == base^i && i <= exp}
    while (i < exp) {
        ...
    }
    // {result == base^i && i <= exp && i >= exp}
    // {result == base^exp}
    return result;
}

Designing an algorithm from an invariant: fast exponentiation

The power above runs in \(O(\text{exp})\) multiplications. We can do better using the identity:

\[b^e = \begin{cases} (b^{e/2})^2 & \text{if } e \text{ is even} \\ b \times (b^{(e-1)/2})^2 & \text{if } e \text{ is odd} \end{cases}\]

E.g. computing \(3^{13}\): \(3^{13} = 3 \times 3^{12}\) [13 odd] \(= 3 \times (3^2)^6\) [12 even] \(= 3 \times 9^6 = 3 \times (9^2)^3\) [6 even] \(= 3 \times 81^3 = 3 \times 81 \times 81^2\) [3 odd] \(= 3 \times 81 \times 6561 = 1{,}594{,}323\) — only a handful of multiplications instead of 12 sequential ones.

Design from the invariant: rather than writing code and then finding its invariant, pick the invariant first and let the code follow. We want a loop maintaining:

\[I : \text{result} \times b^e = \text{base}^{\text{exp}}\]

starting from result = 1, b = base, e = exp, terminating when e == 0:

/**
 * @requires exp >= 0
 * @ensures \result == base^exp
 */
int power(int base, int exp) {
    int result = 1;
    int b = base;
    int e = exp;
    while (e > 0) {
        // invariant: result * b^e == base^exp
        if (e % 2 == 1) {
            result = result * b;
            e = e - 1;
        }
        b = b * b;
        e = e / 2;
    }
    return result;
}

Verifying \(I\) (using \(b^e = (b^{e/2})^2\) when even, \(b \times (b^{(e-1)/2})^2\) when odd, and \((a^b)^c = (a^c)^b\)):

Before the loop: result * b^e == base^exp \(\equiv 1 \times \text{base}^{\text{exp}} = \text{base}^{\text{exp}} \equiv\) true. ✓
Through the body: splitting on e % 2, both branches reduce back to exactly result * b^e == base^exp after the update (the if branch peels off one factor of b into result and decrements e first; both branches then square b and halve e). ✓
On exit (e <= 0): result * b^e == base^exp with e <= 0 only concludes the postcondition when e >= 0 too (i.e. e == 0) — which holds as long as exp >= 0, giving the same precondition as before. ✓

This preserves the exact same specification as the slow version — both satisfy @requires exp >= 0 / @ensures \result == base^exp — but the fast version reaches it in \(O(\log \text{exp})\) multiplications instead of \(O(\text{exp})\).

Pragmatic considerations

Proving correctness can be vital, but it’s also time-consuming — you want code running on a plane or controlling trains to be correct; you may not care nearly as much whether a weekend web-scraping script is correct. Where formal reasoning tends to pay off:

Combinatorial algorithms — proving a faster/trickier implementation still satisfies the original spec (as with power above).
Distributed and concurrent algorithms — notoriously hard to reason about by testing alone (see CSSE3610/7610).

Reasoning about programs this way provides (1) a more rigorous way to think about your software, and (2) a better interface design for others to interact with it — it doesn’t remove the need to think about your programs, but gives a framework to structure that thinking.

Beware of bugs in the above code; I have only proved it correct, not tried it.

— Donald Knuth (memo to Peter van Emde Boas, 1977)

Correct Programming

Today’s outline

Applied class

Practical

Next steps

Generics

Setup

§1 Generic Bus

§2 Bus Stop

Lambdas and Streams

§1 \(\lambda\)-functions

§2 Streams

Reference material

Java Generics

Why generics?

Generic classes

Generic methods

Bounded generics

Bounds through wildcards

Unbounded wildcard: List<?>

Upper bounded wildcard: ? extends T

Lower bounded wildcard: ? super T

Type erasure

Practical example: a bookshop

Without generics

With generics

Java Hoare Logic

What does it mean for a program to be correct?

Hoare triples

Deriving preconditions by propagating backward

Straight-line code

Through if/else

Proving a block correct

Java Lambdas and Streams

Lambdas (anonymous functions)

Functional interfaces

Streams

Anatomy of a stream pipeline

Java Loop Invariants

What is an invariant?

Motivating puzzle

Loop invariants

Deriving an invariant for power

Designing an algorithm from an invariant: fast exponentiation

Pragmatic considerations

Unbounded wildcard: `List<?>`

Upper bounded wildcard: `? extends T`

Lower bounded wildcard: `? super T`

Through `if`/`else`

Deriving an invariant for `power`