This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A UNITY-Style Programming Logic for Shared Dataspace Programs
July 1990 (vol. 1 no. 3)
pp. 365-376

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.

[1] S. Ahuja, N. Carriero, and D. Gelernter, "Linda and friends,"IEEE Computer, vol. 19, no. 8, pp. 26-34, Aug. 1986.
[2] R. J. R. Back and R. Kurki-Suonio, "Distributed cooperation with Action Systems,"ACM Trans. Programming Languages Syst., vol. 10, no. 4, pp. 513-554, Oct. 1988.
[3] L. Brownston et al.,Programming Expert Systems in OPS5, An Introduction to Rule-Based Programming, Addison Wesley, Reading, Mass., 1985, Chapter 4, pp. 161- 164.
[4] N. Carriero and D. Gelernter, "Linda in context,"Commun. ACM, vol. 32, pp. 444-458, Apr. 1989.
[5] K. M. Chandy and J. Misra,Parallel Program Design: A Foundation. Reading, MA: Addison-Wesley, 1988.
[6] E. Chang and R. Roberts, "An improved algorithm for decentralized extrema-finding in circular configurations of processes,"Commun. ACM, vol. 22, no. 5, pp. 281-283, 1979.
[7] H. C. Cunningham, "The shared dataspace approach to concurrent computation: The Swarm programming model, notation, and logic," Ph.D. dissertation, Washington Univ., Dep. of Comput. Sci., St. Louis, MO, Aug. 1989.
[8] H. C. Cunningham and G.-C. Roman, "Toward formal verification of rule-based systems: A shared dataspace perspective," Tech. Rep. WUCS-89-28, Washington Univ., Dep. of Comput. Sci., St. Louis, MO, June 1989.
[9] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976.
[10] N. Francez,Fairness. New York: Springer-Verlag, 1986.
[11] C. A. R. Hoare, "Communicating sequential processes,"Commun. ACM, vol. 21, pp. 666-677, 1978.
[12] S. S. Lam and A. U. Shankar, "A relational notation for state transition systems," invited talk at the Eighth Int. Symp. Protocol Specification, Testing and Implementation, Atlantic City, NJ, June 1988; available as Tech. Rep. TR- 88-21, Dep. Comput. Sci., Univ. Texas at Austin, May 1988.
[13] G. LeLann, "Distributed systems, towards a formal approach," inInformation Processing 77. New York: North-Holland, 1977, pp. 155-160.
[14] J. Misra, "Soundness of the subsitution axiom," Notes on UNITY 14- 90, Dep. Comput. Sci., Univ. of Texas at Austin, Austin, TX, Mar. 1990.
[15] M. Rem, "Associons: A program notation with tuples instead of variables,"ACM Trans. Programming Languages Syst., vol. 3, no. 3, pp. 251-262, July 1981.
[16] M. Rem, "The closure statement: A programming language construct allowing ultraconcurrent execution,"J. ACM, vol. 28, no. 2, pp. 393-410, Apr. 1981.
[17] G.-C. Roman, "Language and visualization support for large-scale concurrency," inProc. 10th Int. Conf. Software Eng., IEEE, Apr. 1988, pp. 296-308.
[18] G.-C. Roman and K. C. Cox, "A declarative approach to visualizing concurrent computations,"IEEE Comput. Mag., vol. 22, no. 10, pp. 25-36, Oct. 1989.
[19] G.-C. Roman and K. C. Cox, "Declarative visualization in the shared dataspace paradigm," inProc. 11th Int. Conf. Software Eng., IEEE, May 1989, pp. 34-43.
[20] G.-C. Roman and H. C. Cunningham, "A shared dataspace model of concurrency--Language and programming implications," inProc. 9th Int. Conf. Distributed Comput. Syst., IEEE, June 1989, pp. 270-279.
[21] G.-C. Roman and H. C. Cunningham, "Mixed programming metaphors in a shared dataspace model of concurrency," Tech. Rep. WUCS-90-1, Washington Univ., Dep. Comput. Sci., St. Louis, MO, Feb. 1990;IEEE Trans. Software Eng., to be published.
[22] P. Saint-Marc and G. Medioni, "B-spline contour representation and symmetry detection," inProc. Euro. Conf. Comput. Vision(Antibes, France), 1990, pp. 604-606.
[23] L. Sterling and E. Shapiro,The Art of Prolog. Cambridge, MA: MIT Press, 1986.

Index Terms:
Index Termsprogram correctness; UNITY-style programming logic; shared dataspace programs; proof system; Swarm; program verification
Citation:
H.C. Cunningham, G.C. Roman, "A UNITY-Style Programming Logic for Shared Dataspace Programs," IEEE Transactions on Parallel and Distributed Systems, vol. 1, no. 3, pp. 365-376, July 1990, doi:10.1109/71.80163
Usage of this product signifies your acceptance of the Terms of Use.