Dafny

programming-languages

Definition

Dafny

Dafny is a verification-aware programming language that has native support for recording specifications and is equipped with a static program verifier. ¹

Functions vs. Methods

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.

Good Contracts

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.

Termination

Total Correctness

Dafny proves Total Correctness by default. This means that for every method or function, it verifies two things:

1. Partial Correctness: If the program terminates, the post-condition holds.
2. Termination: The program eventually stops (does not loop infinitely or recurse forever).

Decreases Clause

To prove termination, Dafny uses a variant (or rank function). This is an expression that provides a “measure” of the remaining work.

• Requirement: The value of the rank must strictly decrease with every recursive call or loop iteration.
• Bound: The value must be bounded from below (e.g., cannot go below 0 for integers, or empty list for sequences).
• Automatic Inference: Dafny can often guess the termination metric automatically (e.g., x in while x > 0). When it fails, you must provide a decreases clause explicitly.

Termination with Lexicographical Tuples

When a function has multiple parameters that change in complex ways (e.g., one grows while the other shrinks), we use tuples in the decreases clause. Dafny compares these tuples using Lexicographical Order (${<}_{lex}$).

Example (Ackermann-like recursion):

method Ackermann(m: int, n: int) returns (r: int)
    requires m >= 0 && n >= 0
    // Dafny uses the tuple (m, n) to prove termination
    decreases m, n 
{
    if m == 0 {
        r := n + 1;
    } else if n == 0 {
        // m decreases, n increases arbitrarily.
        // (m-1, 1) <_lex (m, n) because m-1 < m.
        r := Ackermann(m - 1, 1);
    } else {
        // Outer call: m decreases. (m-1, ...) <_lex (m, n)
        // Inner call: m stays same, n decreases. (m, n-1) <_lex (m, n)
        var t := Ackermann(m, n - 1);
        r := Ackermann(m - 1, t);
    }
}

Why this works in the decreases m, n tuple:

1. Primary Measure ($m$): If $m$ decreases, the tuple is smaller immediately, regardless of what happens to $n$ (it can grow to infinity).
2. Secondary Measure ($n$): If $m$ stays the same, $n$ must decrease.

todo add examples from the exercises where abs(n) is the decreases function.

Loop Invariant

Dafny reasons about the behaviour of loops solely through their guards and loop invariants. Interestingly this means that Dafny can actually reason about loops without needing a loop implementation.

Loop Invariant

A loop invariant is a condition that must hold true at three critical points in a loop’s execution:

1. Entry: It holds before the loop starts.
2. Maintenance: It holds after every iteration of the loop body.
3. Exit: Consequently, it holds when the loop terminates.

Loop Opacity

Dafny treats loops as opaque (similar to methods). When verifying the code that follows a loop, Dafny forgets everything about the state of the variables modified by the loop, except for what is explicitly preserved by the invariant.

To reason about the state after a loop, Dafny uses only two pieces of information:

4. The Loop Invariant is true.
5. The Loop Guard is false (negated).

Implication: You can verify a program containing a loop without writing the loop’s body, as long as you provide a valid invariant and a decreases clause. Conversely, if you write a perfect loop body but omit the invariant, Dafny will fail to prove properties about the result because it “doesn’t know” what the loop did.

Logic of Verification

To verify a loop while (G) invariant I { Body }, Dafny checks three conditions:

1. Initialisation:

$$\text{Preconditions}⟹I$$

The invariant must be true when the loop is first reached.

2. Preservation:

$$I\wedge G⟹WP(\text{Body},I)$$

If the invariant and guard are true, executing the body must result in a state where the invariant is still true.

3. Termination:

$$I\wedge \neg G⟹\text{Postconditions}$$

When the loop finishes, guard is false, the combination of the invariant and the negated guard must imply the rest of the program’s requirements.

Example: To prove that a loop calculates x = 10, the invariant must track the progress of x.

• Variable: x starts at 0.
• Guard: x < 10.
• Update: x := x + 1.
• Correct Invariant: 0 ⇐ x ⇐ 10

Why:

• Start: 0 is between 0 and 10. (Valid)
• Step: If x < 10, then x + 1 is at most 10. (Valid)
• End: x is not < 10 (so x >= 10) AND 0 <= x <= 10.
• Conclusion: x must be exactly 10.

Partial vs. Total Correctness

Here is the Partial vs. Total Correctness section, formatted to match your style.

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$

• Key: It does not guarantee that the program stops. An infinite loop satisfies any partial correctness specification (vacuously true because it never reaches the final state).

Total Correctness

A program $C$ is totally correct if:

1. It is partially correct.

2. It 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's Approach

As noted in the Termination section, Dafny verifies Total Correctness by default. To verify a method that may not terminate (i.e., to check only partial correctness), you must explicitly allow non-termination using the syntax decreases *.

Examples: Partial vs. Total Correctness

Partial Correctness (Valid): Consider the triple $\{x>0\}x:=x+1\{x>1\}$.

• Partial Correctness: Valid. If $x$ starts at 1, it becomes 2. Since 2 > 1, the postcondition holds.
• Total Correctness: Valid. The assignment x := x + 1 always terminates.

Infinite Loop (Partial vs. Total): Consider the triple $\{true\}\text{while}(true)\{\}\{false\}$.

• Partial Correctness: Valid.
  • The program enters an infinite loop and never terminates.
  • The condition “if it terminates, then $false$ is true” is vacuously true because the “if” part never happens.
• Total Correctness: Invalid.
  • The program fails the termination requirement.

The “False” Precondition: Consider the triple $\{false\}x:=10\{x=5\}$.

• Partial Correctness: Valid (Vacuously).
  • Precondition is false (impossible state).
  • Logical implication $false⟹Q$ is always true.
• Total Correctness: Valid (Vacuously).
  • Since no state satisfies the precondition, the set of states we need to check for termination is empty.

Assignment Validity: Consider $\{true\}x:=10\{x=10\}$.

• Partial Correctness: Valid.
  • Weakest Precondition: $WP(x:=10,x=10)\equiv 10=10\equiv true$.
  • $true⟹true$.
• Total Correctness: Valid. Simple assignment terminates.

Footnotes

1. Dafny ↩