Skip to content

Commit

Permalink
Break long lines
Browse files Browse the repository at this point in the history
  • Loading branch information
btj committed Aug 25, 2020
1 parent ef8d6ef commit 22e8899
Show file tree
Hide file tree
Showing 14 changed files with 263 additions and 137 deletions.
23 changes: 19 additions & 4 deletions behavioral_subtyping.md
Original file line number Diff line number Diff line change
Expand Up @@ -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"};
}
Expand All @@ -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"};
}
Expand Down Expand Up @@ -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"};
}
Expand All @@ -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"};
}
Expand Down
53 changes: 29 additions & 24 deletions complexity_modularity_abstraction.md
Original file line number Diff line number Diff line change
Expand Up @@ -170,18 +170,21 @@ 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
* @may_throw ArithmeticException if arithmetic overflow occurs.
* | 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)
Expand All @@ -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
Expand All @@ -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;
}

/**
Expand All @@ -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)
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand Down
16 changes: 10 additions & 6 deletions entity_relationship_abstractions.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
*/
Expand All @@ -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
Expand Down Expand Up @@ -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) {
Expand All @@ -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;
}
Expand All @@ -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;
}
Expand Down
36 changes: 26 additions & 10 deletions generics.md
Original file line number Diff line number Diff line change
Expand Up @@ -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() { ... }

}
Expand Down Expand Up @@ -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++;
Expand All @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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<Student> iterator = students.iterator(); iterator.hasNext(); ) {
for (Iterator<Student> iterator = students.iterator();
iterator.hasNext(); ) {
Student student = iterator.next();
if (student.nbCredits >= 120)
result++;
Expand All @@ -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<Staff> iterator = staffMembers.iterator(); iterator.hasNext(); ) {
for (Iterator<Staff> iterator = staffMembers.iterator();
iterator.hasNext(); ) {
Staff staff = iterator.next();
nbStaff++;
totalNbPubs += staff.nbPubs;
Expand All @@ -368,8 +384,8 @@ as a subclass of `LinkedList<T>`. For class `SortedLinkedList<T>` to be able to
interface Comparable<T> {

/**
* 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);

Expand Down
3 changes: 2 additions & 1 deletion implementation_inheritance.md
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down
Loading

0 comments on commit 22e8899

Please sign in to comment.