Lecture

Verifying Compiler: Spec# Approach

Description

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.

About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.