Resolve/C++ Catalog
AT/XYZ/Kernel.h
Copyright © 2010, Reusable Software Research Group, The Ohio State University

//  /*-------------------------------------------------------------------*\
//  |   Abstract Template : XYZ_Kernel
//  \*-------------------------------------------------------------------*/

#ifndef AT_XYZ_KERNEL
#define AT_XYZ_KERNEL 1

///------------------------------------------------------------------------
/// Global Context --------------------------------------------------------
///------------------------------------------------------------------------

// This section contains #includes for other abstract components
// that XYZ_Kernel depends on; typically, there are none.  If there is
// nothing in the section, the comment header may be omitted.

///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------

// In this example, there is one parameter to the abstract template.
// This is typical when using templates for generalization, though in
// general there may be more and they may be restricted to
// implementing certain abstract components.

abstract_template <
        concrete_instance class Item
    >
class XYZ_Kernel
{
public:

    /*!
        [mathematics needed to explain the type XYZ_Kernel, i.e., its
         mathematical model; and to explain OpA, OpB, and other
         operations]
    !*/
    
    // The following declaration is always needed in an abstract
    // kernel component.  It has one parameter: the name of the
    // abstract component (class) we are in.  It indicates that any
    // implementation of XYZ_Kernel will have the standard operations
    // to create (and destroy) objects of type XYZ_Kernel, as well as
    // swap (&=) and Clear.
    
    standard_abstract_operations (XYZ_Kernel);
    /*!
	XYZ_Kernel is modeled by [mathematical model of an XYZ_Kernel
	                          object]
	initialization ensures
            [assertion characterizing an initial value of self]
    !*/

    // A procedure operation has zero or more explicit parameters,
    // with their modes and types (examples shown).  It also has an
    // implicit alters-mode receiver object of type XYZ_Kernel that
    // is referred to as "self" in the contract specification.
    
    procedure OpA (
	    preserves Integer i,
	    consumes Text& t,
	    produces Item& x
	) is_abstract;
    /*!
	requires
	    [precondition of OpA]
	ensures
	    [postcondition of OpA]
    !*/

    // A function operation has zero or more explicit parameters, with
    // their modes -- which must be "preserves" -- and types (examples
    // shown).  It also has an implicit preserves-mode receiver object
    // of type XYZ_Kernel that is referred to as "self" in the
    // contract specification.  The return type of the function
    // (example Integer shown) must be one of the built-in types
    // Boolean, Character, Integer, Real, or Text.  (The return-type
    // limitation does not apply to an "accessor" function, i.e.,
    // operator [], not illustrated in this simple example.  If
    // possible, a function should not have a precondition -- but this
    // cannot always be avoided, especially with accessors.)
    
    function Integer OpB (
	    preserves Text t,
	    preserves Item& x
	) is_abstract;
    /*!
	ensures
	    OpB = [expression for return value of OpB]
    !*/

};

#endif // AT_XYZ_KERNEL