2 Dafny Basics

Technically, this program does return a sorted list, so we had to give full credit. The issue, of course, was that the problem statement was underspecified.

So what should the specification have been?

The returned list must be sorted in non-decreasing order.
The returned list must include items from the input.

But this is insufficient. For example, given input [1; 4; 5; 4], a program could return [1; 4; 5; 5]. This list is sorted and contains only elements from the input, yet it replaces one of the 4s with a 5. Clearly, that is incorrect.

The correct specification should state:

The returned list must be sorted in non-decreasing order.
The returned list must be a permutation of the input list.

Now, even with a correct specification, how do we know if an implementation is correct?

Most of the time, we rely on testing: provide sample inputs, check outputs, and declare the program correct if it passes. But is that really enough? Passing a handful of test cases does not guarantee correctness.

In safety-critical domains—such as aerospace, medical devices, or finance—even small errors can cause catastrophic failures. So how much testing is “enough”?

As Edsger Dijkstra famously put it:

"Testing shows the presence, not the absence, of bugs."

This quote highlights a fundamental limitation of testing: while it can demonstrate that bugs exist, it can never guarantee that there are no bugs.

For some critical systems, we need to go beyond testing—we need to prove that a program is correct.

This is where tools like Dafny come in: they are built to help formally verify that programs meet their specifications, ensuring correctness by design.

This is where Dafny comes in. Dafny is a verification-aware programming language with built-in support for specifications and a static program verifier. It can automatically check that an implementation satisfies its specification. Once a program is verified, no further testing is necessary. Dafny programs can also be compiled into C#, Java, JavaScript, Go, and Python.

With Dafny, you can prove properties such as:

Guarantee array indices stay in bounds
Guarantee no null dereferences
Guarantee no division by zero
Guarantee the program conforms to a specification

2.2 Getting Started with Dafny🔗

Before we begin, please install Dafny by following the instructions at https://dafny.org/dafny/Installation.

You can verify that Dafny is correctly installed by running the following commands:

shell

> dafny --version
4.11.0
> dotnet --version
9.0.305

A Dafny program (stored in a file with the .dfy extension) consists of a set of declarations. Below is a simple "Hello, World" program written in Dafny:

Dafny

method Main() {
 assert 1 == 1;
  print "hello, world\n";
}

Dafny’s primary strength lies in its ability to verify program correctness at compile time, ensuring the absence of common runtime errors such as null dereferences, array out-of-bounds access, or division by zero. This verification is performed statically—without requiring a traditional runtime environment.

Once a program passes verification, Dafny compiles it into code for a target programming language such as C#, Java, JavaScript, Go, or Python. The resulting code runs within the runtime environment of the target language (e.g., the .NET runtime for C#, the Java Virtual Machine for Java, etc.).

Running a Dafny Program in Visual Studio Code

You can execute a Dafny program directly from VS Code using one of the following methods:

Press F5
Use the Command Palette and search for Dafny: Run
Right-click in the editor window and select Dafny > Run

Running from the Command Line

shell

> dafny run hello.dfy

Dafny program verifier finished with 1 verified, 0 errors
hello, world

2.3 Types🔗

Dafny has various inbuild types:

bool for booleans
char for characters
real, int, nat for real, unbounded and natural numbers
set<T>, seq<T> for immutable finite sets
array<T> for arrays
seq<T> for representing an immutable ordered list, queues, stacks, etc.
multiset<T> Multisets are like sets in almost every way, except that they keep track of how many copies of each element they have.
object is a super-type of all reference types

2.4 Methods🔗

Methods in Dafny are like functions or procedures in conventional languages. Input parameters and output arguments are typed as follows:

Dafny

method Add(x: int, y: int) returns (sum: int){
  sum := x + y;
}

Input parameters are immutable. The output parameter is mutable and works like a local variable. A ‘return‘ statement is not necessary in a method, but if there is one, it need not have arguments or it must have all the return arguments of the method.

Dafny

method Add(x: int, y: int) returns (sum: int){
  var s := x + y;
  return s;
}

Dafny

method Add(x: int, y: int) returns (sum: int){
  var s := x + y;
  sum := s;
  return;
}

Here is another example:

Dafny

method Abs(x: int) returns (y: int){
  if x < 0 {
    return -x;
  } else {
    return x;
  }
}

2.5 Functions🔗

Functions in Dafny side effect free and consist of a single expression that yields a value of some type.

Dafny

function double(a:int): int{
  a * 2
}

If a function is declared a ghost function, it is only used for verification.

Dafny

ghost function abs(a:int): int{
  if a > 0 then a else -a
}

2.6 Predicates🔗

A predicate is used for verification only. It is a special type of function in that it returns a bool only.

Dafny

predicate Even(x : int) {x % 2 == 0}

2.7 Main()🔗

The main method takes no input parameters and is the entry point of the program.

Dafny

method Main() {
 assert 1 == 1;
 print "hello, world\n";
}

2.8 Pre- and Postconditions🔗

The real power of Dafny comes from the ability to annotate these methods to specify their behavior. For example, one property that we observe with the Abs method is that the result is always greater than or equal to zero, regardless of the input. We could put this observation in a comment, but then we would have no way to know whether the method actually had this property. Further, if someone came along and changed the method, we wouldn’t be guaranteed that the comment was changed to match. With annotations, we can have Dafny prove that the property we claim of the method is true. There are several ways to give annotations, but some of the most common, and most basic, are method pre- and postconditions.

This property of the Abs method, that the result is always non-negative, is an example of a postcondition: it is something that is true after the method returns. Postconditions, declared with the ensures keyword, are given as part of the method’s declaration, after the return values (if present) and before the method body. The keyword is followed by the boolean expression. Like an if or while condition and most specifications, a postcondition is always a boolean expression: something that can be true or false. In the case of the Abs method, a reasonable postcondition is the following:

Dafny

method Abs(x: int) returns (y: int)
  ensures 0 <= y
{
  if x < 0 {
    return -x;
  } else {
    return x;
  }
}

We can have multiple postconditions:

Dafny

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
  ensures less < x
  ensures x < more
{
  more := x + y;
  less := x - y;
}

The postcondition can also be written:

Dafny

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
  ensures less < x && x < more
{
  more := x + y;
  less := x - y;
}

or even:

Dafny

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
  ensures less < x < more
{
  more := x + y;
  less := x - y;
}

Preconditions have their own keyword, requires. We can give the necessary precondition to MultipleReturns as below:

Dafny

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
  requires 0 < y
  ensures less < x < more
{
  more := x + y;
  less := x - y;
}

2.9 Assertions🔗

Unlike pre- and postconditions, an assertion is placed somewhere in the middle of a method. Like the previous two annotations, an assertion has a keyword, assert, followed by the boolean expression and the semicolon that terminates simple statements. An assertion says that a particular expression always holds when control reaches that part of the code. For example, the following is a trivial use of an assertion inside a dummy method:

Dafny

method Testing()
{
  assert 2 < 3;
  // Try "asserting" something that is not true.
  // What does Dafny output?
}

Another example:

Dafny

method Square(x: int) returns (y: int)
  requires x >= 0
  ensures y == x*x
  {
    y := x*x;
    assert y > x;
  }

2.10 Compiling Dafny to Java🔗

Let us comoile a simple Dafny program to Java and run the compiled Java code.

The following dafny code ‘min.dfy‘ calculates the minimum of two integers.

min.dfy
  function Minimum (x : int, y : int):(m : int)
  ensures m <= x && m <= y
  ensures m == x || m == y
  {
      if x <= y then x else y
  }

  method Min (x : int, y : int) returns (m : int)
  ensures m == Minimum(x,y)
  {
      if (x < y) {
          m := x;  // Could also use "return x"
      }
      else {
          m := y;
          // return y;  // Could also use " m := y"
      }
  }

  method Main ()
  {
      var x := Min(2,1);
      print "Minimum is ", x;
  }

Now, we can compile ‘min.dfy‘ to Java:

shell

> dafny build -t:java min.dfy

Dafny program verifier finished with 3 verified, 0 errors

We can also run the Java code:

shell

> java -jar min.jar
Minimum is 1

Now, let us look at the generated Java code. First, we decompile the JAR. (For this example, I used https://www.decompiler.com/jar to decompile.)

package _System;

import dafny.CodePoint;
import dafny.DafnySequence;
import java.math.BigInteger;

public class __default {
   public static BigInteger Minimum(BigInteger var0, BigInteger var1) {
      return var0.compareTo(var1) <= 0 ? var0 : var1;
   }

   public static BigInteger Min(BigInteger var0, BigInteger var1) {
      BigInteger var2 = BigInteger.ZERO;
      if (var0.compareTo(var1) < 0) {
         var2 = var0;
      } else {
         var2 = var1;
      }

      return var2;
   }

   public static void Main(DafnySequence<? extends DafnySequence<? extends CodePoint>> var0) {
      BigInteger var1 = BigInteger.ZERO;
      BigInteger var2 = BigInteger.ZERO;
      var2 = Min(BigInteger.valueOf(2L), BigInteger.ONE);
      System.out.print(DafnySequence.asUnicodeString("Minimum is ").verbatimString());
      System.out.print(String.valueOf(var2));
   }

   public static void __Main(DafnySequence<? extends DafnySequence<? extends CodePoint>> var0) {
      Main(var0);
   }

   public String toString() {
      return "_module._default";
   }
}

2.11 Compiling Dafny to Python🔗

abs.dfy
  method Abs(x: int) returns (y: int)
    ensures x < 0 ==> y == -x
    ensures x >= 0 ==> y == x
  {
    if (x < 0){
      y := -x;
    }else{
      y := x;
    }
  }

  method Test1(x: int)
  {
    var v := Abs(x);
    assert x > 0 ==> v == x;
    assert x < 0 ==> v == -x;

    var v1 := Abs(3);
    assert v1 == 3;

    var v2 := Abs(-3);
    assert v2 == 3;

  }

shell

> dafny verify abs.dfy

Dafny program verifier finished with 2 verified, 0 errors

shell

> dafny translate py abs.dfy

Dafny program verifier finished with 2 verified, 0 errors

shell

> cat abs-py/module_.py
import sys
from typing import Callable, Any, TypeVar, NamedTuple
from math import floor
from itertools import count

import module_ as module_
import _dafny as _dafny
import System_ as System_

# Module: module_

class default__:
    def  __init__(self):
        pass

    @staticmethod
    def Abs(x):
        y: int = int(0)
        if (x) < (0):
            y = (0) - (x)
        elif True:
            y = x
        return y

    @staticmethod
    def Test1(x):
        d_0_v_: int
        out0_: int
        out0_ = default__.Abs(x)
        d_0_v_ = out0_
        d_1_v1_: int
        out1_: int
        out1_ = default__.Abs(3)
        d_1_v1_ = out1_
        d_2_v2_: int
        out2_: int
        out2_ = default__.Abs(-3)
        d_2_v2_ = out2_

We can see that Dafny to Java compiler generated human readable Java code. Please read the instruction at https://dafny.org/dafny/Installation to comoile Dafny code to other languages, such as C#, Go, Python, and JavaScript.

contents ← prev up next →

	Syllabus
	Texts
	Schedule
	Notes
	Assignments
	Midterms
	Final
	Software

1	Dafny Cheatsheet
2	Dafny Basics
3	Getting Started with Dafny
4	Dafny Collections
5	Floyd Hoare Logic
6	Inductive Proofs
7	Inductive Types
8	Sorting
9	Loop Invariants
10	Arrays
11	SAT Solvers

2.1	Why Dafny?
2.2	Getting Started with Dafny
2.3	Types
2.4	Methods
2.5	Functions
2.6	Predicates
2.7	Main()
2.8	Pre- and Postconditions
2.9	Assertions
2.10	Compiling Dafny to Java
2.11	Compiling Dafny to Python