A lattice-theoretic framework for circular assume-guarantee reasoning

Abstract

We develop an abstract lattice-theoretic framework within which we study soundness and other properties of circular assume-guarantee (A-G) rules constrained by side conditions. We identify a particular side condition, non-blockingness, which admits an intelligible inductive proof of the soundness of circular A-G reasoning. Besides, conditional circular rules based on non-blockingness turn out to be complete in various senses and stronger than a large class of sound conditional A-G rules. In this respect, our framework enlightens the foundations of circular A-G reasoning. Due to its abstractness, the framework can be instantiated to many concrete settings. We show several known circular A-G rules for compositional verification to be instances of our generic rules. Thus, we do the circularity-breaking inductive argument once to establish soundness of our generic rules, which then implies soundness of all the instances without resorting to technically complicated circularity-breaking arguments for each single rule. In this respect, our framework unifies many approaches to circular A-G reasoning and provides a starting point for the systematic development of new circular A-G rules.

Wir entwickeln einen abstrakten verbandstheoretischen Rahmen in dem wir die Korrektheit und andere Eigenschaften bedingter zirkulaerer Assume-Guarantee- Regeln (A-G-Regeln) untersuchen. Wir isolieren eine besondere Nebenbedingung, non-blockingness, die zu einem verstaendlichen induktiven Beweis der Korrektheit zirkulaerer A-G-Regeln fuehrt. Ausserdem sind durch non-blockingness eingeschr aenkte zirkulaere Regeln vollstaendig und staerker als eine grosse Klasse von korrekten bedingten A-G-Regeln. So gesehen erhellt unsere Arbeit die Grundlagen des zirkulaeren A-G-Paradigmas.Aufgrund seiner Abstraktheit kann unser Rahmen zu vielen konkreten Formalismen instanziiert werden. Wir zeigen, dass mehrere bekannte A-G-Regeln zur kompositionalen Verifikation Instanzen unserer generischen Regeln sind. So ist der zirkularitaetsaufloesende Beweis der Korrektheit nur einmal fuer unsere generische Regeln zu fuehren, dann erben alle Instanzen Korrektheit, ohne dass noch einmal ein zirkularitaets-aufloesender Beweis noetig ist. In dieser Hinsicht stellt unser Rahmen eine einheitliche Plattform dar, die verschiedene Ausformungen des zirkulaeren A-G-Paradigmas umfasst und von der ausgehend systematisch neue zirkulaere A-G-Regeln entwickelt werden koennen.