No abstract available.

The authors have developed a programming logic for Swarm that is similar in style to that of UNITY. They show how the proof logic for Swarm can be extended to accommodate the dynamic formation of synchronic groups specified by the run-time redefinition of the synchrony relation. The basic Swarm notation is reviewed, the notation for the synchrony relation is introduced, and the concept of a synchronic group is discussed. The use of synchronic groups is illustrated by means of a program for labeling regions in an image unbounded on one side. A UNITY-style assertional programming logic for Swarm without the synchrony relation is reviewed, and the logic is generalized to accommodate synchronic groups.>

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

A simple language called Swarm is used as a vehicle for the investigation of the shared dataspace approach to concurrent computation. An important feature of Swarm is its ability to bring a variety of programming paradigms under a single, unified model. In a series of related examples Swarm's capacity to express shared-variable, message-passing, and rule-based computations; to specify synchronous and asynchronous processing modes; and to accommodate highly dynamic program and data structure is explored. Several illustrations make use of a programming construct unique to Swarm, the synchrony relation and explain how this feature can be used to construct dynamically structured, partially synchronous computations. An overview of the Swarm programming notation, an examination of Swarm programming strategies via a series of related example programs, and a discussion of the distinctive features of the shared dataspace model are given. A formal operational model for Swarm is presented.>

A language paradigm called shared dataspace is defined that causes computations to be performed using an anonymous, content-addressable communication medium acted upon by atomic transactions. To probe the essence of this paradigm, a relatively simple shared dataspace language called Swarm is defined. An overview is presented of the Swarm language. A formal operational model for the language is given and some of the programming implications and distinctive features of the model and language are discussed. Swarm programming strategies are examined using a series of related example programs.>

The authors are currently evaluating the use of shared dataspace paradigm as the basis for a novel programming language, called SDL (Shared Dataspace Language), that supports large-scale concurrency. Their goal is to develop the software support needed for the design, analysis, understanding, and testing of programs involving many thousands of concurrent processes running on a highly parallel multiprocessor. The authors provide an overview of the key SDL features, using small examples to illustrate its power and flexibility.>