The Specification Statement Refined

Authors

Wei Chen, Washington University in St. Louis
Jan Tijmen Udding, Washington University in St. Louis

Document Type

Technical Report

Publication Date

1989-09-27

Filename

WUCS-89-37.pdf

Technical Report Number

WUCS-89-37

Abstract

In this paper, we present a rigorous treatment of so-called logical constants, which are used to relate the values of program variables between the precondition and the postcondition of a program. In order to do so, we generalize the latest proof rule for procedures and give a new definition for the specification statement. We show that the specification statement with this definition is the greatest lower bound of all its implementations under the usual refinement ordering and that it is A-distributive. We also demonstrate that a previous treatment of logical constants in specification statements does not have these properties.

Comments

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

Recommended Citation

Chen, Wei and Udding, Jan Tijmen, "The Specification Statement Refined" Report Number: WUCS-89-37 (1989). All Computer Science and Engineering Research.
https://openscholarship.wustl.edu/cse_research/749