Exercises in Style (Alpha Specifications)

Issue title: Concurrency Specification and Programming (CS&P'2002), Part 1

Article type: Research Article

Authors: Abraham, Uri | Pinhas, Tamar

Affiliations: Departments of Mathematics and Computer Science, Ben-Gurion University, Be'er-Sheva, Israel

Abstract: We compare two documents: the Alpha Architecture Reference Manual (from Compaq Computer Corporation) and the TLA^+ specification of the Alpha memory model (by Lamport, Sharma, Tuttle, and Yu). We compare the styles, the languages employed, and the fundamental assumptions (that is the basic frameworks of the two texts). We conclude that the TLA^+ specification is not so much a formalization of the Alpha Reference Manual text as it is a translation into a different framework. We believe that a formalization of the Alpha Reference Manual can be useful, and we propose one.

Keywords:

Journal: Fundamenta Informaticae, vol. 54, no. 2-3, pp. 107-135, 2003