Courses

Level 2

Program Verification with Dafny

Verify real properties of ordinary code, including code you did not write. When Dafny stops, work out which claim it could not prove and supply what is missing. A green check covers only the claims that were written.

This course is for engineers who check code they may not have written, including generated code. Dafny will often stop on a property that is true. Your job is to read why it stopped, decide what it is missing, and supply that. You are not writing clever proofs from scratch. A green check covers only the claims you wrote.

What you will practice

When verification fails, the missing piece is usually one of these.

• Precondition — what can the code assume when it starts?
• Postcondition — what must be true when it finishes?
• Invariant — what stays true on every pass through a loop?
• Assertion or lemma call — which fact has the solver not been shown?
• Frame — which parts of memory is this allowed to change?
• Termination measure — what shrinks to show this must stop?

Units are numbered 1–7 inside this course, followed by the capstone. You do not need to finish Level 1 first, but Level 1 explains the words used here.

0 of 7 units done · 0 of 48 exercises verified · capstone not finished

1. 01Specifying collections

   Describe collections as sequences, sets, maps, and multisets (bags) by what they contain, then use quantifiers with bounds that cover exactly the positions you mean.

   • Same elements, new orderState that reversing an array keeps the same elements, using a multiset rather than a list of indexes.locked
   • Balances are a mapSpecify a deposit on a map of account balances so one key changes and the others do not.locked
   • Dedupe dropped a valueFix a deduplication loop whose specification already describes the right set of values.locked
   • The element is in thereSpecify a search by an existential witness, and by the forall that means “not found.”locked
   • No repeated idDefine pairwise uniqueness with a forall over two indexes.locked
   • Adjacent sortednessExpress sortedness as a bounded quantifier over adjacent indexes.locked
   • The last index was skippedRepair a quantifier whose upper bound leaves the last element unconstrained.locked
   • Exactly one matchSpecify that a key occurs once, using a count over the array rather than a boolean with no meaning.locked

2. 02Ghost state

   Keep extra data that exists only for the proof, such as a snapshot, a running total, or a simple model the real code must match. Ghost data is erased when the program runs.

   • Remember the original arrayKeep a ghost copy of an array so a fill can still talk about what was there.locked
   • Total supply is not a field you printUpdate a ghost total when cash moves, so the sum of the books stays a proof obligation.locked
   • The array and the model disagreeKeep a ghost sequence in agreement with an executable array of balances.locked

3. 03Lemmas and recursive proofs

   Sometimes a property is true and the solver still stops. Name the missing fact and hand it to the solver, using a separately proved helper called a lemma. Find where an already-proved fact belongs, and supply the missing step in a recursive one.

   • Say the slice is the whole arrayAdd the assertions that connect a prefix invariant to a postcondition about the whole array.locked
   • Call the fact you already haveThe recursive case is stuck. The missing step is a call to the lemma you already have.locked
   • The one-element fact is missingThe reverse-of-append ensures does not follow until the same fact is known for the tail. Supply that missing step.locked
   • The two halves are reversed separatelyJoined’s postcondition does not follow from reversing one concatenation. Use the lemma that already relates the two.locked
   • Signing off clears the requestState that approval clears every flag, and use the fact that already says so.locked
   • Insert stays sortedState that insertion stays sorted and keeps the new value, and use the fact that already says so.locked

4. 04Termination

   Proving that a loop or recursion stops needs a measure that shrinks each time. Write it when Dafny cannot guess it, and write it when a human reader should see it.

   • The index walks forwardGive a decreases clause for a recursion that increases its index.locked
   • The loop stops when the flag flipsProve termination of a loop whose guard is a boolean, not a shrinking bound.locked
   • Two counters, one limitProve termination with a lexicographic measure when one argument resets.locked
   • Counting to the limitWork out which fact a termination argument needs from the loop, and where the loop must carry it.locked

5. 05Heap, aliasing, and frames

   Objects are references, so two names can point to one object. Say exactly which objects a method may change, and callers can rely on everything outside that footprint staying the same.

   • An account is an objectSpecify a constructor and a mutating method on a class.locked
   • One object, two namesRead an aliasing counterexample and decide what the proof needs to know about the two references.locked
   • A linked nodeUpdate a linked node without accidentally specifying a change to the head.locked
   • Only two accounts moveDeclare the heap footprint of a transfer.locked
   • A report does not writeMake a method that only reads usable from code that may not modify anything.locked
   • Savings stays putNarrow a caller’s footprint so an unrelated account is known to be unchanged.locked
   • A check that looks at an accountDeclare what memory a predicate looks at, so callers can tell which writes leave its answer alone.locked

6. 06Abstraction and verified modules

   Hide how a data structure is built behind an invariant, so clients can prove things using only its public promises.

   • What the queue isWrite the representation invariant that ties a queue’s array to the sequence it stands for.locked
   • EnqueueSpecify enqueue as “the abstract sequence grows by one value.”locked
   • DequeueSpecify dequeue as returning the first abstract element and dropping it from the model.locked
   • A client that never mentions the arrayDecide what a client can prove from the public contract alone, and make a round trip verify.locked
   • A registryKeep a representation invariant of unique ids and nonnegative balances across open and credit.locked

7. 07Why verification failed

   When verification fails, decide what actually failed: the code, the specification, the invariant, the frame, or a missing fact.

   • A withdrawalDecide why a proof fails before changing anything, then repair what is actually broken.locked
   • Summing up to nDecide what Dafny knows when a loop ends, and what it still needs to be told.locked
   • Another withdrawalDecide whether a failure comes from the code or from the inputs the method promises to handle.locked
   • The total of two sequencesDecide whether a failed claim is false or only unproved, and say what the verifier is missing.locked
   • Summing up to n, againRead which loop obligation fails, and decide when the claim is supposed to be true.locked
   • One more withdrawalDecide whether the written claim is the claim you meant.locked
   • Absolute valueDecide whether a green check on this file says what its name says.locked
   • The total of two sequences, rewrittenTell a true claim Dafny cannot prove from a claim the code does not meet, when the message is the same.locked
   • A total that cannot be negativeRead an error at a call, decide what the callee needs, and decide who should provide it.locked
   • A reviewer said verifiedAudit a transfer whose proof does not establish the transfer.locked

8. CapVerified transaction ledger

   Build and verify a small transaction ledger: unique accounts, no negative balances, transfers that conserve money, and frozen accounts that cannot send.

   • Open an accountMake account creation preserve unique ids and nonnegative balances.locked
   • Deposit and withdrawRepair a withdraw that changes the ledger when it is supposed to fail.locked
   • Transfer preserves the totalFinish a transfer proof so the sum of balances is unchanged, including the framing of every other account.locked
   • Frozen accountsSpecify and implement the rule that a frozen account cannot send or receive.locked
   • Verify the claimTake a transfer that is claimed to be safe and make the proof match the claim.locked