These lecture notes present Dafny, an automated program verication system that is based on the concept of dynamic frames and is capable of producing .NET executables. These notes overview the basic design, Dafny's history, and summarizes the environment conguration. The key language constructs, and various system limits, are illustrated through the development of a simple Dafny program. Further examples, linked to online demonstrations, illustrate Dafny's approach to loop in-variants, termination, data abstraction, and heap-related specications.
Main Research Area:
8th LASER Summer School on Software Engineering, 2012