The synchronic group: a concurrent programming concept and its proof logic

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