Formal Derivation of Rule-Based Program

Authors

Gruia-Catalin Roman, Washington University in St Louis
Rose F. Gamble, Washington University in St Louis
William E. Ball, Washington University in St Louis

Document Type

Technical Report

Publication Date

1991-12-01

Filename

WUCS-91-17.pdf

Technical Report Number

WUCS-91-17

Abstract

This paper describes a formal approach to developing concurrent rule-based programs. Our program derivation strategy starts with a formal specification of the problem. Specification refinement is used to generate an initial version of the program. Program refinement is then applied to produce a highly concurrent and efficient version of the same program. Techniques for the deriving concurrent programs through either specification or program refinement have been described in previous literature. The main contribution of this paper consists of extending the applicability of these techniques to a broad class of rule-based programs. The derivation process is supported by a powerful proof logic, a logic that recently has been extended to cover rule-based programs. The presentation centers around a rigorous and systematic derivation of a concurrent rule-based solution to a classic problem.

Comments

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

Recommended Citation

Roman, Gruia-Catalin; Gamble, Rose F.; and Ball, William E., "Formal Derivation of Rule-Based Program" Report Number: WUCS-91-17 (1991). All Computer Science and Engineering Research.
https://openscholarship.wustl.edu/cse_research/636