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-case`s.
(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.