Programming in Dafny

Overview

• Dafny is a statically and strongly typed programming language
• A functional program is essentially made of three kinds of definitions
  • Functions
  • Constants
  • Datatypes
  • Type synonyms

Function declaration

• Here is an example function definition

  function FunctionName(x: X, y: Y): R {
    expression
  }

• Declared with the keyword function
• Has a name: FunctionName
• Has typed parameters: x and y, respectively of types X and Y
• Has a return type: R
• Has a body: expression

Function body

• The body of a function is an expression
• An expression has a type
• An expression can be evaluated and produces a value of that type
• Evaluating an expression has no side effect

Calling a function

  function F(n: int, m: int): int {
    n + m
  }

  function G(n: int): int {
    F(n + n, n * n)
  }

• To call a function, the type of the arguments must match that of the parameters
• Arguments are evaluated before the function is called
• The arguments are then substituted in the body of the function
• The type of the expression must match the return type

Constants

• The arity of a function is the number of parameters
• A constant is a function with arity 0, written without the parentheses
• Declared with the keyword const

  const constantName: Type := expression

Predicates

• A function whose return type is bool is also called a predicate
• Declared with keyword predicate
• Return type is implicit

  predicate predicateName(x: X, y: Y) {
    booleanExpression
  }

Expressions

• We will now introduce the language of expressions
• We call this set of expressions “functional expressions”
  • There will be others
• Dafny has 5 primitive scalar types:
  • Booleans (bool)
  • Integers (int)
  • Reals (real)
  • Characters (char)
  • Bit vectors (bv0, bv1, bv2, …, bv32, …)

Type test

• Every expression has a type
• There is an expression to test if an expression is of a certain type
• It uses the keyword is
• It evaluates to a Boolean value
• We will use that expression and predicates to introduce the syntax and types of expressions in Dafny
• That way, you learn Dafny by reading Dafny

  predicate IntPlus3IsInt(n: int) { (n + 3) is int }

Booleans

  predicate False() { false is bool }

  predicate True() { true is bool }

  predicate Conjunction(a: bool, b: bool) { (a && b) is bool }

  predicate Disjunction(a: bool, b: bool) { (a || b) is bool }

  predicate Implication(a: bool, b: bool) { (a ==> b) is bool }

  predicate Explication(a: bool, b: bool) { (a <== b) is bool }

  predicate Equivalence(a: bool, b: bool) { (a <==> b) is bool }

  predicate Negation(a: bool) { !a is bool }

Integers

  predicate DecimalLiteral() { 38 is int }
  predicate HexadecimalLiteral() { 0xBadDecaf is int }
  predicate ReadableLiteral() { 4_345_765 is int }
  predicate Negation(n: int) { -n is int }
  predicate Addition(n: int, m: int) { (n + m) is int }
  predicate Substraction(n: int, m: int) { (n - m) is int }
  predicate Multiplication(n: int, m: int) { (n * m) is int }
  predicate Division(n: int, m: int) { (n / m) is int }
  predicate Modulus(n: int, m: int) { (n % m) is int }
  predicate Equality(n: int, m: int) { (n == m) is bool }
  predicate Disequality(n: int, m: int) { (n != m) is bool }
  predicate SmallerOrEqual(n: int, m: int) { (n <= m) is bool }
  predicate Smaller(n: int, m: int) { (n < m) is bool }
  predicate GreaterOrEqual(n: int, m: int) { (n >= m) is bool }
  predicate Greater(n: int, m: int) { (n > m) is bool }

Reals

  predicate DecimalLiteral() { 38.98 is real }
  predicate ReadableLiteral() { 4_345_765.999_987 is real }
  predicate Negation(n: real) { -n is real }
  predicate Addition(n: real, m: real) { (n + m) is real }
  predicate Substraction(n: real, m: real) { (n - m) is real }
  predicate Multiplication(n: real, m: real) { (n * m) is real }
  predicate Division(n: real, m: real) { (n / m) is real }
  predicate Equality(n: real, m: real) { (n == m) is bool }
  predicate Disequality(n: real, m: real) { (n != m) is bool }
  predicate SmallerOrEqual(n: real, m: real) { (n <= m) is bool }
  predicate Smaller(n: real, m: real) { (n < m) is bool }
  predicate GreaterOrEqual(n: real, m: real) { (n >= m) is bool }
  predicate Greater(n: real, m: real) { (n > m) is bool }
  predicate IntegerToReal(k: int) { (k as real) is real }
  predicate Floor(n: real) { (n.Floor) is int }

Characters

• Characters are Unicode

  predicate ASCII() { 'a' is char }
  predicate SingleQuote() { '\'' is char }
  predicate DoubleQuote() { '\"' is char }
  predicate BackSlash() { '\\' is char }
  predicate NullCharacter() { '\0' is char }
  predicate LineFeed() { '\n' is char }
  predicate CarriageReturn() { '\r' is char }
  predicate Tab() { '\t' is char }
  predicate Unicode() { '\U{1F71D}' is char }
  predicate Addition(a: char, b: char) { (a + b) is char }
  predicate Substraction(a: char, b: char) { (a - b) is char }
  predicate Less(a: char, b: char) { (a < b) is bool }
  predicate LessEqual(a: char, b: char) { (a <= b) is bool }
  predicate Greater(a: char, b: char) { (a > b) is bool }
  predicate GreaterEqual(a: char, b: char) { (a >= b) is bool }

Other expressions

  predicate ConditionalExpression<T>(bexpr: bool, expr1: T, expr2: T)  { 
    (if bexpr then expr1 else expr2) is T
  }

  predicate LetBinding<U, V>(expr1: U, expr2: V) { (var x := expr1; expr2) is V }

  predicate Tuple<T, U, V>(t: T, u: U, v: V) { (t, u, v) is (T, U, V) }

  predicate TupleAccess0<T, U, V>(tup: (T, U, V)) { tup.0 is T }

  predicate TupleAccess1<T, U, V>(tup: (T, U, V)) { tup.1 is U }

  predicate TupleAccess2<T, U, V>(tup: (T, U, V)) { tup.2 is V }

• Despite what the name suggests, x is not a mutable variable
• x cannot be updated, it is just a name for the value of expr1
• You can replace x with expr1 in expr2 without changing the value of the expression

Functions are first-class citizens

• A function can be passed as an argument to a function
• Type of a function
  • If parameters have types X, Y, Z
  • If return type is U
  • The type of the function is (X, Y, Z) -> U

Functions as in-parameters

  function Apply(f: int -> int, n: int): int {
    f(n)
  }

Functions as out-parameters

  function ApplyPartial(f: int -> int -> int, n: int): int -> int {
    f(n)
  }

Recursive functions

• A function definition can be recursive

  function Factorial(n: int): int {
    if n == 0 then 1 else n * Factorial(n - 1)
  }

New expression: anonymous functions and application

  predicate LambdaAbstraction<U, V>(expr: V) { ((x: U) => expr) is U -> V }

  predicate Application<U, V>(fun: U -> V, arg: U) { fun(arg) is V }

Algebraic datatypes

• Algebraic datatypes are a staple of functional programming
• As a first approximation, they are like an enumeration of possible values
• Here, the datatype defines two values, Small and Large

  datatype Size =
    | Small
    | Large

Type and constructors

• A datatype definition defines multiple things
  • A type whose name is that of the datatype definition
  • The possible values
  • Constructors for such values (in this simple case, the constructor and the value cannot be distinguished)

  predicate Constructor() { Small is Size }

Equality

• Simple datatypes support equality

  predicate Equality(a: Size, b: Size) { (a == b) is bool }

  predicate Disequality(a: Size, b: Size) { (a != b) is bool }

Pattern matching

• Pattern matching allows you to consider the possible values of a datatype

  function SizeToOunces(s: Size): int {
    match s
    case Small => 4
    case Large => 8
  }

New expression: pattern matching

  predicate MatchExpression(s: Size) {
    (match s case Small => 4 case Large => 8) is int
  }

Parameterized constructors

• Constructors can have parameters
• Example
  • Coffee is a constructor: it takes a value of type Size and produces a value of type Drink
  • Coffee(Small) is a value

  datatype Drink =
    | Coffee(Size)
    | Tea(Size)
    | Water(Size)

Applying constructors

  predicate Constructor() { (Tea(Small)) is Drink }

• Are constructors functions?
  • No
  • Coffee and Tea cannot be used without being fully applied

Matching constructors with parameters

  function GetCaffeine(d: Drink): int {
    match d
    case Coffee(s) => 5 * SizeToOunces(s)
    case Tea(s) => 7 * SizeToOunces(s)
    case Water(s) => 0
  }

Wild identifiers on arguments

• When you don't need to use a value and don't want to name it

  function GetCaffeine(d: Drink): int {
    match d
    case Coffee(s) => 5 * SizeToOunces(s)
    case Tea(s) => 7 * SizeToOunces(s)
    case Water(_) => 0
  }

Wild identifiers on constructors

  function GetCaffeine(d: Drink): int {
    match d
    case Coffee(s) => 5 * SizeToOunces(s)
    case Tea(s) => 7 * SizeToOunces(s)
    case _ => 0
  }

Named parameters

• Constructor parameters can be named

  datatype Drink =
    | Coffee(sz: Size)
    | Tea(sz: Size)
    | Water(sz: Size)

Discriminators and destructors

• Discriminator: test if a value correspond to a specific constructor
• Destructor: extract value for some constructor

  predicate Discriminator(d: Drink) { d.Coffee? is bool }

  predicate Destructor(d: Drink) { d.sz is Size }

Example with discriminators and destructors

  function GetCaffeine(d: Drink): int {
    if d.Coffee? then
      5 * SizeToOunces(d.sz)
    else if d.Tea? then
      7 * SizeToOunces(d.sz)
    else
      0
  }

Member declarations

• Functions can be defined along with datatype
  • That is, including constants and predicates
• In this context, the datatype value can be referred to as this

  datatype Size =
    | Small
    | Large
  {

    predicate This() { this is Size }

  }

Example with member function

  datatype Size =
    | Small
    | Large
  {

    function ToOunces(): int {
      match this
      case Small => 4
      case Large => 8
    }

  }

Functional dot notation

• You have functional programming with dot notation!
• For OO experts: no late binding, no dynamic dispatch, it's just syntactic convenience

  predicate DotExpression(s: Size) { s.ToOunces is () -> int }

Records

• Algebraic datatypes with a single constructor are also called records
• The single constructor usually has the same name as the datatype, but you can also choose a different name

  datatype Complex = Complex(r: real, i: real)

Type operators

• Datatypes can be parameterized with a type
• That way, you can define collections that are oblivious to what they contain
• List is a type operator: it takes a type as an argument and creates a new type

  datatype List<T> =
    | Nil
    | Cons(head: T, tail: List)

Polymorphism

• Functions can also be parameterized
• That way, you can not only define collections oblivious to what they contain
• But also functions on them that are also oblivious
• The parameters of a function can be typed with type parameters
• Type parameters always appear before parameters (prenex polymorphism)
• A parameterized type needs to be applied to a type argument

  function Len<T>(l: List<T>): nat {
    match l
    case Nil => 0
    case Cons(_, tail) => 1 + Len(tail)
  }

Type parameter inference

• In most cases, Dafny can infer that the type should be

  function Len<T>(l: List): nat {
    match l
    case Nil => 0
    case Cons(_, tail) => 1 + Len(tail)
  }

Type characteristics

• Sometimes, you want to constrain a type parameter
• It is done with type characteristics (of which there are 4 in Dafny)
• For example, you can demand that the type support equality

  function TestEquality<T(==)>(a: T, b: T): bool {
    a == b
  }

Collections

• Dafny has 4 built-in immutable collections for programming
  • Sequences (seq<T>)
  • Sets (set<T> and iset<T>)
  • Multisets (multiset<T>)
  • Maps (map<K, V> and imap<K, V>)
• Sets and maps come in two flavors: finite and possibly infinite
• Sequences and multisets are always finite
• The built-in type string is a type synonym for seq<char>
• The contents of these collections may be mutable, but the collections themselves are not

Sequences

  predicate Empty<T>() { [] is seq<T> }
  predicate SequenceDisplay<T>(x: T, y: T, z: T) { [x, y, z] is seq<T> }
  predicate Equality<T(==)>(a: seq, b: seq) { (a == b) is bool }
  predicate Disequality<T(==)>(a: seq, b: seq) { (a != b) is bool }
  predicate ProperPrefix<T(==)>(a: seq, b: seq) { (a < b) is bool }
  predicate Prefix<T(==)>(a: seq, b: seq) { (a <= b) is bool }
  predicate Concatenation<T>(a: seq, b: seq) { (a + b) is seq<T> }
  predicate Membership<T(==)>(a: seq, e: T) { (e in a) is bool }
  predicate Absence<T(==)>(a: seq, e: T) { (e !in a) is bool }
  predicate Size<T>(a: seq) { |a| is int }
  predicate Indexing<T>(a: seq, k: int) { a[k] is T }
  predicate Update<T>(a: seq, k: int, e: T) { a[k := e] is seq<T> }
  predicate Slice<T>(a: seq, k: int, l: int) { a[k..l] is seq<T> }
  predicate Drop<T>(a: seq, k: int) { a[k..] is seq<T> }
  predicate Take<T>(a: seq, l: int) { a[..l] is seq<T> }

Strings

• Strings are sequences of characters

  predicate Type(s: string) { s is seq<char> }

  predicate Display() { "Hello" is string }

Sets

  predicate EmptySet<T(==)>() { {} is set<T> }
  predicate SetDisplay<T(==)>(x: T, y: T, z: T) { {x, y, z} is set<T> }
  predicate Union<T(==)>(A: set<T>, B: set<T>) { (A + B) is set<T> }
  predicate Intersection<T(==)>(A: set<T>, B: set<T>) { (A * B) is set<T> }
  predicate AsymmetricDifference<T(==)>(A: set<T>, B: set<T>) { (A - B) is set<T> }
  predicate Equality<T(==)>(A: set<T>, B: set<T>) { (A == B) is bool }
  predicate Disequality<T(==)>(A: set<T>, B: set<T>) { (A != B) is bool }
  predicate Subset<T(==)>(A: set<T>, B: set<T>) { (A <= B) is bool }
  predicate StrictSubset<T(==)>(A: set<T>, B: set<T>) { (A < B) is bool }
  predicate Superset<T(==)>(A: set<T>, B: set<T>) { (A >= B) is bool }
  predicate StrictSuperset<T(==)>(A: set<T>, B: set<T>) { (A > B) is bool }
  predicate Disjoint<T(==)>(A: set<T>, B: set<T>) { (A !! B) is bool }
  predicate Membership<T(==)>(e: T, A: set<T>) { (e in A) is bool }
  predicate Absence<T(==)>(e: T, A: set<T>) { (e !in A) is bool }
  predicate Cardinality<T(==)>(A: set<T>) { |A| is int }

Multisets

  predicate EmptyMultiset<T(==)>() { multiset{} is multiset<T> }
  predicate MultisetDisplay<T(==)>(x: T, y: T, z: T) { multiset{x, y, z} is multiset<T> }
  predicate Union<T(==)>(A: multiset<T>, B: multiset<T>) { (A + B) is multiset<T> }
  predicate Intersection<T(==)>(A: multiset<T>, B: multiset<T>) { (A * B) is multiset<T> }
  predicate Difference<T(==)>(A: multiset<T>, B: multiset<T>) { (A - B) is multiset<T> }
  predicate Equality<T(==)>(A: multiset<T>, B: multiset<T>) { (A == B) is bool }
  predicate Disequality<T(==)>(A: multiset<T>, B: multiset<T>) { (A != B) is bool }
  predicate Submultiset<T(==)>(A: multiset<T>, B: multiset<T>) { (A <= B) is bool }
  predicate StrictSubmultiset<T(==)>(A: multiset<T>, B: multiset<T>) { (A < B) is bool }
  predicate Supermultiset<T(==)>(A: multiset<T>, B: multiset<T>) { (A >= B) is bool }
  predicate StrictSupermultiset<T(==)>(A: multiset<T>, B: multiset<T>) { (A > B) is bool }
  predicate Disjoint<T(==)>(A: multiset<T>, B: multiset<T>) { (A !! B) is bool }
  predicate Membership<T(==)>(e: T, A: multiset<T>) { (e in A) is bool }
  predicate Absence<T(==)>(e: T, A: multiset<T>) { (e !in A) is bool }
  predicate Cardinality<T(==)>(A: multiset<T>) { |A| is int }
  predicate Multiplicity<T(==)>(e: T, A: multiset<T>) { A[e] is int }
  predicate MultiplicityUpdate<T(==)>(e: T, A: multiset<T>, k: int) { A[e := k] is multiset<T> }

Maps

  predicate Empty<U(==), V>() { map[] is map<U, V> }
  predicate Display() { map[20 := true, 3 := false, 20 := false] is map<int,bool>}
  predicate KeyMembership<U(==), V>(m: map, k: U) { (k in m) is bool }
  predicate KeyAbsence<U(==), V>(m: map, k: U) { (k !in m) is bool }
  predicate Cardinality<U(==), V>(m: map) { |m| is int }
  predicate Indexing<U(==), V>(m: map, k: U) { m[k] is V}
  predicate Update<U(==), V>(m: map, k: U, v: V) { m[k := v] is map}
  predicate Keys<U(==), V>(m: map) { m.Keys is set<U> }
  predicate Values<U(==), V(==)>(m: map) { m.Values is set<V> }
  predicate Items<U(==), V(==)>(m: map) { m.Items is set<(U, V)> }
  predicate Merge<U(==), V>(m1: map, m2: map) { (m1 + m2) is map }
  predicate MapDomainSubtraction<U(==), V>(m: map, s: set) { (m - s) is map }

Type synonyms

  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;
  }