CSE 321 Homework 5

1. Read the lab1 assignment. Then, carefully review the Sorting_Machine_Kernel_2 component which is included in this handout. In particular, look at:
   
   
• the representation,
• the convention, and
• the correspondence.
  
  
Explain in informal, intuitive terms what the convention and the correspondence state in formal terms. Note that we are not asking you to simply translate in English what the math says (e.g., don't say that "if self.inserting_rep then ..." means "if self.inserting_rep is true then ..."; instead say something like "if the sorting machine is in insertion phase then ..."). You have to show us that you understand what the convention and the correspondence are actually trying to say that would be helpful to the implementer. (Hint: The math predicate SUB_TREE_IS_ORDERED (a, start, stop) simply states that elements start through stop in the array a are an ARE_IN_ORDER heap according to the mapping from binary tree to array that we discussed in class.)

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

#ifndef CT_SORTING_MACHINE_KERNEL_2
#define CT_SORTING_MACHINE_KERNEL_2 1

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

#include "AT/Sorting_Machine/Kernel.h"
#include "CT/Queue/Kernel_1a.h"
#include "CT/Array/Kernel_1.h"
#include "CT/Array/Are_In_Order_At_1.h"
#include "CT/Array/Exchange_At_1.h"

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

concrete_template <
	concrete_instance class Item,
	concrete_instance utility_class Item_Are_In_Order,
        /*!
            implements
                abstract_instance General_Are_In_Order <Item>
        !*/
	concrete_instance class Queue_Of_Item =
            Queue_Kernel_1a <Item>,
	concrete_instance class Array_Of_Item =
            Array_Exchange_At_1 <
		    Item,
		    Array_Are_In_Order_At_1 <
			    Item,
			    Item_Are_In_Order,
			    Array_Kernel_1 <Item>
			>
                >,
	concrete_instance class Rep =
            Representation <
		    Boolean,
		    Queue_Of_Item,
		    Array_Of_Item,
		    Integer
		>
    >
class Sorting_Machine_Kernel_2 :
    implements
	abstract_instance Sorting_Machine_Kernel <Item, Item_Are_In_Order>,
    encapsulates
	concrete_instance Rep
{
private:

    rep_field_name (Rep, 0, Boolean, inserting_rep);
    rep_field_name (Rep, 1, Queue_Of_Item, queue);
    rep_field_name (Rep, 2, Array_Of_Item, array);
    rep_field_name (Rep, 3, Integer, heap_size);

    /*!
        math definition IS_ORDERED (
                s: string of Item
            ): boolean is
	    for all u, v: Item where (<u> * <v> is substring of s)
		(ARE_IN_ORDER (u, v))

        math definition LOCATIONS_OF_SUB_TREE_ELEMENTS (
		a: ARRAY_MODEL
		start: integer
		stop: integer
	    ): finite set of integer satisfies
	    if a.lb <= start <= stop <= a.ub
	    then
		LOCATIONS_OF_SUB_TREE_ELEMENTS (a,start,stop) =
		    {start} union
		    LOCATIONS_OF_SUB_TREE_ELEMENTS (a,2 * start,stop) union
		    LOCATIONS_OF_SUB_TREE_ELEMENTS (a,2 * start + 1,stop)
	    else
		LOCATIONS_OF_SUB_TREE_ELEMENTS (a,start,stop) = empty_set
		
        math definition SUB_TREE_ARRAY_ELEMENTS (
		a: ARRAY_MODEL
		start: integer
		stop: integer
	    ): finite multiset of Item satisfies
	    for all x: Item
		(x is in SUB_TREE_ARRAY_ELEMENTS (a, start, stop)  iff
		 there exists i: integer
		     (i is in LOCATIONS_OF_SUB_TREE_ELEMENTS (
			      a, start, stop)  and
		      (i, x) is in a.table))

	math definition SUB_TREE_IS_ORDERED (
		a: ARRAY_MODEL
		start: integer
		stop: integer
	    ): boolean satisfies
	    if a.lb <= start and 2 * start + 1 <= stop and stop <= a.ub
	    then
		for all x, y, z: Item
		where ((start, x) is in a.table  and
		       (2 * start, y) is in a.table  and
		       (2 * start + 1, z) is in a.table)
		    (SUB_TREE_IS_ORDERED (a, start, stop) =
		     SUB_TREE_IS_ORDERED (a, 2 * start, stop)  and
		     SUB_TREE_IS_ORDERED (a, 2 * start + 1, stop)  and
		     ARE_IN_ORDER (x, y)  and  ARE_IN_ORDER (x, z))
	    else if a.lb <= start and 2 * start <= stop and stop <= a.ub
	    then
		for all x, y: Item
		where ((start, x) is in a.table  and
		       (2 * start, y) is in a.table)
		    (SUB_TREE_IS_ORDERED (a, start, stop) =
		     SUB_TREE_IS_ORDERED (a, 2 * start, stop)  and
		     ARE_IN_ORDER (x, y))
	    else
		SUB_TREE_IS_ORDERED (a, start, stop) = true    

	convention
	    if self.inserting_rep
	    then
		self.heap_size = 0  and
		self.array = (1, 0, empty_set)
	    else
		self.array.lb = 1  and
		0 <= self.heap_size  and
		self.heap_size <= self.array.ub  and
		SUB_TREE_IS_ORDERED (self.array, 1, self.heap_size)  and
		self.queue = empty_string
		
	correspondence
	    self.inserting = self.inserting_rep  and
	    if self.inserting
	    then
		self.contents = multiset_elements (self.queue)
	    else
		for all x: Item
		    (x is in self.contents  iff
		     there exists i: integer
			 (self.array.lb <= i  and
			  i <= self.heap_size  and
			  (i,x) is in self.array.table))
    !*/

    // private local operations omitted

public:

    standard_concrete_operations (Sorting_Machine_Kernel_2);

    procedure_body Insert (
	    consumes Item& x
	)
    {
        // implementation omitted
    }

    procedure_body Change_To_Extraction_Phase ()
    {
        // implementation omitted
    }
   
    procedure_body Remove_First (
	    produces Item& x
	)
    {
        // implementation omitted
    }

    procedure_body Remove_Any (
	    produces Item& x
	)
    {    
        // implementation omitted
    }

    function_body Boolean Is_In_Extraction_Phase ()
    {
        // implementation omitted
    }

    function_body Integer Size ()
    {
        // implementation omitted
    }

};

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

#endif // CT_SORTING_MACHINE_KERNEL_2