10.1 Function Refinement

Refinement of functions specified at the top-level works by the same mechanism as specification inheritance (see section 7.9 Inheritance of Specifications and Subtyping). That is, an implementation of the refinement must satisfy the original specification, as well as any additional specification cases.

(See section 10.2 Class Refinement for how to refine the specification of a member function in a class by refining the class as a whole. See section 10.5 Namespace Refinement for how to refine the specification of a function declared in a namespace.)

For example, consider the following informal specification.

// @(#)$Id: SetToRMS-informal.lh,v 1.5 1997/06/03 20:29:51 leavens Exp $
extern void SetToRMS(double & v, double x, double y) throw();
//@ behavior {
//@   requires informally "x and y are not too big";
//@   modifies v;
//@   ensures informally "v' is an approximation to"
//@                      "the root mean square of x and y";
//@ }

This can be refined into a formal specification as follows.

// @(#)$Id: SetToRMS-formal.lh,v 1.6 1997/06/03 20:29:50 leavens Exp $

#include "SetToRMS-informal.lh"

//@ refine SetToRMS
//@ by
extern void SetToRMS(double & v, double x, double y) throw();
//@ behavior {
//@   requires (x*x) + (y*y) < DBL_MAX;
//@   modifies v;
//@   ensures  approx(v' * v', rational((x*x) + (y*y) / 2.0), 1/100);
//@ }

The above specification allows either the positive or the negative root to be placed in v. We could refine the above specification further by specifying that the positive root only is to be placed in v. This is done below. Since this additional specification is added to the specification above, there is no need to repeat the postcondition above. (The precondition must be repeated, because otherwise the function would be required to terminate normally even when the precondition is not met. The modifies-clause also must be repeated, because otherwise the specification would become unsatisfiable.)

// @(#)$Id: SetToRMS-refined.lh,v 1.6 1997/06/13 05:23:46 leavens Exp $

#include "SetToRMS-formal.lh"

//@ refine SetToRMS
//@ by
extern void SetToRMS(double & v, double x, double y) throw();
//@ behavior {
//@   requires (x*x) + (y*y) < DBL_MAX;
//@   modifies v;
//@   ensures  v' >= 0.0;
//@ }

A function that satisfies the above refinement must return a positive approximation to the root mean square of x and y. This can be seen clearly in the following slight desugaring, where all the specification cases have been gathered into one specification. The idea is that the function has to satisfy all of these spec-cases. (See section 6.10 Case Analysis for the meaning of such a specification and a further desugaring.)

// @(#)$Id: SetToRMS-desugared.lh,v 1.7 1997/07/31 04:02:26 leavens Exp $

extern void SetToRMS(double & v, double x, double y) throw();
//@ behavior {
//@   requires informally "x and y are not too big";
//@   modifies v;
//@   ensures informally "v' is an approximation to"
//@                      "the root mean square of x and y";

//@ also

//@   requires (x*x) + (y*y) < DBL_MAX;
//@   modifies v;
//@   ensures  approx(v' * v', rational((x*x) + (y*y) / 2.0), 1/100);

//@ also

//@   requires (x*x) + (y*y) < DBL_MAX;
//@   modifies v;
//@   ensures  v' >= 0.0;
//@ }

[[[Does one ever need to use the with refine-list with a function refinement?]]]

Go to the first, previous, next, last section, table of contents.