Document Type
Technical Report
Publication Date
1990-01-03
DOI:
10.7936/K74M92V4
Technical Report Number
WUCS-90-02
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 of extensive program verification research. This paper specifies a proof system for a shared dataspace programming notation called Swarm-- a program logic similar in style to that of UNITY. The paper then uses the logic to reason about a solution to the problem of labeling the connected equal-intensity regions of a digital image.
Recommended Citation
Cunningham, H. Conrad and Roman, Gruia-Catalin, "Unity-Style Proofs for Shared Dataspace Programs Using Dynamic Statements" Report Number: WUCS-90-02 (1990). All Computer Science and Engineering Research.
https://openscholarship.wustl.edu/cse_research/677
Comments
Permanent URL: http://dx.doi.org/10.7936/K74M92V4