Introduction to Dafny

Weakest Precondition Definition

• wp(S, Q) is the weakest precondition.
• {wp(S, Q)} S {Q} holds.
• Valid if P → wp(S, Q).
• Enables backward reasoning.

wp for Assignment

• wp(x, y := E, F, P) = P[x, y := E, F].
• Same as assignment rule precondition.
• Substitutes E for x and F for y.

wp for Composition

• wp(S₁; S₂; …; Sₙ, Q) = wp(S₁, wp(S₂, …, wp(Sₙ, Q))).
• Computes weakest precondition working backwards.

wp for Conditional

• wp(if G {S} {T}, Q) = (G → wp(S, Q)) ∧ (¬G → wp(T, Q)).
• Determines branch's weakest precondition.

wp for While Loop

• Given invariant P and variant v:
• P ∧ B → wp(S, P)
• P ∧ B ∧ v=V → wp(S, v < V)
• P ∧ B → v ≥ 0
• P ∧ ¬B → Q
• Then P → wp(while B {S}, Q).

Consequence Rule in wp

• Not required; wp computes weakest precondition.
• If P → wp(S, Q) then {P} S {Q} holds.

Dafny Language Overview

• Object-oriented language.
• Java-like syntax based on Hoare logic and weakest precondition.
• Used for formal verification.

Dafny Method Specification

• Example: method inc(x: int) returns (y: int)
• requires x > 2
• ensures y > 3.
• Specifies preconditions and postconditions.

Dafny Array Types

• array: non-null integer arrays.
• array?: nullable arrays.
• Forall quantifier:
• forall i: int :: 0

Dafny Quantifier Scope

• Bound variable names are local to quantifier.
• Example:
• forall x: int :: 0

Dafny Modifies Clause

• modifies thisa, thisb: indicates modifiable fields.
• Essential for object state change reasoning.

Dafny Old Quantifier

• ensures this.a == old(this.b) && this.b == old(this.a).
• old(expr): value before method execution.

Dafny Loop Invariant

• Invariants hold before, during, and after loop.
• Example:
• invariant r >= 0 && y > 0.
• invariant x == r + y \* q.

Dafny Decrease Clause

• specifies loop variant.
• Expression must decrease on each iteration, bounded below.

Dafny Quotient-Remainder Example

• Example: method quotient_remainder(x: int, y: int) returns (r: int, q: int).
• requires x >= 0 && y > 0.
• Implements division algorithm with loop.

Dijkstra on Programming

• Edsger Dijkstra quote:
• "If debugging is the process of removing software bugs, then programming must be the process of putting them in."
• Emphasizes formal methods.

Rustan Leino's Work

• Principal designer of Dafny at Microsoft Research.
• Focused on provably correct software and formal verification.

Dafny Playground

• Online environment for experimenting with Dafny code.