Technical Report Number
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.
Chen, Wei and Udding, Jan Tijmen, "The Specification Statement Refined" Report Number: WUCS-89-37 (1989). All Computer Science and Engineering Research.