The Specification Statement Refined
Wei Chen · Open Scholarship Institutional Repository (Washington University in St. Louis) · 1989
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.