Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs

  • Rustan Leino ,
  • Peter Müller

Advanced Lectures on Software Engineering |

Published by Springer Berlin Heidelberg

Publication

Spec# is a programming system for the development of correct programs. It consists of a programming language, a verification methodology, and tools. The Spec# language extends C# with contracts, which allow programmers to document their design decisions in the code. The verification methodology provides rules and guidelines for how to use the Spec# features to express and check properties of interesting implementations. Finally, the tool support consists of a compiler that emits run-time checks for many contracts and a static program verifier that attempts to prove automatically that an implementation satisfies its specification. These lecture notes teach the use of the Spec# system, focusing on specification and static verification.