Imperative Programming

Methods

  method MethodName<T>(x: T, y: string) {
    print x;
    print y;
  }

• Methods can have side effects
• The body of a method is a sequence of statements
• Unlike an expression, a statement does not produce a value
• A method can have type parameters

Statement: method call

  method Call() {

    MethodName("Hello, ", "World\n");

  }

• A method call is a statement

Statement: variable declaration

  method VariableDeclaration() {

    var x: int := integerExpression;

  }

• The Right-Hand Side (RHS) of := is a RHS expression
• A RHS expression produces a value and may have side effects
• An expression is a (side-effect free) RHS expression
• The type of a local variable can often be inferred, in which case it can be omitted

Statement: assignment

  method Assignment() {

    var x := integerExpression;
    x := x + 1;

  }

• The Left-Hand Side (LHS) of := is an $\ell$-value
• An $\ell$-value is an expression that denotes a variable or location

Example variable declarations and assignments

  method Assignment() {

    var w: int := integerExpression;

    var x: int;
    x := integerExpression;

    var y := integerExpression;

    var z;
    z := integerExpression;

  }

Method out-parameters

  method MultipleInsAndOuts(a: int, b: int) returns (x: int, y: int) {

    x := a + b;
    y := x + 1;

  }

• A method can have both in-parameters and out-parameters
• Out-parameters are named, just like in-parameters
• In the method body, out-parameters can be used as local variables
• The values of the out-parameters on exit from the method body are returned to the caller

Statement: return

  method MultipleInsAndOuts(a: int, b: int) returns (x: int, y: int) {

    x := a + b;
    y := x + 1;
    return;
    y := 500; // this statement is never reached

  }

• A method exits upon reaching the method body's }
• A return statement abruptly exits the body of a method
  • A return is like a control-flow jump to the method body's }

Statement: return with arguments

  method Return() returns (o: int) {

    return integerExpression;

  }

  method ReturnArgumentsMeaning() returns (o: int) {

    o := integerExpression;
    return;

  }

• Instead of first assigning to the out-parameters and then exiting, the return statement can be used with arguments, which are assigned to the out-parameters

Statement: method call with out-parameter

  method Calls() {

    var s: int := Return();
    var x, y := MultipleInsAndOuts(20, 30);

  }

• A method call with out-parameters is an RHS expression

Statement: conditional

  method If() {

    if booleanExpression {
      // ...
    }

  }

Statement: alternative conditional

  method IfElse() {

    if booleanExpression {
      // ...
    } else {
      // ...
    }

  }

Statement: cascading if

  method CascadingIf() {

    if booleanExpressionA {
      // ...
    } else if booleanExpressionB {
      // ...
    } else {
      // ...
    }

  }

Statement: while loops

  method WhileLoop() {

    while booleanExpression {
      // ...
    }

  }

• The control flow of loops can be modified with break and continue statements

Statement: for loops

  method ForLoop() {

    for x := loExpression to hiExpression {
      // ...
    }

    for x := hiExpression downto loExpression {
      // ...
    }

  }

• The bounds loExpression and hiExpression of each loop are evaluated once, on entry to the loop
• Each loop above requires loExpression <= hiExpression
• The bounds in each loop are a half-open interval
  • In each loop body, the value of x satisfies loExpression <= x < hiExpression

Statement: match

  method Match() {

    match datatypeValue {
      case Case1 => // ...
      case Case2 => // ...
    }

  }

• Any local variables declared in a case are in scope in just that case
  • No additional { } needed
• The case conditions must cover all possibilities
  • It is an error if a program reaches a match where no case applies

Failure-compatible types

  datatype Status<T> =
    | Success(value: T)
    | Failure(error: string)
  {

    predicate IsFailure() { this.Failure? }

    function PropagateFailure(): Status<T> { this }

    function Extract(): T { this.value }

  }

• A failure-compatible type is a type with the members IsFailure, PropagateFailure, and Extract
• Failure-compatible types are related to monads in functional programming

Statement: failure-propagating assignment

  method Callee(i: int) returns (r: Status<int>)
  {
    if i < 0 {
      return Failure("negative");
    }
    return Success(i);
  }

  method Caller(i: int) returns (r: Status<int>)
  {
    var x: int :- Callee(i);
    return Success(x + 5);
  }

  method CallerMeaning(i: int) returns (r: Status<int>)
  {
    var tmp: Status<int> := Callee(i);
    if tmp.IsFailure() {
      return tmp.PropagateFailure();
    }
    var x: int := tmp.Extract();

    return Success(x + 5);
  }

• The assignment operator :- is commonly known as the “elephant operator”

Arrays

• Dafny has arrays
• Unlike collections we have seen so far, arrays are mutable
• An expression cannot modify an array, but a statement can
• Consequently, a function cannot modify an array, but a method can

Array rhs expression: creation

  method Allocate<T>(size: int) returns (arr: array<T>) {
    arr := new T[size];
  }

• new is a RHS expression

References

  method Aliasing() {

    var arr := new int[100];
    var brr := arr;

  }

• We commonly speak of arr as an array, but technically:
  • arr is a reference to an array
  • arr points to the array
• So is brr, and it refers to the same array as arr
• This is known as aliasing

Allocatedness

  predicate Null<T>() { null is array?<T> }

  predicate IsNull<T>(arr: array?) { (arr == null) is bool }

• There are two flavors of the array type
  • array<T> is the type of T-array references
  • array?<T> additionally contains the value null

Array functional expressions

  predicate Indexing<T>(arr: array<T>, index: int) { arr[index] is T }

  predicate Length<T>(arr: array<T>) { arr.Length is int }
  
  predicate ToSequence<T>(arr: array<T>) { arr[..] is seq<T> }

Array $\ell$-value: update

  method Update<T>(arr: array<T>, index: int, value: T) {
    arr[index] := value;
  }