Meet Dafny

Bugs often hide because nobody asked “what must always be true?” Dafny checks the answer to that question.

You write the claim: what must be true when a function starts, and what must be true when it finishes. Dafny then turns the function's code and that claim into logical formulas and asks an automated solver to prove them. Dafny does not run your code on sample inputs. It proves the claim for every input it allows.

The next five units do this for one function at a time. The code may already be wrong, or may be code you did not write, such as generated code. You decide what it must do.

Dafny is a programming language where you write claims next to the code. Together the claims are called a contract. A method is Dafny's word for a routine, like a function in C# or Java.

A contract has two kinds of line. requires is what the caller must give you. It is assumed on the way in. ensures is what you promise back. It must be true on the way out.

To check the claim, Dafny hands the code and the contract to a solver called Z3. A solver is a program that searches for a proof. Green means it found one. Red means it did not, and it usually shows a counterexample: real values that break the claim.

The method on the right is short. Here it is one line at a time.

method Double(x: int) returns (y: int) takes a whole number x and gives back a whole number y.

ensures y == 2 * x is the claim: the result is always twice the input. == means “is equal to”. The claim sits between the signature and the {.

y := 2 * x; is the code. := means “store this value in y”.

The claim says what must be true. The code is how it gets there. Dafny's job is to check that the code keeps the promise.

Hit Verify. If the code keeps the claim for every input, you get a green result.

Suppose someone changed the code to y := 2 * x + 1;. The claim is the same, but the code no longer keeps it. Dafny would fail and show a counterexample such as x = 0, where the code returns 1 but the claim needs 0. You debug that input like a failing test, then verify again.

A green result covers only the claims that were written. If the only line were ensures true, it would pass for any code, because that claim says nothing. Dafny's own output also warns that a counterexample may be inconsistent or invalid, so check it against the claim before you trust it.

Usually one or two claim lines. The code is often already there.

Claim lines sit between the signature and the {. They are not statements inside the body.

Inside a claim, == means “is equal to”. In the code, := stores a value. They are different symbols.

You learn keywords as you need them. This is not a language lecture. You do not need TLA+ or Lean yet. Later units ask the same question about a design, and about a step a solver could not finish.

The method on the right already verifies. Hit Verify (or ⌘↩ / Ctrl+Enter). The green check is the whole exercise. A real Dafny run is the grader, so the first time you meet it, you are not solving a syntax puzzle.

Then start unit 1. There, you will write an ensures yourself.