SE 504 Spring 2026
HW #4: Proving Lemmas in Dafny
Due: 8pm, Wednesday March 25

Each of the .dfy files listed below is a Dafny module that includes one or more lemmata whose proofs are incomplete or missing altogether. Your task is to complete those proofs. The lemmata whose proofs are complete provide models for what your proofs should look like.

Dafny modules:

• Sum_Through (including Problems SUM.1 and SUM.2(a,b,c))
• PowersOfTwo (including Problems PT.1, PT.2, and PT.3)
• Full_Bin_Tree (including Problems FBT.1 and FBT.2)
• Fibonacci (including Problems FIB.1, FIB.2, and FIB.3)
• Ackermann (including Problem ACK.1)