// /*--------------------------------------------------------*\
// | Concrete Template : XYZ_Kernel_1
// \*--------------------------------------------------------*/
#ifndef CT_XYZ_KERNEL_1
#define CT_XYZ_KERNEL_1 1
///-------------------------------------------------------------
/// Global Context ---------------------------------------------
///-------------------------------------------------------------
#include "AT/XYZ/Kernel.h"
#include "CT/DEF/Kernel_1.h" // suppose this class is
// parameterized by Item
// The following #include is in a formal comment because the names it
// brings into scope are used within formal comments in what follows.
// The compiler doesn't need them, but a human reader does need them
// in order to understand the formal comments and code in this
// component.
/*!
#include "AT/ABC/Some_Op.h" // suppose this utility class is
// parameterized by Item
!*/
///-------------------------------------------------------------
/// Interface --------------------------------------------------
///-------------------------------------------------------------
// In this example, there is one parameter to the abstract template
// being implemented, plus three additional components used in the
// implementation. The latter three are all declared as concrete
// template parameters, with defaults selected by the implementer
// whenever possible. In this case, DEF_Kernel_1 has been chosed as a
// default implementation (of DEF_Kernel, assuming that's what it
// implements), and the only implementation of Representation has been
// chosed for the data representation record Rep. A client using this
// component MUST provide actual components for all the non-default
// parameters, and MAY provide actual components as replacements for
// the default parameters. Typically, a client will provide ONLY the
// non-default parameters.
concrete_template <
concrete_instance class Item,
concrete_instance utility_class ABC_Utility,
/*!
implements
abstract_instance ABC_Some_Op <Item>
!*/
concrete_instance class DEF_Of_Item =
DEF_Kernel_1 <Item>,
concrete_instance class Rep =
Representation <
DEF_Of_Item,
Integer
>
>
class XYZ_Kernel_1 :
implements
abstract_instance XYZ_Kernel <Item>,
encapsulates
concrete_instance Rep
{
private:
// The following declarations are needed to give names to the
// fields of Rep, the data representation record for an object of
// type XYZ_Kernel_1. These are analogous to the "data members"
// of a class in an ordinary C++ class design. If one of the
// fields is itself a Record instance, then there are also
// field_name declarations here.
rep_field_name (Rep, 0, DEF_Of_Item, name_of_field_0);
rep_field_name (Rep, 1, Integer, name_of_field_1);
/*!
[mathematical definitions needed to explain convention and
correspondence and anything else that follows]
convention
[assertion characterizing the "legal"
configurations of Rep, i.e., the data representation
record of an object of type XYZ_Kernel_1; also known as
the "representation invariant"]
correspondence
[assertion relating self (which is the abstract
value of an object of type XYZ_Kernel) to the
fields of Rep, i.e., self.name_for_field_0 and
self.name_for_field_1 (which comprise the
concrete representation of self); also known as the
"abstraction relation"]
!*/
// The following operation header and body appears ONLY if the
// default initial value for Rep does not represent an initial
// abstract value of an object of type XYZ_Kernel. It is
// analogous in functionality to the "constructor" in an ordinary
// C++ class design -- but it is invoked "lazily", i.e., not until
// initialization of the data representation record is no longer
// avoidable. This happens upon the first call to an operation
// other than object creation (or destruction), swap (&=), or
// Clear. If only these standard operations are invoked on an
// object, its data representation record is neither allocated nor
// initalized.
local_procedure_body Initialize ()
{
// The purpose of this code is to change one or both of
// self[name_of_field_0] and self[name_of_field_1] from their
// default initial values to the values needed to represent an
// initial value of type XYZ_Kernel.
}
// The following operation header and body appears ONLY if the
// representation of an object of type XYZ_Kernel_1 involves
// explicit use of pointers, and some of the operations do dynamic
// storage allocation. It is analogous in functionality to the
// "destructor" in an ordinary C++ class design -- but it is not
// invoked unless the (lazy) call to Initialize has actually
// occurred.
local_procedure_body Finalize ()
{
// The purpose of this code is to reclaim any otherwise
// unreclaimed storage that was allocated explicitly (using
// "New") by any operation in this class.
}
// The following operation is a local "helper" operation that may
// be called in the bodies of Initialize and/or Finalize and/or
// the XYZ_Kernel operations. There may be zero or more local
// operations, and they may call each other (and/or themselves
// recursively).
local_procedure_body Local_Op (
// formal parameters of Local_Op, if any, with their modes
// and types
)
/*!
requires
[precondition of Local_Op]
ensures
[postcondition of Local_Op]
!*/
{
// This code may mention any of its formal parameters, but it
// may NOT mention self (or, by implication, any of the fields
// of self). Generally, some of these fields do need to be
// manipulated by such "helper" operations, and if so they
// must be passed as explicit parameters.
}
public:
// The following declaration is always needed in a concrete kernel
// component. It has one parameter: the name of the concrete
// component (class) we are in. It implements the standard
// operations to create (and destroy) objects of type
// XYZ_Kernel_1, as well as swap (&=) and Clear.
standard_concrete_operations (XYZ_Kernel_1);
procedure_body OpA (
preserves Integer i,
consumes Text& t,
produces Item& x
)
{
// This code may mention the formal parameters of OpA, the
// fields of Rep (here, self[name_of_field_0] and
// self[name_of_field_1]), and any local objects declared in
// the body of OpA. It may call private local operations such
// as Local_Op, using the syntax of a global operation call,
// i.e., without a receiver object. It also may call
// ABC_Utility::Some_Op, where Some_Op is a utility operation
// of utility_class ABC_Utility. But it may NOT call any of
// the XYZ_Kernel operations other than the four standard
// operations (including itself recursively), nor may it
// explicitly call Initialize or Finalize.
}
function_body Integer OpB (
preserves Text t,
preserves Item& x
)
{
// This code is similar to OpA, but as a function body it must
// return a value.
}
};
#endif // CT_XYZ_KERNEL_1
Last modified: Thu Jan 11 17:05:57 EST 2007
