A Development Calculus for Specifications
Logic in Computer Science
2007-05-23 v2 Programming Languages
Abstract
A first order inference system, called R-calculus, is defined to develop the specifications. It is used to eliminate the laws which is not consistent with the user's requirements. The R-calculus consists of the structural rules, an axiom, a cut rule, and the rules for logical connectives. Some examples are given to demonstrate the usage of the R-calculus. The properties about reachability and completeness of the R-calculus are formally defined and are proved.
Cite
@article{arxiv.cs/0303021,
title = {A Development Calculus for Specifications},
author = {Wei Li},
journal= {arXiv preprint arXiv:cs/0303021},
year = {2007}
}
Comments
14 pages with some minor errors in the original version corrected