Technical Report Number
Rule-based programs used in mission- and safety-critical applications need to be shown to be free of hazards. This paper discusses formal proof-techniques which promise to assist designers in this task. In this paper we show that the shared dataspace language Swarm has many key features in common with rule-based languages. We outline an assertional programming logic for Swarm programs and use the logic to reason about the correctness of a simple program. This logic is a suitable foundation for the development of techniques specific to present and future rule-based languages.
Cunningham, H. Conrad and Roman, Gruia-Catalin, "Toward Formal Verification of Rule-Based Systems: A Shared Dataspace Perspective" Report Number: WUCS-89-28 (1989). All Computer Science and Engineering Research.