Last updated on

Specifications

Reasoning about your code requires specifying what it is supposed to do?

By popular request, here are extra exercises focused on the contents of the SE lectures. These are intended to complement the exercises already included in the slides.

As usual, ⭐️ indicates the most important exercises and questions; 🔥, the most challenging ones; and 🔜, the ones that are useful to prepare for future lectures.

You do not need to complete all exercises to succeed in this class, and you do not need to do all exercises in the order they are written.

We strongly encourage you to solve the exercises on paper first, in groups. After completing a first draft on paper, you may want to check your solutions on your computer. To do so, you can download the scaffold code (ZIP).

In Scala, it’s common to use require and ensuring to specify pre- and post-conditions for functions, respectively. The require method checks a given condition (usually an input validation) and throws an IllegalArgumentException if the condition is not met. On the other hand, ensuring is used to validate the result of a function. It takes a predicate that the result must satisfy, and if not, an assertion error is thrown.

For example:

val eps = 0.00001f

def sqrt(x: Double): Double = {
  require(x >= 0)
  Math.sqrt(x)
} ensuring (res =>
    (x - res * res) <= eps && (x - res * res) >= -eps
)

This exercise set will make writing such specs second nature!

Debugging with tests and specs

Bad combinatorics ⭐️

Consider the following incorrect function:

/** Construct all subsets of `s` of size `k` (INCORRECT!) */
def badCombinations[T](set: Set[T], k: Int): Set[Set[T]] = {
  if k == 0 then Set(Set())
  if set.isEmpty then Set()
  else
    for
      item <- set
      rest = set - item
      subset <- Iterable.concat(
        for s <- badCombinations(rest, k - 1) yield rest + item,
        for s <- badCombinations(rest, k) yield rest
      )
    yield subset
}

src/main/scala/specs/Tracing.scala

  1. Read this function carefully.

  2. Which inputs are meaningful for this function? Write a require clause to rule out meaningless arguments. Check that your require clause works by calling this function with invalid arguments in a worksheet and confirming that it raises an exception.

  3. Unit tests are a great way to ensure that corner cases are correctly handled. Create a new test suite class in src/test/scala/specs/SpecsSuite.scala (you can consult a previous-week exercise set or lab for inspiration, or the munit documentation), then write a unit test that asserts that this function computes the right result when called with an empty set as input (use assertEquals and Set()).

  4. Make sure that your test runs and reports a failure (it should, since this function is incorrect). You can use sbt testOnly -- *your-test-name* to run your test.

  5. Find the bug that leads to an empty set being returned, and confirm that the unit test now passes.

  6. What does the documentation of this function promise? Write an ensuring clause to capture this formally. Is this a complete specification? (A specification is complete if any function that respects it is a correct implementation of the original requirements — here, the documentation string).

  7. Find an input for which this function violates the postcondition that you just wrote. Confirm your conjecture by calling this function in a worksheet and confirming that the ensuring clause throws an exception.

  8. Correct the remain bugs in this function. You may find it useful to add tracing instructions to observe its behavior.

  9. Bonus question: Is your corrected function efficient? Look carefully at the work it does on a simple example. Do you spot any redundant work?

Bad transactions

The following code defines a class BankAccount and associated operations deposit, withdraw and transfer:

protected class BankAccount(private var _balance: Double):
  import AccOpResult.*

  def balance = _balance

  private def updateBalance(amount: Double): AccOpResult =
    val oldBalance = balance
    _balance = amount
    Ok(oldBalance)

  /** Deposits the specified amount into the bank account.
    *
    * @param amount
    *   The amount to be deposited. Must be non-negative.
    */
  def deposit(amount: Double): AccOpResult = {
    updateBalance(balance + amount)
  }

  /** Withdraws the specified amount from the bank account.
    *
    * @param amount
    *   The amount to be withdrawn. Must be non-negative.
    */
  def withdraw(amount: Double): AccOpResult = {
    if balance >= amount then
      updateBalance(balance - amount)
    else
      InsufficientFund(balance)
  }

  /** Transfers the specified amount from this bank account to `that` bank
    * account.
    *
    * @param amount
    *   The amount to be transferred. Must be non-negative.
    */
  def transfer(that: BankAccount, amount: Double): (AccOpResult, AccOpResult) = {
    if this.balance >= amount then
      (this.withdraw(amount), that.deposit(amount))
    else
      (InsufficientFund(this.balance), Ok(that.balance))
  }

src/main/scala/specs/BankAccount.scala

Type AccOpResult is used to memorize a “screenshot” of the balance before the operation and whether the operation is successful:

enum AccOpResult:
  case Ok(oldBalance: Double)
  case InsufficientFund(oldBalance: Double)

src/main/scala/specs/BankAccount.scala

  1. Write the preconditions and postconditions for function deposit, withdraw and transfer using require and ensuring.
  2. Can you identify the bugs in the code that violate these conditions?

Translating specs from English

Ambiguous specs

The following statements are ambiguous. For each of them, explain the ambiguity (either in words, or by giving at least two different, unambiguous expressions in Scala code that are compatible with the original sentence):

  1. “Access to the system is restricted to senior engineers and developers.”
  2. “The argument to this function must be a supertype of a serializable type that implements IsFinite”
  3. “Only finite Double lists are supported.”
  4. “Any sibling of a node that makes a request must be ready to process answers.”
  5. “Objects passed to this method must be unlockable.”

A particularly good source of examples of ambiguities is newspapers; just look up “Ambiguous newspaper headlines” on Google.

Translating simple specs ⭐️

Translate the following English statements to mathematical statements or to Scala code. Aim to be as succinct and clear as possible; do not optimize for performance. For some statement, it may not be possible to write Scala code (which ones?).

  1. The list of integers l is sorted in ascending order
  2. All values in map m1 are keys in map m2.
  3. Even numbers are always immediately followed by odd numbers in list l.
  4. There are no negative numbers in the output of function f.
  5. Functions f and g compute the same output when given a positive number.
  6. List l1 is a permutation of list l2.
  7. Number p is prime.

Paths and cycles

Translate the following English statements to Scala code:

A path is a nonempty sequence of edges (pairs of points) such that the endpoint of each edge is the starting point of the next edge.

A cycle is a path whose starting point equals its endpoint.

Course policies

This course has a reasonably complex grading policy: one lab is dropped, we accept medical reasons for skipping a lab, callbacks combine with labs, we have a midterm and a final, etc.

Translate the grading policy of this course (found in Overall Grade) into a Scala function, OverallGrade. First, start with the easy version:

def OverallGrade(labScore: Double, midtermScore: Double, finalScore: Double): Double =
  ???

src/main/scala/specs/Specs.scala

🔥 Then, try the full grading policy.

Finding incompleteness in specs ⭐️

The following ensuring specifications are incomplete: they do not detect all incorrect behaviors.

For each one, replace the existing function body with an incorrect implementation that still obeys the ensuring clause, then find an input that proves that your modified function is incorrect and confirm that the ensuring clause is incomplete by checking that it does not raise an assertion.

  1. def filterWithIncompleteSpec[T](l: List[T], p: T => Boolean) = {
  l.filter(p)
} ensuring (res => res.forall(p))

    src/main/scala/specs/Specs.scala

  2. def mapWithIncompleteSpec[T, Q](ts: List[T])(f: T => Q) = {
  ts.map(f)
} ensuring (qs =>
  qs.length == ts.length &&
    qs.forall(q => ts.exists(t => f(t) == q))
)

    src/main/scala/specs/Specs.scala

  3. def flattenWithIncompleteSpec[T](tss: List[List[T]]) = {
  tss.flatten
} ensuring (ts =>
  ts.length == tss.map(_.length).sum &&
    tss.forall(ts.containsSlice(_))
)

    src/main/scala/specs/Specs.scala

© 2023, 2024 EPFL. All rights reserved.