Dafny

programming-languages

Definition

Dafny

Dafny is an object-oriented and functional programming language designed for formal verification. It enables developers to write code alongside its specification (preconditions, postconditions, invariants), which the compiler then proves correct using an automated theorem prover. ¹

Verification Semantics

Partial vs. Total Correctness

Partial Correctness

A program $C$ is partially correct with respect to a precondition $P$ and post-condition $Q$ if whenever execution starts in a state satisfying $P$ and terminates, the final state satisfies $Q$.

$${\models }_{par}\{P\}C\{Q\}⟺\forall s,s^{\prime }.(s\models P\wedge (C,s)\to s^{\prime })⟹s^{\prime }\models Q$$

Total Correctness

A program $C$ is totally correct if it is partially correct and terminates for all inputs satisfying $P$.

$${\models }_{tot}\{P\}C\{Q\}⟺{\models }_{par}\{P\}C\{Q\}\wedge (\forall s.s\models P⟹C\text{ terminates on }s)$$

Dafny proves Total Correctness by default.

Examples:

• Valid/Valid: $\{x>0\}x:=x+1\{x>1\}$
  (Terminates and holds).
• Valid/Invalid: $\{true\}\text{while}(true)\{\}\{false\}$
  (Infinite loop implies partial correctness vacuously, but fails total correctness).
• Valid/Valid: $\{false\}x:=10\{x=5\}$
  (Vacuously true for both as precondition is impossible).

Opacity

Opacity: Functions vs. Methods

Would the verification behaviour change if a method is changed to a function?

Answer: Yes.

• Methods are opaque, meaning the callers takes only explicitly defined contracts into account.
• Functions, on the other hand, are transparent to the caller. The caller takes the actual implementation of the function into account.

Proving: Functions vs. Methods

Can it be the case that Dafny proves a program correct using a method contract, but does not when using a function with the same implementation as the method?

Answer: Yes. Dafny’s function provider might fail for more complex functions due to timeouts. Methods are faster to check since they only rely on the explicitly specified contract.

Termination

To prove total correctness, Dafny must verify that every loop and recursive call terminates. It does this using a variant (or rank function).

Decreases Clause

The decreases clause specifies the rank function. Dafny checks two properties:

1. Strict Decrease: The rank must be strictly smaller in the recursive call or next iteration.
2. Bounded: The rank must be bounded from below (cannot decrease forever).

Valid Ranks

Dafny supports various types for the decreases clause:

• Integers: Must decrease and be bounded by $0$.
• Sequences/Sets: The size (cardinality) must decrease.
• Tuples: Compared lexicographically.

If no clause is provided, Dafny attempts to guess one (e.g., x if x < N is the guard).

Lexicographical Ordering

For multiple parameters, use tuples. Dafny compares these using lexicographical order (${<}_{lex}$).

Tuple Decrease Logic

For a tuple $(m,n)$:

1. Primary Measure ($m$): If $m$ decreases, the tuple is smaller immediately.
2. Secondary Measure ($n$): If $m$ stays the same, $n$ must decrease.

Example (Ackermann-like):

method Ackermann(m: int, n: int) returns (r: int)
    requires m >= 0 && n >= 0
    decreases m, n // Uses tuple (m, n)
{
    if m == 0 {
        r := n + 1;
    } else if n == 0 {
        r := Ackermann(m - 1, 1); // m decreases
    } else {
        var t := Ackermann(m, n - 1); // n decreases, m same
        r := Ackermann(m - 1, t);     // m decreases
    }
}

Examples:

1. Simple Upper Bound
The function F increases x until it hits 10. The distance to 10 (10 - x) decreases with every step.

function F(x: int): int
decreases 10 - x
{
   if x > 10 then 0
   else 2*F(x+1)
}

2. Relative Difference
The function G decreases the gap between x and y (x - y) until x <= y.

function G(x: int, y: int): int
decreases x - y
{
   if x <= y then 0
   else 1+G(x-1, y)
}

3. Magnitude Sum
The function H terminates when x and y have the same sign. The sum of absolute values decreases because the variables move towards zero or flip signs in a way that reduces total magnitude.

function H(x: int, y: int): int
decreases Abs(x) + Abs(y)
{
   if x * y >= 0 then
      0
   else if y < 0 then
      H(x-1, y+2)
   else
      H(y-1, x+2) // Note: the arguments are swapped here
}

Loops

Dafny reasons about loops solely through guards and loop invariants.

Loop Opacity

Dafny treats loops as opaque. To reason about the state after a loop, Dafny uses only:

1. The Loop Invariant is true.
2. The Loop Guard is false.

Thus, the effective postcondition of the loop is:
$I\wedge \neg G$

Verification Logic

To verify while (G) invariant I { Body }, three conditions must hold:

1. Initialisation ($\text{Pre}⟹I$)
   The invariant holds before the loop starts.

2. Preservation ($I\wedge G⟹WP(\text{Body},I)$)
   If the invariant and guard hold, executing the body preserves the invariant.

3. Termination ($I\wedge \neg G⟹\text{Post}$)
   When the loop finishes (guard false), the invariant implies the post-condition.

Example:
To prove $x$ reaches $10$:

• Guard: $x<10$
• Update: $x:=x+1$
• Invariant: $0\le x\le 10$

Specification

Strong Contracts?

Should you always aim to make your post-conditions as strong as possible?

Answer: No, Strong post-conditions lead to over-specification and loss of abstraction. Modifying code becomes increasingly difficult.

Design Principles

Designing contracts involves a trade-off between the client (caller) and the supplier (method):

Strong vs. Weak Preconditions:

• Weak Precondition:
  • Pros: Easier for the Client to use (fewer restrictions).
  • Cons: Harder for the Method to implement (must handle more cases, e.g., nulls, negatives).
• Strong Precondition:
  • Pros: Easier for the Method (can assume valid data).
  • Cons: Harder for the Client (must ensure data is valid before calling).

Runtime Checking

While Dafny verifies contracts statically (at compile time), standard languages (Java, Python) check contracts at runtime using:

1. Error Output: Printing error messages (weakest).
2. Exceptions: Throwing IllegalArgumentException (standard).
3. Assertions: Using assert statements (often disabled in production).

Class

Dafny supports object-oriented programming with classes. Unlike datatypes, classes are reference types and contain mutable state.

Class Invariant

A class invariant is a condition that defines the valid state of an object. It is typically defined as a ghost predicate.

Invariant Maintenance

Dafny does not automatically enforce class invariants. You must explicitly:

1. Establish the invariant in the constructor (ensures Valid()).
2. Require it in methods (requires Valid()).
3. Preserve it in methods (ensures Valid()).

Example (Ledger):

class Ledger {
    var total_credit: nat
    var total_debit: nat
 
    // Class Invariant
    ghost predicate Balanced()
    reads this
    {
        this.total_credit == this.total_debit
    }
 
    constructor()
    ensures Balanced() // establish invariant
    {
      this.total_credit := 0;
      this.total_debit := 0;
    }
 
    method RecordTransactions(newDebit: array<nat>, newCredit: array<nat>)
    modifies this
    requires Balanced() // require valid state
    ensures Balanced()  // preserve valid state
    requires Sum(newDebit) == Sum(newCredit)
    {
        this.total_debit := this.total_debit + Sum(newDebit);
        this.total_credit := this.total_credit + Sum(newCredit);
    }
}
 
function Sum(a: array<nat>): int
reads a { SumFrom(a,0) }
 
function SumFrom(a: array<nat>, pos: nat): nat
decreases a.Length - pos
reads a
{
    if pos >= a.Length then 0 else a[pos] + SumFrom(a, pos+1)
}

Ghost Code

The ghost keyword marks code that is used only for verification. It is erased by the compiler and does not exist at runtime.

• Usage: Specification functions, logical variables, proofs.
• Restriction: Ghost code cannot affect non-ghost (compiled) state.

Subtyping

Classes in Dafny follow strict behavioural subtyping (Design by Contract). When a subclass overrides a method, it must satisfy the Liskov Substitution Principle:

1. Preconditions are contravariant: Sub-classes can require less (weaken), but not more.
2. Postconditions are covariant: Sub-classes can promise more (strengthen), but not less.

Base Trait:

trait Course {
    var ECTS: nat
 
    // The Contract (The Baseline)
    method Complete(effort: int) returns (grade: int)
    modifies this
    requires effort >= 25 * ECTS
    ensures 1 <= grade <= 5
}

1. RegularCourse (Valid)

• Pre: Weakened ($20<25$) $⟹$ Valid.
• Post: Strengthened ($0<grade\le 3\subset \mathrm{1..5}$) $⟹$ Valid.

class RegularCourse extends Course {
    method Complete(effort: int) returns (grade: int)
    modifies this
    requires effort >= 20 * ECTS
    ensures 0 < grade <= 3
    { return 2; }
}

2. HardCourse (Invalid)

• Pre: Strengthened ($50>25$) $⟹$ Error. Subclass demands more effort than parent.

class HardCourse extends Course {
    method Complete(effort: int) returns (grade: int)
    modifies this
    requires effort >= 50 * ECTS // ERROR
    ensures 2 <= grade <= 4
    { return 3; }
}

3. EasyCourse (Invalid)

• Pre: Strengthened (Range restricted to $\le 10$) $⟹$ Error. Rejects valid inputs ($\mathrm{11..24}$).

class EasyCourse extends Course {
    method Complete(effort: int) returns (grade: int)
    modifies this
    requires effort <= 10 * ECTS // ERROR
    ensures grade == 1
    { return 1; }
}

4. ImpossibleCourse (Valid)

• Pre: Weakened (True) $⟹$ Valid. Accepts any effort.
• Post: Strengthened (Exactly 5) $⟹$ Valid.

class ImpossibleCourse extends Course {
    method Complete(effort: int) returns (grade: int)
    modifies this
    // Implicit 'requires true'
    ensures grade == 5
    { return 5; }
}

5. NeverEndingCourse (Valid)

• Pre: Weakened (True) $⟹$ Valid.
• Post: Strengthened (False) $⟹$ Valid. The empty set is a subset of $\mathrm{1..5}$.

class NeverEndingCourse extends Course {
    method Complete(effort: int) returns (grade: int)
    modifies this
    ensures false
    {
        while true {} // Divergence satisfies 'ensures false'
    }
}

6. GermanCourse (Invalid)

• Post: Weakened ($\mathrm{1..6}⊈\mathrm{1..5}$) $⟹$ Error. Promises less than parent (might return 6).

class GermanCourse extends Course {
    method Complete(effort: int) returns (grade: int)
    modifies this
    requires effort >= 25 * ECTS
    ensures 1 <= grade <= 6 // ERROR
    { return 6; }
}

7. NonExistentCourse (Invalid)

• Pre: Strengthened (False) $⟹$ Error. Accepts nothing, violating parent contract.

class NonExistentCourse extends Course {
    method Complete(effort: int) returns (grade: int)
    modifies this
    requires false // ERROR
    { return 1; }
}

Footnotes

1. Dafny ↩