Issue No. 03 - July (1990 vol. 1)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/71.80163
<p>A proof system for a shared dataspace programming notation called Swarm (a programming logic similar in style to that of UNITY) is specified. Relevant aspects of the Swarm language and model are overviewed. To illustrate the proof system, the Swarmlogic is used to verify the correctness of a program for labeling connected equal-intensity regions of a digital image. Like UNITY, the Swarm proof system uses an assertional programming logic which relies upon proof of programwide properties, e.g. global invariants and progress properties. The Swarm logic is defined in terms of the same logical relations as UNITY (unless, ensures, and leads-to), but several of the concepts are reformulated to accommodate Swarm's distinctive features.</p>
Index Termsprogram correctness; UNITY-style programming logic; shared dataspace programs; proof system; Swarm; program verification
G. Roman and H. Cunningham, "A UNITY-Style Programming Logic for Shared Dataspace Programs," in IEEE Transactions on Parallel & Distributed Systems, vol. 1, no. , pp. 365-376, 1990.