►CMSC 433:   Programming Language Technologies and Paradigms
▼Notes
►3 Getting Started with Dafny
On this page:
3.1 Methods and Specification
3.2 Control Paths
3.3 Method Contracts
3.4 Underspecification
3.5 Multiple Postconditions
3.6 Functions
3.7 Compiled vs Ghost
8.17
    contents    up   

3 Getting Started with Dafny🔗

    3.1 Methods and Specification

    3.2 Control Paths

    3.3 Method Contracts

    3.4 Underspecification

    3.5 Multiple Postconditions

    3.6 Functions

    3.7 Compiled vs Ghost

3.1 Methods and Specification🔗

In this lecture, we review some basics of Dafny programming and learn how to write simple specification. We include multiple numbered versions, to capture different edits made in class.

Dafny

method Triple(x: int) returns (r: int) {
  var y := 2 * x;
  r := x + y;
}

This method takes an integer x and returns an integer r. The body of the method is a list of statements. A method can have any number of input argumements and return values. The input arguments are read-only. The return parameters are like local variables and can be assigned values. When the method terminates, the final value of the out-parameters will be returned.

Here is a method that calls the method Triple

Dafny

method Caller() {
  var t := Triple(18); //sets t to 54
}

Calling Triple with 18 will set t to 54, which is 3 * 18. In the following lectures, we will learn how to turn comments like this into conditions that we can prove to be true.

We can add assrt statements to explicitly state the fact that it returns the value 3 * x.

Dafny

method Triple(x: int) returns (r: int) {
  var y := 2 * x;
  r := x + y;
  assert r == 3 * x;
}

It is good practice to use assertions to express non-obvious conditions in your code. If an assertion fails (i.e., the condition of the assertion evaluates to false), then the program contains an error. For example:

Dafny

method Triple2(x: int) returns (r: int) {
  var y := 2 * x;
  r := x + y;
  //assert r == 10 * x;
  //assert r < 5; // Very surprising this one is accepted by Dafny!  Do you see why?
  //assert false;
}

The first assertion may not always hold. However, if the first assertion does hold — where 

r == 10 * x ==> 3 * x == 10 * x ==> x == 0 ==> r < 5
then the second assertion always holds as well. Therefore, in VS Code, the Dafny verifier does not complain about assert r < 5;. The third assertion always fails, regardless of whether the first and second assertions pass or fail.

3.2 Control Paths🔗

A program with with if statements, it is correct if all control paths are correct. Here is the method Triple with if statement:

Dafny

method Triple3(x: int) returns (r: int) {
  if x == 0 {
    r := 0;
  } else {
    var y := 2 * x;
    r := x + y;
  }
  assert r == 3 * x;
}

When reasoning about the if statement, in the control path through the "then" (true) branch, x == 0, and in the control path through the "else" (false) branch, x != 0.

3.3 Method Contracts🔗

Dafny

method Caller() {
  var t := Triple(18);
  assert t < 100;
}

We know from the implementation of Triple that t == 54. However, the assertion fails because the caller should not be able to see the implementation of Triple. This encapsulation allows Triple to change its implementation without affecting the caller.

A method can include specifications, which describe the behavior of the method. A specification essentially defines the contract between the caller and the method, outlining what the method is expected to do.

A specification, or method contract, has two parts: a precondition and a postcondition. The precondition must hold when the method is called, and the postcondition must hold when the method terminates. The precondition is introduced using the requires keyword, and the postcondition is introduced using the ensures keyword.

Dafny

method Triple4(x: int) returns (r: int)
  ensures r == 3 * x
{
  var y := 2 * x;
  r := x + y;
}

method Caller2() {
  var t := Triple4(18);
  assert t < 100;
}

Let us add a precondition that requires the input arguments must be even numbers:

Dafny

method Triple5(x: int) returns (r: int)
  requires x % 2 == 0
  ensures r == 3 * x
{
  var y := 2 * x;
  r := x + y;
}

Now, Triple can change its implementation without breaking the caller, as long as it meets its specification.

Dafny

method Triple5(x: int) returns (r: int)
  requires x % 2 == 0
  ensures r == 3 * x
{
  var y := x / 2;
  r := 6 * y;
}

3.4 Underspecification🔗

In the following example, the specification does not which number between 0 and n is returned.

We say "0 to n" to mean the values in the half-open interval [0, n), which includes 0, but does not include n.

That means the implementation is free to return any value n where 0 <= n <= n.

Dafny

method Index(n: int) returns (i: int)
  requires 1 <= n
  ensures 0 <= i < n
{
  i := n / 2;
}

This implementation is also correct.

Dafny

method Index2(n: int) returns (i: int)
  requires 1 <= n
  ensures 0 <= i < n
{
  i := 0;
}

Because the method is non-deterministic, the following assertions does not hold.

Dafny

method Doesn'tWork() {
  var x := Index(50);
  var y := Index(50);
  assert x == y;
}

3.5 Multiple Postconditions🔗

We can add multiple conditions by connecting them with &&, or using multiple separate ensures and requires.

Dafny

method Min0(x: int, y: int) returns (m: int)
  ensures m <= x && m <= y


method Min(x: int, y: int) returns (m: int)
  ensures m <= x && m <= y
  ensures m == x || m == y

3.6 Functions🔗

Dafny functions can be used in expressions. Therefore, we can use functions in specifications. In the following code, the method Triple’ uses the function Average in its specification.

Dafny

function Average(a: int, b: int): int {
  (a + b) / 2
}

method Triple'(x: int) returns (r: int)
  ensures Average(r, 3 * x) == 3 * x
{
  r := x + x + x;
}

Here is another example, where the function restricts the arguments of Average to non-negative values.

Dafny

function Average2(a: int, b: int): int
  requires 0 <= a && 0 <= b
{
  (a + b) / 2
}

method Triple6(x: int) returns (r: int)
  ensures r == 3 * x
{
  if 0 <= x {
    r := Average(2 * x, 4 * x);
  } else {
    r := -Average(-2 * x, -4 * x);
  }
}

3.7 Compiled vs Ghost🔗

The precondition construct requires, the postcondition construct ensures, and assert are used to specify the behavior of a program. These are used by the Dafny verifier but are erased when the program is compiled. Any statement, variable, or declaration that is used only for specification is called a ghost. To declare a method, function, or variable as a ghost, simply add the keyword ghost in front. Compiled code should not rely on ghost constructs.

Dafny

/*method IllegalAssignment() returns (y: int) {
  ghost var x := 10;
  y := 2 * x;
}*/

ghost method DoubleQuadruple(x: int) returns (a: int, b: int)
  ensures a == 2 * x && b == 4 * x
{
  a := 2 * x;
  b := 2 * a;
}

method Triple7(x: int) returns (r: int)
  ensures r == 3 * x
{
  var y := 2 * x;
  r := x + y;
  ghost var a, b := DoubleQuadruple(x);
  assert a <= r <= b || b <= r <= a;
}

    contents    up