Typed Parameters and Return Values

Slang methods have zero or more parameters that must be given explicit types. Slang also requires return types to be explicitly declared (this is a restriction of Scala – Scala allows method return types to be omitted and automatically inferred):

  def abs(n: Z): Z = {  // method is declared with typed parameters and a return type
    var result: Z = 0
    if (n >= 0) {
      result = n
    } else {
      result = -n
    }
    return result  // return statement is required for methods returning a value
  }
  assert(abs(4) == 4)     // checking simple correctness properties
  assert(abs(-10) == 10)

  def less(n1: Z, n2: Z): B = {
    return n1 < n2  // return argument can be an expression
  }

Return Statements / Expressions

Slang requires an explicit return statement/expression for every method that returns a value (this is a restriction of Scala, which allows the return keyword to be omitted (e.g., in Scala, the less method body can simply be n1 < n2).

Multiple returns within a method body are allowed, as illustrated below. While this sometimes allows to be more concise (and even more readable), it may make verification activities more difficult:


  def absMultiReturn(n: Z): Z = {
    if (n >= 0) {
      return n  // multiple returns are allowed, but may make analysis and proofs more complicated
    } else {
      return -n
    }
  }

Methods can have no parameters, and they don’t have to return a value. When methods don’t return a value, Unit is used as the return type and the return statement can be omitted:


  def printHelloWorld(): Unit = { // return type is always required, Unit means it does not return a value
    println("Hello World")
    // return               // return not required when not returning a value
  }

  printHelloWorld() // method call with zero parameters

Warning

ToDo: To John: Address the following

  • Pure annotations
  • Rules for aliasing
  • Pass by value vs pass by reference
  • In previous section on assignment, addressing copying semantics and value-based equality
  • can formal parameters be assigned to in method body (there contents can be modified, but can the identifier itself be assigned to