A refinement is a (possibly) stronger version of a specification. That is, a refinement may have fewer implementations that satisfy it than the original specification. This chapter describes how to specify a refinement of an existing specification, without rewriting the existing specification. Leaving the original specification alone allows you to specify different perspectives on the same class or function. Having different perspectives may be helpful to the reader; for example, you can provide an informal specification to orient the reader, a formal specification without implementation-specific details for use by client, and also a specification that records design decisions for use by maintainers of an implementation. Having the refinements is better than having a single specification, which would necessarily be overly-detailed for some readers.
In Larch/C++, refinements can be given for any declaration. or member-declaration (see section 7.2 Class Member Specifications).
The syntax of a refinement-declaration is as follows.
refinement-declaration ::= [ refine-prefix ] declaration refine-prefix ::=refinerefinable-id [withreplace-list ]byrefinable-id ::= original-class-name | typedef-class-name | class-key identifier | unqualified-id | template-class-name | template-non-class-name | original-namespace-name | namespace-alias-name
See section 9.2 The Uses Clause for the syntax of replace-list.
The declaration in a refinement-declaration must use the same identifier as the refinable-id. The refinable-id must name a class, struct, union, template, function, or namespace that has already been defined.
The basic semantics is that the C++ program module that includes the refinement-declaration must have a definition that satisfies the specification given in the refinement-declaration's declaration. The exact notion of satisfaction depends on the kind of declaration, but the idea is that the implementation must satisfy both the original specification and the specifications explicitly given in the refinement-declaration's declaration. The subsections below describe examples of refinement for various kinds of declarations.
Go to the first, previous, next, last section, table of contents.