Konditionale Kontextuelle Verfeinerung

Viel Arbeit in der formalen Verifikation von Low-Level-Systemen basiert auf einem von zwei Ansätzen: Verfeinerung oder Trennlogik. Diese beiden Ansätze bieten komplementäre Vorteile: Die Verfeinerung unterstützt die Verwendung von Programmen als Spezifikationen sowie die transitive Komposition von Beweisen, während die Trennlogik bedingte Spezifikationen unterstützt und modulares Eigentum über gemeinsam genutzten Zustand ermöglicht. Eine Reihe von Verifikationsrahmen nutzt diese Techniken in Kombination, aber in all diesen Fällen bleiben die Vorteile der beiden Techniken getrennt. Zum Beispiel unterstützt in Rahmen, die relationale Trennlogik verwenden, um kontextuelle Verfeinerung zu beweisen, das Urteil der relationalen Trennlogik nicht die transitive Komposition von Beweisen, während das Urteil zur kontextuellen Verfeinerung keine bedingten Spezifikationen unterstützt. In diesem Papier schlagen wir die Konditionale Kontextuelle Verfeinerung (kurz CCR) vor, das erste Verifikationssystem, das nicht nur Verfeinerung und Trennlogik in einem einzigen Rahmen kombiniert, sondern sie auch wahrhaftig zu einem einheitlichen Mechanismus verbindet, der gleichzeitig alle Vorteile der Verfeinerung und der Trennlogik genießt. Insbesondere sind, anders als in früheren Arbeiten, die Verfeinerungsspezifikationen von CCR sowohl bedingt (mit Trennlogik-Vor- und -Nachbedingungen) als auch transitiv kompositionierbar. Wir implementieren CCR in Coq und bewerten seine Effektivität an einer Reihe interessanter Beispiele.