Lab for Automated Reasoning and Analysis LARA

Homework 06

Due Wednesday, 17 November, 10:10am. Please hand it in to Hossein before the beginning of the exercise session.

Problem 1

Determine if the following piece of codes type check according to the type rules.

a) The class Array has a field length in which the length of the array is stored.

def swap(lst: Array[Int], a: Int, b: Int): Array[Int] = {
  if (a >= lst.length || b >= lst.length) lst else {
    val swap = lst(a)
    lst(a) = lst(b)
    lst(b) = swap


For solving this part you have to write down the type rule corresponding to new.

class Shape
class Rectangle(width: Int, length: Int) extends Shape {
  def area : Int = width * length
class Square(length: Int) extends Rectangle(length,length)
new Square(5).area

Problem 2

We can partition the set of positive integers $\mathbb{N}^{+} = \{1,2,3,\cdots\}$ into the set of $\textit{even}=\{2,4,6,\cdots\}$ and the set of $\textit{odd}=\{1,3,5,\cdots\}$ numbers.
Assume that we have the types pos, even and odd in a programming language. Give the type rules for addition, multiplication, division and exponentiation.
For division, consider the following cases.

  • Division rounds up the result: x / y is interpreted as $\lceil x/y\rceil$.
  • Division returns the quotient: x / y is interpreted as $\lfloor x/y\rfloor$.

Specify in which case(s) there may be run-time error. Is there any way to prevent the run-time error at the type checking phase?

cc10/homework_06.txt · Last modified: 2010/11/11 19:18 by hossein