Last updated on Monday, December 16, 2024

Autograded Exercises with Stainless

Welcome to a new exercise set of CS-214 — Software Construction!

As usual, ⭐️ indicates the most important exercises and questions and 🔥 indicates the most challenging ones.

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.

To complete these exercises, you can download the scaffold code (ZIP).

We have prepared a set of exercises that will help you explore course concepts from previous weeks, while at the same time leveraging the Stainless software verifier under the hood. You will find Monday’s week 13 lecture Formal Verification helpful for these exercises.

The auto-prover is set up on our servers: you can run it by submitting your solutions on Moodle, just like for labs (but no worries! The score returned by the grader and the feedback are just for you: just like other exercises, they don’t impact your course grade in any way).

Autograding with Stainless

If you submit a solution, you will receive automated feedback based not only on tests, but also on formal verification against a set of solutions. In addition to testing, our autograder uses Stainless for formal equivalence checking mode.

Recall that, in contrast to testing, formal verification provides a guarantee that your programs are never wrongly classified as correct or incorrect, reducing the danger of misleading you. Compared to syntactic code comparison, this approach allows you to experiment with solutions beyond those envisioned by instructors.

Recommended Workflow: How to use the feedback.txt file

We recommend submitting your solutions and inspecting the generated feedback.txt file. In the case where your solution fails on some test, or our verifier disproves the correctness of your submission, you will get as feedback an example input where your solution does not return the expected result. We encourage you to iterate on your solution and resubmit until you fully solve each problem. In the case where the feedback file reports safety errors for helper functions that you write, you should consider adding require statements to those functions to ensure that the input parameters are valid.

Troubleshooting: How to use the logging.log file

The logging.log file provides more details on the proofs made by the Stainless autograder. You can inspect the report at the end of the log file, in the stainless summary sections, where you will find two tables indicating the list of properties that the autograder tries to prove. These properties can be preconditions, pattern matching exhaustiveness, termination checks, equivalence checks etc. There you will also find the outcome (valid, invalid, timeout, etc.) of the autograder for each of these properties. Timeout indicates that the autograder was neither able to prove nor disprove that a certain property holds. The log file also provides additional information in case some internal error occurs.

Notes on Stainless Subset of Scala

Stainless Autograder supports a subset of Scala, with a preference for purely functional constructs. This subset largely aligns with the concepts that we present in the course. However, there are some language constructs that are currently not supported. Here is a (non-exhaustive) list of unsupported language constructs together with recommendations on how to avoid them:

If you need to use library functions (such as scala.math.max), you will need to implement them yourself in the file that you are going to submit. For exercises operating on lists, we will already provide you with a custom List library, with a subset of the library functions that you are allowed to use in those exercises, without having to implement them yourself.
Stainless does not support for-comprehensions. Rather than writing for-loops, you should consider writing recursive functions.
Stainless does not support exceptions. You should write require statements to ensure that the function’s input parameters are valid.

To check whether you are staying within the fragment supported by Stainless, you can download the Stainless release and run stainless on your program. You can use command-line options to adjust stainless behavior. Command line options start with a double dash sign --. Here are some of the most important ones:

check-measures=no to skip checking termination
infer-measures=no to skip inferring termination measures
watch to keep stainless active and re-run whenever the files change
solvers=smt-z3,smt-cvc5 to specify alternative theorem provers
timeout=10 to specify 10 seconds as the maximal timeout for each proof obligation
functions=f1,f2 to verify only functions f1 and f2
strict-arithmetic=false to omit checks for wrap-around in modular arithmetic (errors are still checked)

Now that you know the essentials about Stainless and how to use this formal verifier, you can start with the exercises!

Review of Pattern Matching exercises

In this first section, we will review some of the exercises of week 3 exercise set on Pattern Matching. You can try to submit the solutions you wrote during week 3, and see if the autograder can detect any errors in your implementation!

Contexts

We will start by reviewing the Contexts exercise.

Remember that our contexts associate names (Strings) with values (Ints), and let us do the following:

Create an empty context;
Add another key/value pair (called a “binding”) to a context;
Look up a key to retrieve the corresponding value;
Remove a key and its corresponding value.

Implement the following functions and try to submit them on Moodle:

empty returns an empty context:
```
  def empty: Context =
    ???
```
src/main/scala/patmat/EnumContextOps.scala
cons forms a new context by associating a new pair of name-value in an existing context:
```
  def cons(name: String, value: Int, rem: Context) =
    ???
```
src/main/scala/patmat/EnumContextOps.scala
lookup looks a name up in a given context:
```
  def lookup(ctx: Context, name: String): LookupResult =
    ???
```
src/main/scala/patmat/EnumContextOps.scala
erase drops all bindings with the given name in the context:
```
  def erase(ctx: Context, name: String): Context =
    ???
```
src/main/scala/patmat/EnumContextOps.scala
Finally, filter drops all bindings that fail the test pred (i.e. for which pred evaluates to `false):
```
  def filter(ctx: Context, pred: (String, Int) => Boolean): Context =
    ???
```
src/main/scala/patmat/EnumContextOps.scala

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/patmat/EnumContextOps.scala

Tree Mapping and Tree Reducing

We will now work with Trees. For this exercise, you will work with the same tree definition as in week 3:

enum IntTree:
  case Leaf(value: Int)
  case Branch(left: IntTree, right: IntTree)

src/main/scala/patmat/IntTree.scala

You need to implement and submit the three following functions:

treeMap creates a new tree by applying the given function on the value of each leaf node in the tree:
```
  def treeMap(tree: IntTree, op: Int => Int): IntTree =
    ???
```
src/main/scala/patmat/IntTreeOps.scala
treeReduce reduces the values in the tree with the operator:
```
  def treeReduce(tree: IntTree, op: (Int, Int) => Int): Int =
    ???
```
src/main/scala/patmat/IntTreeOps.scala
Note that if you do not remember how the function should work, you can review the examples given in Week 3 exercise set.
treeMapReduce first maps the values stored in each leaf with mapper, then reduces these mapped values using reducer
```
  def treeMapReduce(tree: IntTree, mapper: Int => String, reducer: (String, String) => String): String =
    ???
```
src/main/scala/patmat/IntTreeOps.scala

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/patmat/IntTreeOps.scala

Natural Numbers ⭐️

For this exercise, you will work with Natural Numbers.

Remember that a way to represent natural numbers is to use the following enum:

enum UnaryNat:
  case Zero
  case Succ(pred: UnaryNat)

src/main/scala/patmat/UnaryNat.scala

This exercise is divided into three independent parts that you will submit individually.

Conversion to/from integers

In this section, you will implement the following functions:

fromInt converts integers into UnaryNat:
```
  def fromInt(n: Int): UnaryNat =
    ???
```
src/main/scala/patmat/UnaryNatConv.scala
toInt converts UnaryNat to integers:
```
  def toInt(n: UnaryNat): BigInt =
    ???
```
src/main/scala/patmat/UnaryNatConv.scala

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/patmat/UnaryNatConv.scala

Operations on UnaryNat numbers

Now that we can convert integers into UnaryNat numbers, we want to be able to make simple operations on them. Implement the following functions to do so:

add adds two UnaryNat numbers:
```
  def add(n: UnaryNat, m: UnaryNat): UnaryNat =
    ???
```
src/main/scala/patmat/UnaryNatOps.scala
multiply multiplies two UnaryNat numbers:
```
  def multiply(n: UnaryNat, m: UnaryNat): UnaryNat =
    ???
```
src/main/scala/patmat/UnaryNatOps.scala
minus subtracts a UnaryNat number from another:
```
  def minus(n: UnaryNat, m: UnaryNat): UnaryNat =
    ???
```
src/main/scala/patmat/UnaryNatOps.scala

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/patmat/UnaryNatOps.scala

Parity checks

Finally, we could want to know the parity of a UnaryNat number. Implement the following functions to be able to know whether a UnaryNat number is odd or even:

  def isEven(n: UnaryNat): Boolean =
    ???

src/main/scala/patmat/UnaryNatParity.scala

  def isOdd(n: UnaryNat): Boolean =
    ???

src/main/scala/patmat/UnaryNatParity.scala

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/patmat/UnaryNatParity.scala

Context as Binary Search Trees

For this exercise, we will review how to work with context using binary search trees.

Remember that to improve the efficiency of lookups, insertions, and removals in contexts, we used binary search trees (BSTs). BSTs store bindings in a sorted manner, allowing faster operations compared to linear structures like linked lists. You can have a look at the complete description made in week 3 following this link.

Stainless Autograder do not support string comparaisons with operators like < or >. To simplifiy the exercise, the BST you will use is a bit different to the one of week 3: it maps string, as value, to integrers, as key (instead of mapping integers to strings).

Here is the new definition of BSTContext:

enum BSTContext:
  case Leaf
  case Branch(k: Int, v: String, l: BSTContext, r: BSTContext)

src/main/scala/patmat/BST.scala

We divided this exercise into two parts that need to be completed and submitted individually.

Basic operations

First, you need to implement basic operations made on BSTs:

lookup looks a name up in a given BSTs context:
```
  def lookup(bst: BSTContext, key: Int): FindResult =
    ???
```
src/main/scala/patmat/BSTOpsBasic.scala
insert inserts a pair (key, value) in a given BSTs context:
```
  def insert(bst: BSTContext, key: Int, v: String): BSTContext =
    ???
```
src/main/scala/patmat/BSTOpsBasic.scala

The lookup function will return an instance of the enum FindResult which is very similar to the LookupResultenum:

enum FindResult:
  case Found(value: String)
  case NotFound

src/main/scala/patmat/BST.scala

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/patmat/BSTOpsBasic.scala

Rotations

Now, you will work on rotation of BSTs. Remember that operations are much more efficient if they run on a balanced tree, so rotations on trees can be very useful. The following diagram illustrates two rotations (left and right), with the root node colored in blue:

Implement the two rotation functions in the file BSTOpsRotate:

  def rotateLeft(tree: BSTContext): BSTContext =
    ???

src/main/scala/patmat/BSTOpsRotate.scala

  def rotateRight(tree: BSTContext): BSTContext =
    ???

src/main/scala/patmat/BSTOpsRotate.scala

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/patmat/BSTOpsRotate.scala

Drop

Let’s now implement new functions and try to submit them on Moodle to see the result of the autograder.

For this exercise, you should implement a function that takes a list of integers ls and an integer n as argument, and returns the list obtained by dropping every n-th element from ls. For example, the input (List(1, 2, 3, 4, 5, 6, 7, 8, 9), 3) should lead to the output List(1, 2, 4, 5, 7, 8). You need to implement this function recursively.

  def drop(ls: List[Int], n: Int): List[Int] =
    require(n >= 0)
    ???

src/main/scala/drop/Drop.scala

You are provided with a custom implementation of List, you must use it instead of Scala’s List.

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/drop/Drop.scala

Prime numbers ⭐️

Implement a function that takes a natural integer n as argument, and returns whether this integer is prime or not. For example, the input 7 should lead to the output true. As a helper, you get the implementation of the isqrt function.

  def isPrime(n: BigInt): Boolean =
    require(n >= 0)
    ???

src/main/scala/prime/Prime.scala

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/prime/Prime.scala

GCD ⭐️

Implement a function that takes two natural integers a and b as arguments, and returns the greatest common divisor of these two. For example, the inputs 24 and 16 should lead to the output 8.

  def gcd(a: Int, b: Int): Int =
    require(a >= 0 && b >= 0)
    ???

src/main/scala/gcd/GCD.scala

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/gcd/GCD.scala

Infix operator

In this exercise, we will implement some definitions for logical operations.

Except for the not operation, find a way to define the following logical operations (and, or, equ, xor, nor, nand, impl) as infix operators for Boolean type.

Then, write the definitions of those 8 operators in the most concise manner.

For example :

val a, b : Boolean = true
	res = a xor b

Should compile and return false when evaluating res.

def not(b: Boolean): Boolean = ???

extension (a: Boolean)

  infix def and(b: Boolean): Boolean = ???

  infix def or(b: Boolean): Boolean = ???

  infix def equ(b: Boolean): Boolean = ???

  infix def xor(b: Boolean): Boolean = ???

  infix def nor(b: Boolean): Boolean = ???

  infix def nand(b: Boolean): Boolean = ???

  infix def impl(b: Boolean): Boolean = ???

src/main/scala/infix/Infix.scala

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/infix/Infix.scala

Board Game ⭐️

The goal of this exercise is to implement a made-up board game inspired by the game Civilization VI. The world of boardgame is composed of hexagonal tiles arranged on a cylinder (that is, they wrap around on the X-axis). This is represented by the class WorldMap in defs.scala. The tiles of the world are stored in a one-dimensional list and are ordered from left to right, bottom to top.

A tile (defined in defs.Tile) is made of the following:

a base that describes the kind of tile (mountain, hill, coast, etc.)
optionally, a feature such as a forest
optionally, a resource such as iron
optionally, a construction that is one of the following:
- a city center
- an exploitation that “improves” a resource (increasing their yields, which is discussed in Task 1)
- a district, such as a campus; it can be seen as an “extension” to the city, though it does not need to be adjacent to the city center

Tiles have yields (described as a non-negative number, in defs.scala) representing how valuable they are. There are 4 kinds of yields: food, production, coins and science. The base yield depends on the kind of the tile, and is increased by the presence of a feature or resource. It can be further increased by an exploitation. A tile may produce multiple kinds of yields. If it does not produce a yield of any kind, its value is zero.

Warm-up: Tile Access

Implement the tile extension method for WorldMap in BoardGame.scala that, for given x and y, returns the tile at that position. The bottom-left of the map is defined to be at the position (0, 0). Remember that the tiles are ordered from left to right, bottom to top and that the X-axis wraps around.

The following should hold:

val G = Tile(TileBase.FlatTerrain(BaseTerrain.Grassland))
val X = Tile(TileBase.HillTerrain(BaseTerrain.Desert))
val Y = Tile(TileBase.Mountain)
val Z = Tile(TileBase.Lake)
val tiles = (
        G :: Z :: G :: G :: G ::
      G :: G :: G :: Y :: G ::
    G :: X :: G :: G :: G ::
  G :: G :: G :: G :: G :: Nil()
)
val wm = WorldMap(tiles, 5, 4)
assert(wm.tile(1, 1) == X)
assert(wm.tile(6, 1) == X) // wraps around X-axis
assert(wm.tile(3, 2) == Y)
assert(wm.tile(13, 2) == Y)
assert(wm.tile(1, 3) == Z)

Task 1: Yield Calculation

We are interested in calculating the yields of a tile. The yields are computed by summing the individual yields from the terrain, the feature (if any), the resource (if any) and the construction (if any). The exception to this rule is if the tile has a district. In this case, the yields for that tile are zero. We instead compute its adjacency bonus, discussed in Task 2.

The rules for the terrain are as follows:

For flat and hill terrains, plains add 1 food and 1 production, grasslands 2 food and tundra 1 food; desert and snow do not have yields. Additionally, hills provide one extra production
Lakes and coasts provide 1 food and 1 gold, whereas oceans only provide 1 food
Finally, mountains do not have yields

If a tile has a feature, the following yields are added:

Woods provide 1 production
Marshes and rainforests provide 1 food
Oasis provides 3 food and 1 coin
Geothermal fissures provide 1 science
Reefs provide 1 food and 1 science
Finally, floodplains provide the following depending on the base terrain:
- For plains and deserts, 2 food
- For grasslands, 1 food and 1 production

For tiles with a resource, the total yields are increased by:

1 food for fishes, rice and wheat
1 science for aluminum and iron
2 production for coal
2 coins for crabs
1 production for stone

The rules for the construction are as follows:

City centers do not add extra yields
Exploitations have the following yields:
- Farms and fishing boats produce 1 food
- Quarries and mines provide 1 production
- Lumber mills provide 2 productions
Remember that tiles having districts produce 0 total yields

Your task is to implement the yields extension method for Tile in BoardGame.scala according to the above rules. You may add extension methods for BaseTerrain, Feature and so on or auxiliary functions to help you implement Tile.yields.

Task 2: Adjacency Calculation

Districts also produce “yields” of their kind through their adjacency bonus. However, as swiftly mentioned in the previous task, the yield coming from the tile itself is nullified. The adjacency yields kind science for campuses, production for industrial zones and coins for commercial hubs. The adjacency bonus depends on the tiles or constructions adjacent to the district in question. The total adjacency bonus is the sum of all adjacent bonuses, rounded down.

All districts gain 0.5 of their respective yield for each adjacent city center or district. The adjacency bonus is further enhanced by the following:

For campuses:
- 2 for each reef or geothermal fissure
- 1 for each mountain
- 0.5 for each rainforest
For industrial zones:
- 1 for each quarry, iron or aluminum
- 0.5 for each lumber mills or mine

Implement the adjacencyBonus function in BoardGame.scala, that, given a WorldMap and a position (x, y) calculates the adjacency bonus for the district placed at that tile. If there are no district, it should return 0. You are not allowed to use floating point (Double or Float): instead, the calculation should proceed by having all yields doubled before having the total sum being divided by two, rounded down.

Task 3: City Settlement

For this final task, we will implement the rule for settling down new cities in BoardGame.validCitySettlement. Given a WorldMap and a position (x, y), a city can be settled down on that tile if all these requirements are met:

The tile is a flat or hill terrain
There are no other cities or districts on that tile (exploitation is allowed, since these are removed upon settling)
No other cities are within a 2-tiles radius

For the last rule, we split the task into 3 parts.

Part A

We are first going to compute the list of all tiles situated at the ring radius from a tile at (x, y) in BoardGame.collectTilesInRing. If radius is zero, the tile at (x, y) should be returned. The traversal must happen clockwise and start at the top-right corner of the hexagon. If, during the traversal, a tile happens to be outside (in y) of the world, it should be skipped. Note that the precondition require(2 * radius < wm.width) ensures that all tiles in x are within bounds and are not repeated due to wrapping.

Part B

With the help of collectTilesInRing, implement BoardGame.allTilesWithinRadius that should collect all tiles within radius from a tile at (x, y). The tile at (x, y) must be included as well. The list of tiles must be ordered from inwards to outwards.

Part C and putting it all together

We are almost there! It remains to fill noOtherCitiesInRange that returns true if there are no cities within 2 tiles from (x, y) and false otherwise. Then, validCitySettlement may be completed.

Notes

You are only allowed to modify the file BoardGame.scala. You are provided with a custom implementation of List you must use instead of Scala’s List, as well as a custom implementation of Option you must use instead of Scala’s Option.

Scala’s match expressions let you handle multiple cases in a single case statement, for example:

  res match
    case Resource.Crabs => Yields(coins = 2)
    case Resource.Fish | Resource.Rice | Resource.Wheat => Yields(food = 1)

However, in this exercise, you should not use this feature, as it is not currently supported by our grader. Please copy the logic for each case separately instead:

  res match
    case Resource.Crabs => Yields(coins = 2)
    case Resource.Fish => Yields(food = 1)
    case Resource.Rice => Yields(food = 1)
    case Resource.Wheat => Yields(food = 1)

Once you are done, submit the following file to the Moodle assignment for this exercise:

src/main/scala/boardgame/BoardGame.scala