SNAP: A Validator / Annotator for Proofs of Distributed Programs

Mr. Ramesh Bharadwaj

Mr. Frank A. Stomp

Software Engineering Research Group
CRL, McMaster University,
Hamilton, Ontario, Canada L8S 4K1


Abstract

Distributed programs are notorious for subtle errors. requiring proofs to establish their correctness. Correctness proofs carried out on paper tend to be error-prone. This paper presents system SNAP (Simple Notion of Annotating Proofs) being developed to validate correctness proofs in Linear Time Temporal Logic (LTL). SNAP supports forward proofs and can be used either interactively or batch mode. The system validates proofs entered by users - in a representation close to handwritten proofs - by providing justifications for every proof step. Justifications are in essence theorems or meta rules in the system's rule- base; together with the proof, they constitute a proof annotation. Theorems proved elsewhere may be loaded into the system's rule-base without having to redo proofs, a mechanism to raise the abstraction level of proofs. SNAP supports proofs of theorems and certain meta rules, all of which may be dynamically added to its rule-base. Since the design goal of SNAP is to validate and annotate correctness proofs of programs, we have sacrificed generality for efficiency and ease of use. For example, the system does not support higher-order logics.

To demonstrate the use of SNAP, we discuss how the proof of a safety property for Dekker's algorithm (an algorithm for mutual exclusion) has been validated by the system.