Document Type

Technical Report

Publication Date

1989-06-01

Filename

WUCS-89-28.pdf

Technical Report Number

WUCS-89-28

Abstract

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.

Comments

Permanent URL: http://dx.doi.org/10.7936/K7B56H10

Share

COinS