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
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.