Verifying Compiler: Spec# Approach

This lecture by the instructor presents the Spec# programming system, focusing on a verifying compiler for sequential C# 2.0. It covers method contracts, invariants, and type annotations, using weakest preconditions for verification. The lecture demonstrates the power of non-null types, moving runtime errors to compile time, and introducing new language changes for reference types. It also discusses comparing against null, non-null instance fields, and solutions for handling non-null issues. Additionally, it explores the limitations of pre- and postconditions, re-entrance with callbacks, and the concept of allowing certain invariants to be broken. The lecture concludes with a discussion on exposing invariants through special block statements.