Resolve/C++ Catalog
CT/Sequence/Kernel_1.h
Copyright © 2010, Reusable Software Research Group, The Ohio State University

//  /*----------------------------------------------------------------*\
//  |   Concrete Template : Sequence_Kernel_1
//  \*----------------------------------------------------------------*/

#ifndef CT_SEQUENCE_KERNEL_1
#define CT_SEQUENCE_KERNEL_1 1

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

#include "AT/Sequence/Kernel.h"

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

concrete_template <
	concrete_instance class Item,
	concrete_instance class Node,
	/*!
	    implements
		abstract_instance Record <
			Item,
			Pointer_C <Node>
		    >
	!*/
	concrete_instance class Rep =
            Representation <
		    Pointer_C <Node>,
		    Integer
		>    
    >
class Sequence_Kernel_1 :
    implements
	abstract_instance Sequence_Kernel <Item>,
    encapsulates
	concrete_instance Rep
{
private:

    rep_field_name (Rep, 0, Pointer_C <Node>, pre_front);
    rep_field_name (Rep, 1, Integer, length);

    field_name (Node, 0, Item, data);
    field_name (Node, 1, Pointer_C <Node>, next);

    /*!
	convention
	    self.pre_front /= NULL  and
	    self.length >= 0  and
	    [self.pre_front points to the first node of a
	     singly linked list containing self.length+1
	     Node nodes]
	     
	correspondence
	    self =
		<self.pre_front.next.data> *
		<self.pre_front.next.next.data> *
		... *
		<self.[last node in list].data>
    !*/

    local_procedure_body Initialize ()
    {
	New (self[pre_front]);
    }

    local_procedure_body Finalize ()
    {
	object Pointer_C <Node> p = self[pre_front];
	
	while (self[length] > 0)
	{
	    self[pre_front] = (*p)[next];
	    Delete (p);
	    p = self[pre_front];
	    self[length]--;
	}
	Delete (p);
    }

    local_procedure_body Move_To_Pos (
	    preserves Pointer_C <Node>& start,
	    produces Pointer_C <Node>& p,
	    preserves Integer pos
	)
    /*!
	requires
	    -1 <= pos  and
	    [start points to the first node of a singly linked
	     list containing at least pos Node nodes]
	ensures
	    [p points to the (pos+2)th node in the singly linked
	     list]  and
	    [the singly linked list has not been modified]
    !*/
    {
	object Integer p_pos = -1;
	p = start;
	while (p_pos < pos)
	{
	    p = (*p)[next];
	    p_pos++;
	}
    }

public:

    standard_concrete_operations (Sequence_Kernel_1);

    procedure_body Add (
	    preserves Integer pos,
	    consumes Item& x
	)
    {
	object Pointer_C <Node> before, on;
	
	Move_To_Pos (self[pre_front], before, pos - 1);
	New (on);
	
	(*on)[data] &= x;
	(*on)[next] = (*before)[next];
	(*before)[next] = on;

	self[length]++;
    }  

    procedure_body Remove (
	    preserves Integer pos,
	    produces Item& x
	)
    {
	object Pointer_C <Node> before, on;
	
	Move_To_Pos (self[pre_front], before, pos - 1);
	on = (*before)[next];
	
	x &= (*on)[data];
	(*before)[next] = (*on)[next];
	Delete (on);
    
	self[length]--;
    }

    function_body Item& operator [] (
	    preserves Integer pos
	)
    {
	object Pointer_C <Node> on;
	
	Move_To_Pos (self[pre_front], on, pos);
    
	return (*on)[data];
    }

    function_body Integer Length ()
    {
	return self[length];
    }

};

#endif // CT_SEQUENCE_KERNEL_1