Formal Methods in System Design. 23(2):115–142, SEPTEMBER 2003

Issn Print: 0925-9856

Publication Date: September 2003

# A Mechanized Proof Environment for the Convenient Computations Proof Method*

Marcelo Glusman;Shmuel Katz;

+ Author Information

Department of Computer Science, The Technion, Haifa, Israel

### Abstract

A mechanized verification environment made up of theories over the deductive mechanized theorem prover PVS is presented, which allows taking advantage of the “convenient computations” method. This method reduces the conceptual difficulty of proving a given property for all the possible computations of a system by separating two different concerns: (1) proving that special convenient computations satisfy the property, and (2) proving that every computation is related to a convenient one by a relation which preserves the property. The approach is especially appropriate for applications in which the first concern is trivial once the second has been shown, e.g., where the specification itself is that every computation reduces to a convenient one. Two examples are the serializability of transactions in distributed databases, and sequential consistency of distributed shared memories. To reduce the repetition of effort, a clear separation is made between “infrastructural” theories to be supplied as a proof environment PVS library to users, and the specification and proof of particular examples. The provided infrastructure formally defines the method in its most general way. It also defines a computation model and a reduction relation—the equivalence of computations that differ only in the order of finitely many independent operations. One way to prove that this relation holds between every computation and some convenient one involves the definition of a measure function from computations into a well-founded set. Two possible default measures, which can be applied in many cases, are also defined in the infrastructure, along with useful lemmas that assist in their usage. We show how the proof environment can be used, by a step-by-step explanation of an application example.