A UNITY-Style Programming Logic for a Shared Dataspace Language

Abstract

The term shared dataspace refers to the general class of programming languages in which the principal means of communication among the concurrent components of programs is a common, content-addressable data structure called a dataspace. In the programming language and artificial intelligence communities, there is considerable interest in such languages, e.g., logic-based languages, production rule systems, and the Linda language. However, these languages have not been the subject extensive program verification research. This paper specifies a proof system for the shared dataspace language Swarm - a proof system similar in style to that of UNITY. The paper then uses the proof system to reason about two different solutions to the problem of labelling the connection equal-intensity regions of the digital image.