From 22e88998252ae73eb64a5cfc3009c5bcf835d6cb Mon Sep 17 00:00:00 2001 From: Bart Jacobs Date: Tue, 25 Aug 2020 17:16:15 +0200 Subject: [PATCH] Break long lines --- behavioral_subtyping.md | 23 ++++++++-- complexity_modularity_abstraction.md | 53 ++++++++++++---------- entity_relationship_abstractions.md | 16 ++++--- generics.md | 36 ++++++++++----- implementation_inheritance.md | 3 +- inheritance.md | 67 ++++++++++++++++++---------- interfaces.md | 66 +++++++++++++++++---------- iterators.md | 31 +++++++++---- latex.template | 2 +- lecture2part1.md | 2 +- lecture2part2.md | 9 ++-- make-pdf.sh | 11 ++++- multi_class_abstractions.md | 39 ++++++++++------ representation_objects.md | 42 ++++++++++------- 14 files changed, 263 insertions(+), 137 deletions(-) diff --git a/behavioral_subtyping.md b/behavioral_subtyping.md index 029ad93..653a4f3 100644 --- a/behavioral_subtyping.md +++ b/behavioral_subtyping.md @@ -64,7 +64,11 @@ If the changed method no longer complies with its original specification, we nee In the example, there are at least two possible specifications that we can assign to method `getLocations`: - We can assign a strong specification: ```java - /** @post | result != null && result.length == 3 && Arrays.stream(result).allMatch(e -> e != null) */ + /** + * @post | result != null + * @post | result.length == 3 + * @post | Arrays.stream(result).allMatch(e -> e != null) + */ String[] getLocations() { return new String[] {"Brussels", "Paris", "Berlin"}; } @@ -76,7 +80,10 @@ In the example, there are at least two possible specifications that we can assig be updated as well. - We can also assign a weaker specification: ```java - /** @post | result != null && Arrays.stream(result).allMatch(e -> e != null) */ + /** + * @post | result != null + * @post | Arrays.stream(result).allMatch(e -> e != null) + */ String[] getLocations() { return new String[] {"Brussels", "Paris", "Berlin"}; } @@ -162,7 +169,11 @@ These two calls illustrate the two different types of method calls in Java: To reason about programs that use dynamic binding, such as the one shown above, we can simply apply the principle we introduced above: assign a specification to each method of the program, and check that each method's behavior complies with its specification, assuming that the behavior of method calls complies with the called methods' specifications. Suppose we assign the strong specification to method `getLocations` in class `CompanyA`: ```java -/** @post | result != null && result.length == 3 && Arrays.stream(result).allMatch(e -> e != null) */ +/** + * @post | result != null + * @post | result.length == 3 + * @post | Arrays.stream(result).allMatch(e -> e != null) + */ String[] getLocations() { return new String[] {"Brussels", "Paris", "Berlin"}; } @@ -176,7 +187,11 @@ However, this approach does _not_ deal optimally with another type of program mo Indeed, suppose we extend the example program with the following class: ```java class CompanyB extends Company { - /** @post | result != null && result.length == 2 && Arrays.stream(result).allMatch(e -> e != null) */ + /** + * @post | result != null + * @post | result.length == 2 + * @post | Arrays.stream(result).allMatch(e -> e != null) + */ String[] getLocations() { return new String[] {"Vienna", "Prague"}; } diff --git a/complexity_modularity_abstraction.md b/complexity_modularity_abstraction.md index a3ad4cd..291c95f 100644 --- a/complexity_modularity_abstraction.md +++ b/complexity_modularity_abstraction.md @@ -170,7 +170,8 @@ public class Fraction { public static final Fraction ZERO = new Fraction(0, 1); /** - * Returns an object representing the rational number defined by the given numerator and denominator. + * Returns an object representing the rational number defined by the given + * numerator and denominator. * * @throws IllegalArgumentException if the given denominator is zero. * | denominator == 0 @@ -178,10 +179,12 @@ public class Fraction { * | true * @post The result is not null. * | result != null - * @post The rational number represented by the result equals the rational number defined by the - * given numerator and denominator. - * | BigInteger.valueOf(result.getNumerator()).multiply(BigInteger.valueOf(denominator)).equals( - * | BigInteger.valueOf(numerator).multiply(BigInteger.valueOf(result.getDenominator()))) + * @post The rational number represented by the result equals the rational + * number defined by the given numerator and denominator. + * | BigInteger.valueOf(result.getNumerator()) + * | .multiply(BigInteger.valueOf(denominator)).equals( + * | BigInteger.valueOf(numerator).multiply( + * | BigInteger.valueOf(result.getDenominator()))) */ public static Fraction of(long numerator, long denominator) { if (denominator == 0) @@ -197,7 +200,8 @@ public class Fraction { } /** - * Returns whether this object and the given object represent the same rational number. + * Returns whether this object and the given object represent the same + * rational number. * * @throws IllegalArgumentException if {@code other} is null. * | other == null @@ -210,7 +214,8 @@ public class Fraction { public boolean equals(Fraction other) { if (other == null) throw new IllegalArgumentException("other is null"); - return numerator == other.numerator && denominator == other.denominator; + return numerator == other.numerator + && denominator == other.denominator; } /** @@ -232,10 +237,9 @@ public class Fraction { * | BigInteger.valueOf(this.getNumerator()). * | multiply(BigInteger.valueOf(result.getDenominator())). * | multiply(BigInteger.valueOf(other.getDenominator())). - * | add( - * | BigInteger.valueOf(other.getNumerator()). - * | multiply(BigInteger.valueOf(result.getDenominator())). - * | multiply(BigInteger.valueOf(this.getDenominator())))) + * | add(BigInteger.valueOf(other.getNumerator()). + * | multiply(BigInteger.valueOf(result.getDenominator())). + * | multiply(BigInteger.valueOf(this.getDenominator())))) */ public Fraction plus(Fraction other) { if (other == null) @@ -297,7 +301,8 @@ public class MoreMath { * @post The result divides both given numbers. * | divides(result, a) && divides(result, b) * @post No greater number divides both given numbers. - * | LongStream.range(result, Math.max(a, b)).allMatch(x -> !(divides(x + 1, a) && divides(x + 1, b))) + * | LongStream.range(result, Math.max(a, b)).allMatch(x -> + * | !(divides(x + 1, a) && divides(x + 1, b))) */ public static long gcd(long a, long b) { if (a == 0) return b; @@ -406,10 +411,12 @@ public class FractionContainer { * | denominator == 0 * @may_throw ArithmeticException if arithmetic overflow occurs. * | true - * @post The rational number stored by this object equals the rational number defined by the - * given numerator and denominator. - * | BigInteger.valueOf(getNumerator()).multiply(BigInteger.valueOf(denominator)).equals( - * | BigInteger.valueOf(numerator).multiply(BigInteger.valueOf(getDenominator()))) + * @post The rational number stored by this object equals the rational + * number defined by the given numerator and denominator. + * | BigInteger.valueOf(getNumerator()) + * | .multiply(BigInteger.valueOf(denominator)).equals( + * | BigInteger.valueOf(numerator) + * | .multiply(BigInteger.valueOf(getDenominator()))) */ public void set(long numerator, long denominator) { if (denominator == 0) @@ -436,14 +443,12 @@ public class FractionContainer { * | BigInteger.valueOf(getNumerator()). * | multiply(BigInteger.valueOf(old(getDenominator()))). * | multiply(BigInteger.valueOf(denominator)). - * | equals( - * | BigInteger.valueOf(old(getNumerator())). - * | multiply(BigInteger.valueOf(getDenominator())). - * | multiply(BigInteger.valueOf(denominator)). - * | add( - * | BigInteger.valueOf(numerator). - * | multiply(BigInteger.valueOf(getDenominator())). - * | multiply(BigInteger.valueOf(old(getDenominator()))))) + * | equals(BigInteger.valueOf(old(getNumerator())). + * | multiply(BigInteger.valueOf(getDenominator())). + * | multiply(BigInteger.valueOf(denominator)).add( + * | BigInteger.valueOf(numerator). + * | multiply(BigInteger.valueOf(getDenominator())). + * | multiply(BigInteger.valueOf(old(getDenominator()))))) */ public void add(long numerator, long denominator) { if (denominator == 0) diff --git a/entity_relationship_abstractions.md b/entity_relationship_abstractions.md index 0573df2..4217d09 100644 --- a/entity_relationship_abstractions.md +++ b/entity_relationship_abstractions.md @@ -58,7 +58,8 @@ public class OOPStudent { } /** - * Returns this student's teammate, or {@code null} if this student has no teammate. + * Returns this student's teammate, or {@code null} if this student has no + * teammate. * * @peerObject */ @@ -67,8 +68,8 @@ public class OOPStudent { } /** - * Initializes this object to represent a student with the given study programme - * and no teammate. + * Initializes this object to represent a student with the given study + * programme and no teammate. * * @throws IllegalArgumentException if {@code studyProgramme} is null * | studyProgramme == null @@ -96,7 +97,8 @@ public class OOPStudent { * @post This student's teammate equals the given teammate * | getTeammate() == teammate * @post The given student's teammate equals this student - * (Note: this postcondition is redundant because it follows from the public class invariant.) + * (Note: this postcondition is redundant because it follows from the + * public class invariant.) * | teammate.getTeammate() == this */ public void setTeammate(OOPStudent teammate) { @@ -105,7 +107,8 @@ public class OOPStudent { if (this.teammate != null) throw new IllegalStateException("This student already has a teammate"); if (teammate.teammate != null) - throw new IllegalArgumentException("The given teammate already has a teammate"); + throw new IllegalArgumentException( + "The given teammate already has a teammate"); this.teammate = teammate; teammate.teammate = this; } @@ -123,7 +126,8 @@ public class OOPStudent { */ public void clearTeammate() { if (teammate == null) - throw new IllegalStateException("This student does not have a teammate"); + throw new IllegalStateException( + "This student does not have a teammate"); this.teammate.teammate = null; this.teammate = null; } diff --git a/generics.md b/generics.md index 1a3fb68..56b644a 100644 --- a/generics.md +++ b/generics.md @@ -18,7 +18,10 @@ class University { boolean hasStaff(Staff staff) { ... } - /** Returns the average number of scientific publications authored by this university's staff members. */ + /** + * Returns the average number of scientific publications authored by this + * university's staff members. + */ int getAvgNbPubs() { ... } } @@ -110,7 +113,8 @@ class University { /** Returns the number of students that have obtained at least 120 credits. */ int getNbFinishers() { int result = 0; - for (IteratorOfStudent iterator = students.iterator(); iterator.hasNext(); ) { + for (IteratorOfStudent iterator = students.iterator(); + iterator.hasNext(); ) { Student student = iterator.next(); if (student.nbCredits >= 120) result++; @@ -126,11 +130,15 @@ class University { return staffMembers.contains(staff); } - /** Returns the average number of scientific publications authored by this university's staff members. */ + /** + * Returns the average number of scientific publications authored by this + * university's staff members. + */ int getAvgNbPubs() { int nbStaff = 0; int totalNbPubs = 0; - for (IteratorOfStaff iterator = staffMembers.iterator(); iterator.hasNext(); ) { + for (IteratorOfStaff iterator = staffMembers.iterator(); + iterator.hasNext(); ) { Staff staff = iterator.next(); nbStaff++; totalNbPubs += staff.nbPubs; @@ -233,7 +241,10 @@ class University { return staffMembers.contains(staff); } - /** Returns the average number of scientific publications authored by this university's staff members. */ + /** + * Returns the average number of scientific publications authored by this + * university's staff members. + */ int getAvgNbPubs() { int nbStaff = 0; int totalNbPubs = 0; @@ -327,7 +338,8 @@ class University { /** Returns the number of students that have obtained at least 120 credits. */ int getNbFinishers() { int result = 0; - for (Iterator iterator = students.iterator(); iterator.hasNext(); ) { + for (Iterator iterator = students.iterator(); + iterator.hasNext(); ) { Student student = iterator.next(); if (student.nbCredits >= 120) result++; @@ -343,11 +355,15 @@ class University { return staffMembers.contains(staff); } - /** Returns the average number of scientific publications authored by this university's staff members. */ + /** + * Returns the average number of scientific publications authored by this + * university's staff members. + */ int getAvgNbPubs() { int nbStaff = 0; int totalNbPubs = 0; - for (Iterator iterator = staffMembers.iterator(); iterator.hasNext(); ) { + for (Iterator iterator = staffMembers.iterator(); + iterator.hasNext(); ) { Staff staff = iterator.next(); nbStaff++; totalNbPubs += staff.nbPubs; @@ -368,8 +384,8 @@ as a subclass of `LinkedList`. For class `SortedLinkedList` to be able to interface Comparable { /** - * Returns a negative number, zero, or a positive number if this object compares as - * less than, equal to, or greater than {@code other}. + * Returns a negative number, zero, or a positive number if this object + * compares as less than, equal to, or greater than {@code other}. */ int compareTo(T other); diff --git a/implementation_inheritance.md b/implementation_inheritance.md index 78839e1..6761028 100644 --- a/implementation_inheritance.md +++ b/implementation_inheritance.md @@ -41,7 +41,8 @@ public class TransparentColor extends Color { } @Override public String toString() { - return "rgba(" + red + ", " + green + ", " + blue + ", " + transparency + ")"; + return + "rgba(" + red + ", " + green + ", " + blue + ", " + transparency + ")"; } @Override public boolean equals(Object other) { diff --git a/inheritance.md b/inheritance.md index 7eee33d..713ec15 100644 --- a/inheritance.md +++ b/inheritance.md @@ -31,16 +31,23 @@ public class Triangle { public boolean contains(int x, int y) { return - Math.signum(((long)x - x1) * ((long)y2 - y1) - ((long)y - y1) * ((long)x2 - x1)) * - Math.signum(((long)x3 - x1) * ((long)y2 - y1) - ((long)y3 - y1) * ((long)x2 - x1)) >= 0 && - Math.signum(((long)x - x2) * ((long)y3 - y2) - ((long)y - y2) * ((long)x3 - x2)) * - Math.signum(((long)x1 - x2) * ((long)y3 - y2) - ((long)y1 - y2) * ((long)x3 - x2)) >= 0 && - Math.signum(((long)x - x3) * ((long)y1 - y3) - ((long)y - y3) * ((long)x1 - x3)) * - Math.signum(((long)x2 - x3) * ((long)y1 - y3) - ((long)y2 - y3) * ((long)x1 - x3)) >= 0; + Math.signum(((long)x - x1) * ((long)y2 - y1) + - ((long)y - y1) * ((long)x2 - x1)) * + Math.signum(((long)x3 - x1) * ((long)y2 - y1) + - ((long)y3 - y1) * ((long)x2 - x1)) >= 0 && + Math.signum(((long)x - x2) * ((long)y3 - y2) + - ((long)y - y2) * ((long)x3 - x2)) * + Math.signum(((long)x1 - x2) * ((long)y3 - y2) + - ((long)y1 - y2) * ((long)x3 - x2)) >= 0 && + Math.signum(((long)x - x3) * ((long)y1 - y3) + - ((long)y - y3) * ((long)x1 - x3)) * + Math.signum(((long)x2 - x3) * ((long)y1 - y3) + - ((long)y2 - y3) * ((long)x1 - x3)) >= 0; } public String getDrawingCommand() { - return "triangle " + x1 + " " + y1 + " " + x2 + " " + y2 + " " + x3 + " " + y3; + return "triangle " + + x1 + " " + y1 + " " + x2 + " " + y2 + " " + x3 + " " + y3; } } @@ -237,25 +244,35 @@ public class Object { public Class getClass() { /* ... */ } /** - * Returns a number suitable for use as a hash code when using this object as a key in a hash table. - * Note: two objects that are equal according to the `equals(Object)` method must have the same hash code. - * The implementation of this method in class java.lang.Object returns a hash code - * based on the identity of this object. That is, this implementation usually returns a different number - * for different objects, although this is not guaranteed. + * Returns a number suitable for use as a hash code when using this object as + * a key in a hash table. + * + * Note: two objects that are equal according to the `equals(Object)` method + * must have the same hash code. + * + * The implementation of this method in class java.lang.Object returns a hash + * code based on the identity of this object. That is, this implementation + * usually returns a different number for different objects, although this is + * not guaranteed. */ public int hashCode() { /* ... */ } /** * Returns a textual representation of this object. - * The implementation of this method in class java.lang.Object is based on the name of this object's class - * and this object's identity-based hash code. + * + * The implementation of this method in class java.lang.Object is based on the + * name of this object's class and this object's identity-based hash code. */ - public String toString() { return this.getClass().getName() + "@" + Integer.toHexString(this.hashCode()); } + public String toString() { + return this.getClass().getName() + "@" + + Integer.toHexString(this.hashCode()); + } /** * Returns whether this object is conceptually equal to the given object. - * The implementation of this method in class java.lang.Object returns whether this object and the given - * object are the same object. + * + * The implementation of this method in class java.lang.Object returns whether + * this object and the given object are the same object. */ public boolean equals(Object other) { return other == this; } @@ -322,17 +339,19 @@ The `@Override` annotations cause Java's static type checker to check that the m As a result of overriding these methods from class `Object`, we get the following behavior: ```java -assertEquals("This is Point [x=10, y=20].", "This is " + new Point(10, 20) + "."); -assertEquals(true, new Point(10, 20).equals(new Point(10, 20))); +assertEquals("This is Point [x=10, y=20].","This is " + new Point(10, 20) + "."); +assertTrue(new Point(10, 20).equals(new Point(10, 20))); assertEquals(new Point(10, 20), new Point(10, 20)); -assertEquals(true, Arrays.asList(new Point(3, 9), new Point(7, 20)).contains(new Point(3, 9))); -assertEquals(true, Set.of(new Point(3, 9), new Point(7, 20)).contains(new Point(7, 20))); +assertTrue( + Arrays.asList(new Point(3, 9), new Point(7, 20)).contains(new Point(3, 9))); +assertTrue(Set.of(new Point(3, 9), new Point(7, 20)).contains(new Point(7, 20))); ``` If we had not overridden these methods, the behavior would be as follows: ```java assertEquals("This is Point@12345678.", "This is " + new Point(10, 20) + "."); -assertEquals(false, new Point(10, 20).equals(new Point(10, 20))); -assertEquals(false, Arrays.asList(new Point(3, 9), new Point(7, 20)).contains(new Point(3, 9))); -assertEquals(false, Set.of(new Point(3, 9), new Point(7, 20)).contains(new Point(7, 20))); +assertFalse(new Point(10, 20).equals(new Point(10, 20))); +assertFalse( + Arrays.asList(new Point(3, 9), new Point(7, 20)).contains(new Point(3, 9))); +assertFalse(Set.of(new Point(3, 9), new Point(7, 20)).contains(new Point(7, 20))); ``` diff --git a/interfaces.md b/interfaces.md index 3bb434f..4bd1f84 100644 --- a/interfaces.md +++ b/interfaces.md @@ -38,7 +38,9 @@ public class IntValue extends Value { public Type getType() { return IntType.INSTANCE; } private IntValue(int value) { this.value = value; } public final static IntValue ZERO = new IntValue(0); - public static IntValue of(int value) { return value == 0 ? ZERO : new IntValue(value); } + public static IntValue of(int value) { + return value == 0 ? ZERO : new IntValue(value); + } } public class StringValue extends Value { @@ -46,7 +48,9 @@ public class StringValue extends Value { public Type getType() { return StringType.INSTANCE; } private StringValue(String value) { this.value = value; } public final static StringValue EMPTY = new StringValue(""); - public static StringValue of(String value) { return value.equals("") ? EMPTY : new StringValue(value); } + public static StringValue of(String value) { + return value.equals("") ? EMPTY : new StringValue(value); + } } ``` First of all, notice the following: @@ -67,38 +71,45 @@ public abstract class AndableType { public class BooleanType extends Type, AndableType { // ERROR // ... public Value and(Value leftOperand, Value rightOperand) { - return BooleanValue.of(((BooleanValue)leftOperand).value & ((BooleanValue)rightOperand).value); + return BooleanValue.of(((BooleanValue)leftOperand).value + & ((BooleanValue)rightOperand).value); } } public class IntType extends Type, AddableType, AndableType { // ERROR // ... public Value add(Value leftOperand, Value rightOperand) { - return IntValue.of(((IntValue)leftOperand).value + ((IntValue)rightOperand).value); + return IntValue.of(((IntValue)leftOperand).value + + ((IntValue)rightOperand).value); } public Value and(Value leftOperand, Value rightOperand) { - return IntValue.of((IntValue)leftOperand).value & ((IntValue)rightOperand).value); + return IntValue.of((IntValue)leftOperand).value + & ((IntValue)rightOperand).value); } } public class StringType extends Type, AddableType { // ERROR // ... public Value add(Value leftOperand, Value rightOperand) { - return StringValue.of(((StringValue)leftOperand).value + ((StringValue)rightOperand).value); + return StringValue.of(((StringValue)leftOperand).value + + ((StringValue)rightOperand).value); } } public class Interpreter { - public static Value evaluate(Value leftOperand, char operator, Value rightOperand) { - Type type = leftOperand.getType(); - if (type != rightOperand.getType()) - throw new UnsupportedOperationException("The operand types do not match"); + public static Value evaluate(Value value1, char operator, Value value2) { + Type type = value1.getType(); + if (type != value2.getType()) + throw new UnsupportedOperationException( + "The operand types do not match"); switch (operator) { case '+': if (!(type instanceof AddableType)) - throw new UnsupportedOperationException("Type " + type + " does not support the + operator"); - return ((AddableType)type).add(leftOperand, rightOperand); + throw new UnsupportedOperationException( + "Type " + type + " does not support the + operator"); + return ((AddableType)type).add(value, value2); case '&': if (!(type instanceof AndableType)) - throw new UnsupportedOperationException("Type " + type + " does not support the & operator"); - return ((AndableType)type).and(leftOperand, rightOperand); + throw new UnsupportedOperationException( + "Type " + type + " does not support the & operator"); + return ((AndableType)type).and(value1, value2); // ... } } @@ -115,38 +126,45 @@ public interface AndableType { public class BooleanType extends Type implements AndableType { // ... public Value and(Value leftOperand, Value rightOperand) { - return BooleanValue.of(((BooleanValue)leftOperand).value & ((BooleanValue)rightOperand).value); + return BooleanValue.of(((BooleanValue)leftOperand).value + & ((BooleanValue)rightOperand).value); } } public class IntType extends Type implements AddableType, AndableType { // ... public Value add(Value leftOperand, Value rightOperand) { - return IntValue.of(((IntValue)leftOperand).value + ((IntValue)rightOperand).value); + return IntValue.of(((IntValue)leftOperand).value + + ((IntValue)rightOperand).value); } public Value and(Value leftOperand, Value rightOperand) { - return IntValue.of((IntValue)leftOperand).value & ((IntValue)rightOperand).value); + return IntValue.of((IntValue)leftOperand).value + & ((IntValue)rightOperand).value); } } public class StringType extends Type implements AddableType { // ... public Value add(Value leftOperand, Value rightOperand) { - return StringValue.of(((StringValue)leftOperand).value + ((StringValue)rightOperand).value); + return StringValue.of(((StringValue)leftOperand).value + + ((StringValue)rightOperand).value); } } public class Interpreter { - public static Value evaluate(Value leftOperand, char operator, Value rightOperand) { + public static Value evaluate(Value value1, char operator, Value value2) { Type type = leftOperand.getType(); if (type != rightOperand.getType()) - throw new UnsupportedOperationException("The operand types do not match"); + throw new UnsupportedOperationException( + "The operand types do not match"); switch (operator) { case '+': if (!(type instanceof AddableType)) - throw new UnsupportedOperationException("Type " + type + " does not support the + operator"); - return ((AddableType)type).add(leftOperand, rightOperand); + throw new UnsupportedOperationException( + "Type " + type + " does not support the + operator"); + return ((AddableType)type).add(value1, value2); case '&': if (!(type instanceof AndableType)) - throw new UnsupportedOperationException("Type " + type + " does not support the & operator"); - return ((AndableType)type).and(leftOperand, rightOperand); + throw new UnsupportedOperationException( + "Type " + type + " does not support the & operator"); + return ((AndableType)type).and(value1, value2); // ... } } diff --git a/iterators.md b/iterators.md index 5e90f48..6a56186 100644 --- a/iterators.md +++ b/iterators.md @@ -34,7 +34,9 @@ public class ClientProgram { } public void printAll(LinkedList linkedList) { - for (LinkedList.Node node = linkedList.firstNode; node != null; node = node.next) + for (LinkedList.Node node = linkedList.firstNode; + node != null; + node = node.next) System.out.println(node.value); } @@ -70,14 +72,20 @@ We show the styles used by some of the most popular programming languages (trans // Java public interface Iterator { boolean hasNext(); - /** Mutates the iterator to point to the next element and returns the current element. */ + /** + * Mutates the iterator to point to the next element and returns the current + * element. + */ Object next(); } // C# public interface Enumerator { Object getCurrent(); - /** Mutates the enumerator to point to the next element, or returns `false` if the end has been reached. */ + /** + * Mutates the enumerator to point to the next element, or returns `false` if + * the end has been reached. + */ boolean moveNext(); } @@ -85,14 +93,17 @@ public interface Enumerator { public interface Iterator { Object getCurrent(); // syntax in C++: *iterator void moveNext(); // syntax in C++: iterator++ - // in C++, to tell whether you have reached the end of the data structure, you have - // to test equality with a special "one-past-the-end" iterator + // in C++, to tell whether you have reached the end of the data structure, you + // have to test equality with a special "one-past-the-end" iterator boolean equals(Iterator other); } // Python public interface Iterator { - /** Throws a StopIteration exception if the end of the data structure has been reached. */ + /** + * Throws a StopIteration exception if the end of the data structure has been + * reached. + */ Object next(); } @@ -100,7 +111,10 @@ public interface Iterator { public interface Iterator { // Nested classes inside interfaces are implicitly public and static class NextResult { public Object value; public boolean done; } - /** If result.done is true, result.value is not an element but an "iterator return value". */ + /** + * If result.done is true, result.value is not an element but an "iterator + * return value". + */ NextResult next(); } ``` @@ -487,7 +501,8 @@ public class ClientProgram { }); } - public void printBoth(Predicate condition, Iterable collection1, Iterable collection2) { + public void printBoth(Predicate condition, + Iterable collection1, Iterable collection2) { printAll(condition, collection1); printAll(condition, collection2); } diff --git a/latex.template b/latex.template index 9fa7b94..9546bd8 100644 --- a/latex.template +++ b/latex.template @@ -241,7 +241,7 @@ $endif$ $if(listings)$ %\usepackage{geometry} \definecolor{ogpjavadoc}{HTML}{3F5FBF} -\addtolength{\hoffset}{-2cm} +%\addtolength{\hoffset}{-2cm} \usepackage{listings} \newcommand{\passthrough}[1]{#1} \lstset{defaultdialect=[5.3]Lua} diff --git a/lecture2part1.md b/lecture2part1.md index 285815f..f2812d2 100644 --- a/lecture2part1.md +++ b/lecture2part1.md @@ -385,7 +385,7 @@ class Interval { } ``` -Now, if we replace `Interval.setUpperBound(interval, 7)` by `interval.upperBound = 7` in class `IntervalTest`, we immediately get a compilation error: `The field Interval.upperBound is not visible.`. Fix the error by restoring the setter call. +Now, if we replace `Interval.setUpperBound(interval, 7)` by `interval.upperBound = 7` in class `IntervalTest`, we immediately get a compilation error: _The field `Interval.upperBound` is not visible._ Fix the error by restoring the setter call. By making the fields of class `Interval` private, we now get the guarantee that any client code of class `Interval` that has no compilation errors will not break if we change the way we store the interval properties. If our module is used by many clients around the world, this is an extremely valuable guarantee. diff --git a/lecture2part2.md b/lecture2part2.md index b027770..86d8eb8 100644 --- a/lecture2part2.md +++ b/lecture2part2.md @@ -140,7 +140,8 @@ package interval; * * @invar This interval's lower bound is not greater than its upper bound. * | getLowerBound() <= getUpperBound() - * @invar This interval's width equals the difference between its upper bound and its lower bound. + * @invar This interval's width equals the difference between its upper bound + * and its lower bound. * | getWidth() == getUpperBound() - getLowerBound() */ class Interval { @@ -243,9 +244,11 @@ class Interval { * | 0 <= value * @post This interval's width equals the given value. * | getWidth() == value - * @post If the caller specified that the lower bound should be updated, the upper bound has remained unchanged. + * @post If the caller specified that the lower bound should be updated, the + * upper bound has remained unchanged. * | !updateLowerBound || getUpperBound() == old(getUpperBound()) - * @post If the caller specified that the lower bound should not be updated, the lower bound has remained unchanged. + * @post If the caller specified that the lower bound should not be updated, + * the lower bound has remained unchanged. * | updateLowerBound || getLowerBound() == old(getLowerBound()) */ void setWidth(int value, boolean updateLowerBound) { diff --git a/make-pdf.sh b/make-pdf.sh index b77550e..b0d89ec 100644 --- a/make-pdf.sh +++ b/make-pdf.sh @@ -21,6 +21,15 @@ pandoc -o course-notes.html -f gfm \ implementation_inheritance.md \ iterators.md \ generics.md -pandoc -V documentclass=book -V classoption=oneside --toc --template=latex.template --listings -o course-notes.tex course-notes.html +pandoc --wrap=none -V documentclass=book --toc --template=latex.template --listings -o course-notes.tex course-notes.html +sed -i '' \ + -e 's/\chapter{Managing Complexity through Modularity and Abstraction}/\chapter[Managing Complexity: Modularity \\\& Abstraction]{Managing Complexity through Modularity and Abstraction}/' \ + -e 's/\section{FractionLists: Representation Exposure Breaks Consistency}/\section[Representation Exposure Breaks Consistency]{FractionLists: Representation Exposure Breaks Consistency}/' \ + -e 's/\chapter{How to properly document single-object abstractions}/\chapter[How to document single-object abstractions]{How to properly document single-object abstractions}/' \ + -e 's/\section{Nesting class-encapsulated and package-encapsulated abstractions}/\section[Nesting class-level and package-level abstractions]{Nesting class-encapsulated and package-encapsulated abstractions}/' \ + -e 's/\chapter{How to properly document multi-object abstractions}/\chapter[How to document multi-object abstractions]{How to properly document multi-object abstractions}/' \ + -e 's/\chapter{Behavioral subtyping: modular reasoning about programs that use dynamic binding}/\chapter[Modular reasoning about dynamic binding]{Behavioral subtyping: modular reasoning about programs that use dynamic binding}/' \ + -e 's/\section{Modular reasoning about programs that use dynamic binding}/\section[Modular reasoning about dynamic binding]{Modular reasoning about programs that use dynamic binding}/' \ + course-notes.tex pdflatex course-notes.tex pdflatex course-notes.tex diff --git a/multi_class_abstractions.md b/multi_class_abstractions.md index 23b1002..eddecf3 100644 --- a/multi_class_abstractions.md +++ b/multi_class_abstractions.md @@ -139,8 +139,8 @@ import logicalcollections.LogicalSet; public class ProjectCourseStudent { /** - * @invar | true // Phase 1 representation invariant - * @invar | team == null || team.members.contains(this) // Phase 2 representation invariant + * @invar | true // Phase 1 representation invariant + * @invar | team == null || team.members.contains(this) // Phase 2 rep. inv. * * @peerObject */ @@ -192,8 +192,10 @@ public class ProjectCourseStudent { * * @post This student is not in a team. * | getTeam() == null - * @post This student's old team's members are its old members minus this student. - * | old(getTeam()).getMembers().equals(LogicalSet.minus(old(getTeam().getMembers()), this)) + * @post This student's old team's members are its old members minus this + * student. + * | old(getTeam()).getMembers().equals( + * | LogicalSet.minus(old(getTeam().getMembers()), this)) */ public void leaveTeam() { if (this.team == null) @@ -220,8 +222,9 @@ import java.util.Set; public class Team { /** - * @invar | members != null // Phase 1 representation invariant - * @invar | members.stream().allMatch(s -> s != null && s.team == this) // Phase 2 representation invariant + * @invar | members != null // Phase 1 representation invariant + * @invar | members.stream().allMatch(s -> + * | s != null && s.team == this) // Phase 2 rep. inv. * * @representationObject * @peerObjects @@ -318,7 +321,8 @@ public class ProjectCourseStudent { private Team team; /** - * @invar | getTeamInternal() == null || getTeamInternal().getMembersInternal().contains(this) + * @invar | getTeamInternal() == null + * | || getTeamInternal().getMembersInternal().contains(this) * * @peerObject */ @@ -370,8 +374,10 @@ public class ProjectCourseStudent { * * @post This student is not in a team. * | getTeam() == null - * @post This student's old team's members are its old members minus this student. - * | old(getTeam()).getMembers().equals(LogicalSet.minus(old(getTeam().getMembers()), this)) + * @post This student's old team's members are its old members minus this + * student. + * | old(getTeam()).getMembers().equals( + * | LogicalSet.minus(old(getTeam().getMembers()), this)) */ public void leaveTeam() { if (this.team == null) @@ -410,7 +416,8 @@ public class Team { /** * Returns this team's set of members. * - * @invar | getMembersInternal().stream().allMatch(s -> s.getTeamInternal() == this) + * @invar | getMembersInternal().stream().allMatch(s -> + * | s.getTeamInternal() == this) * * @post | result != null && result.stream().allMatch(s -> s != null) * @peerObjects @@ -442,8 +449,10 @@ public class Team { * @throws IllegalArgumentException if {@code student} is null * | student == null * @mutates | this - * @post This team's set of members equals its old set of members plus the given student. - * | getMembersInternal().equals(LogicalSet.plus(old(getMembersInternal()), student)) + * @post This team's set of members equals its old set of members plus the + * given student. + * | getMembersInternal().equals( + * | LogicalSet.plus(old(getMembersInternal()), student)) */ void addMember(ProjectCourseStudent student) { if (student == null) @@ -458,8 +467,10 @@ public class Team { * @throws IllegalArgumentException if {@code student} is null * | student == null * @mutates | this - * @post This team's set of members equals its old set of members minus the given student. - * | getMembersInternal().equals(LogicalSet.minus(old(getMembersInternal()), student)) + * @post This team's set of members equals its old set of members minus the + * given student. + * | getMembersInternal().equals( + * | LogicalSet.minus(old(getMembersInternal()), student)) */ void removeMember(ProjectCourseStudent student) { if (student == null) diff --git a/representation_objects.md b/representation_objects.md index 9ba454c..a884729 100644 --- a/representation_objects.md +++ b/representation_objects.md @@ -52,9 +52,10 @@ public class String { * @throws NullPointerException | other == null * @post | result != null * @post | result.getLength() == getLength() + other.getLength() - * @post | IntStream.range(0, getLength()).allMatch(i -> result.charAt(i) == charAt(i)) - * @post | IntStream.range(0, other.getLength()) - * | .allMatch(i -> result.charAt(getLength() + i) == other.charAt(i)) + * @post | IntStream.range(0, getLength()).allMatch(i -> + * | result.charAt(i) == charAt(i)) + * @post | IntStream.range(0, other.getLength()).allMatch(i -> + * | result.charAt(getLength() + i) == other.charAt(i)) */ public String concat(String other) @@ -128,14 +129,16 @@ public class String { * @throws NullPointerException | other == null * @post | result != null * @post | result.getLength() == getLength() + other.getLength() - * @post | IntStream.range(0, getLength()).allMatch(i -> result.charAt(i) == charAt(i)) - * @post | IntStream.range(0, other.getLength()) - * | .allMatch(i -> result.charAt(getLength() + i) == other.charAt(i)) + * @post | IntStream.range(0, getLength()).allMatch(i -> + * | result.charAt(i) == charAt(i)) + * @post | IntStream.range(0, other.getLength()).allMatch(i -> + * | result.charAt(getLength() + i) == other.charAt(i)) */ public String concat(String other) { char[] cs = new char[characters.length + other.characters.length]; System.arraycopy(characters, 0, cs, 0, characters.length); - System.arraycopy(other.characters, 0, cs, characters.length, other.characters.length); + System.arraycopy(other.characters, 0, cs, characters.length, + other.characters.length); return new String(cs); } @@ -156,10 +159,11 @@ Let's see what happens if we break encapsulation. Here is a first attempt to add * * @post | result != null * @post | result.length == getLength() - * @post | IntStream.range(0, getLength()).allMatch(i -> result[i] == charAt(i)) + * @post | IntStream.range(0, getLength()).allMatch(i -> + * | result[i] == charAt(i)) */ public char[] toCharArray() { - return characters; // WRONG! Representation exposure; breaks encapsulation. + return characters; // WRONG! Representation exposure } ``` Although this method satisfies its postconditions, it is still wrong. This is because it *leaks* the receiver object's representation object; it *exposes* the representation object to clients. This is wrong because it allows clients to perform inappropriate mutations of the abstract value of the `String` object by mutating the representation object. That is, it allows clients to break the immutability of the `String` object: @@ -180,7 +184,8 @@ A correct way to implement method `toCharArray` is by returning a copy of the re * @creates | result * @post | result != null * @post | result.length == getLength() - * @post | IntStream.range(0, getLength()).allMatch(i -> result[i] == charAt(i)) + * @post | IntStream.range(0, getLength()).allMatch(i -> + * | result[i] == charAt(i)) */ public char[] toCharArray() { return characters.clone(); @@ -208,7 +213,8 @@ A class must never leak its representation objects. But not leaking representati * | .allMatch(i -> result.charAt(i) == characters[i]) */ public static String valueOf(char[] characters) { - return new String(characters); // WRONG! Client-supplied object used as representation object. + return new String(characters); // WRONG! Client-supplied object + // used as representation object. } ``` @@ -312,8 +318,10 @@ public class FractionList { * @mutates | this * @post | getSize() == old(getSize()) + 1 * @post | Arrays.equals( - * | IntStream.range(0, old(getSize())).mapToObj(i -> getElementAt(i)).toArray(), - * | old(IntStream.range(0, getSize()).mapToObj(i -> getElementAt(i)).toArray())) + * | IntStream.range(0, old(getSize())) + * | .mapToObj(i -> getElementAt(i)).toArray(), + * | old(IntStream.range(0, getSize()) + * | .mapToObj(i -> getElementAt(i)).toArray())) * @post | Objects.equals(getElementAt(old(getSize())), element) */ public void add(Fraction element) { @@ -341,7 +349,7 @@ FractionList myList = new FractionList(); myList.add(Fraction.ZERO); Fraction[] elements = myList.getElements(); elements[0] = null; -// Object myList is now in an inconsistent state; its representation invariants do not hold. +// Object myList is now in an inconsistent state myList.sum(); // crashes with a NullPointerException ``` Method `sum` relies on the receiver's representation invariants for its safe execution; indeed, running this method @@ -597,7 +605,8 @@ public class ByteBuffer { * @post The elements of the array referenced by this object, except for the * element at the old offset, have remained unchanged. * | IntStream.range(0, getArray().length).allMatch(i -> - * | i == old(getOffset()) || getArray()[i] == old(getArray().clone())[i]) + * | i == old(getOffset()) + * | || getArray()[i] == old(getArray().clone())[i]) */ public void put(byte b) { this.array[offset] = b; @@ -614,7 +623,8 @@ ByteBuffer myBuffer = new ByteBuffer(myBytes); assert myBytes[0] == 1; // Succeeds myBuffer.put(4); assert myBytes[0] == 4; // Succeeds, as expected: - // `myBuffer.put()` mutates `myBuffer.getArray()` a.k.a. `myBytes` + // `myBuffer.put()` mutates `myBuffer.getArray()` + // a.k.a. `myBytes` byte[] moreBytes = myBuffer.getArray(); assert moreBytes[1] == 2; // Succeeds