Formalising LPOs and Invariants in Coq
Henri Korver, Alex Sellink · 1995
In the setting of ¯CRL, the notions of `linear process operator (LPO)' and `invariant' are implemented in Coq, which is a a proof development tool based on type theory. As a first experiment we have computer-checked a general property of a binary search program in the new framework. 1 Introduction Bezem and Groote [5] incorporated several well-known and field-proven concepts such as precondition/effect notation and invariants in the framework of ¯CRL, aiming at a powerful verification methodology for distributed systems. Roughly, ¯CRL [9] can be considered as a dialect of ACP [2] extended with a formal treatment of data. The precondition/effect notation, as found in Unity [6] and I/O automata theory [15], is obtained in ¯CRL by restricting process expressions to a linear format; such expressions are called linear process operators (LPOs). Invariants are formulated in ¯CRL as predicates over linear operators. In this paper, we formalise the ¯CRL versions of the notions LPO and invarian...