Compilateur de vérification: Approche Spec#

Cette séance de cours de l'instructeur présente le système de programmation Spec#, en mettant l'accent sur un compilateur de vérification pour C# 2.0 séquentielle. Il couvre les contrats de méthode, les invariants et les annotations de type, en utilisant les conditions préalables les plus faibles pour la vérification. La séance de cours démontre la puissance des types non null, déplace les erreurs d'exécution pour compiler le temps, et introduit de nouveaux changements de langage pour les types de référence. Il examine également la comparaison avec les champs d'instances nulles, non nulles et les solutions pour traiter les questions non nulles. En outre, il explore les limites des conditions pré- et post-, la réentrée avec les rappels, et le concept de permettre à certains invariants d'être brisés. La séance de cours se termine par une discussion sur l'exposition des invariants à travers des déclarations de blocs spéciales.