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

// /*---------------------------------------------------------------------*\
// |   Abstract Instance:  Undirected_Graph_Kernel
// \*---------------------------------------------------------------------*/

#ifndef AI_UNDIRECTED_GRAPH_KERNEL
#define AI_UNDIRECTED_GRAPH_KERNEL 1

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

abstract_instance
class Undirected_Graph_Kernel
{
public:

    /*!
	math subtype EDGE is finite set of integer
	    exemplar e
	    constraint
	        |e| = 2

        math subtype UNDIRECTED_GRAPH_MODEL is
	    (
		nodes:  finite set of integer,
		edges:  finite set of EDGE
	    )
            exemplar g
	    constraint
		there exists nb: integer
	            (g.nodes = {n: integer where (1 <= n <= nb) (n)})  and
		for all e: EDGE where (e is in g.edges)
                    (for all n: integer where (n is in e)
                         (n is in g.nodes))
    !*/

    standard_abstract_operations (Undirected_Graph_Kernel);
    /*!
	Undirected_Graph_Kernel is modeled by UNDIRECTED_GRAPH_MODEL
	    initialization ensures
	        self.nodes = empty_set  and
	        self.edges = empty_set
    !*/
    
    procedure Set_Number_Of_Nodes (
	    preserves Integer nb
	) is_abstract;
    /*!
	requires
	    nb >= 0
	ensures
	    self.nodes = {n: integer where (1 <= n <= nb) (n)}  and
	    self.edges = empty_set
    !*/

    procedure Add_Edge (
	    preserves Integer n1,
	    preserves Integer n2
	) is_abstract;
    /*!
	requires
	    n1 is in self.nodes  and
	    n2 is in self.nodes  and
	    {n1, n2} is not in self.edges
	ensures
	    self.nodes = #self.nodes  and
	    self.edges = #self.edges union {{n1, n2}}
    !*/

    procedure Remove_Edge (
	    preserves Integer n1,
	    preserves Integer n2
	) is_abstract;
    /*!
	requires
	    n1 is in self.nodes  and
	    n2 is in self.nodes  and
	    {n1, n2} is in self.edges
	ensures
	    self.nodes = #self.nodes  and
	    self.edges = #self.edges - {{n1, n2}}
    !*/

    procedure Remove_Any_Incident_Edge (
	    preserves Integer n1,
	    produces Integer& n2
	) is_abstract;
    /*!
	requires
	    n1 is in self.nodes  and
	    there exists n: integer ({n1, n} is in self.edges)
	ensures
	    self.nodes = #self.nodes  and
	    self.edges = #self.edges - {{n1, n2}}
    !*/

    procedure Remove_Any_Edge (
	    produces Integer& n1,
	    produces Integer& n2
	) is_abstract;
    /*!
	requires
	    self.edges /= empty_set
	ensures
	    self.nodes = #self.nodes  and
	    self.edges = #self.edges - {{n1, n2}}
    !*/

    function Integer Number_Of_Nodes () is_abstract;
    /*!
	ensures
	    Number_Of_Nodes = |self.nodes|
    !*/

    function Boolean Is_Edge (
	    preserves Integer n1,
	    preserves Integer n2
	) is_abstract;
    /*!
	ensures
	    Is_Edge = ({n1, n2} is in self.edges)
    !*/

    function Integer Number_Of_Incident_Edges (
	    preserves Integer n
	) is_abstract;
    /*!
	ensures
	    Number_Of_Incident_Edges =
		|{n1: integer where ({n, n1} is in self.edges) (n1)}|
    !*/

    function Integer Number_Of_Edges () is_abstract;
    /*!
	ensures
	    Number_Of_Edges = |self.edges|
    !*/

};

//--------------------------------------------------------------------------

#endif // AI_UNDIRECTED_GRAPH_KERNEL