daily pastebin goal
12%
SHARE
TWEET

Untitled

a guest Jun 13th, 2018 56 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. //  /*----------------------------------------------------------------------*\
  2. //  |   Concrete Template : Sorting_Machine_Kernel_2
  3. //  \*----------------------------------------------------------------------*/
  4.  
  5. #ifndef CT_SORTING_MACHINE_KERNEL_2
  6. #define CT_SORTING_MACHINE_KERNEL_2 1
  7.  
  8. ///------------------------------------------------------------------------
  9. /// Global Context --------------------------------------------------------
  10. ///------------------------------------------------------------------------
  11.  
  12. #include "AT/Sorting_Machine/Kernel.h"
  13. #include "CT/Queue/Kernel_1a.h"
  14. #include "CT/Array/Kernel_1.h"
  15. #include "CT/Array/Are_In_Order_At_1.h"
  16. #include "CT/Array/Exchange_At_1.h"
  17.  
  18. ///---------------------------------------------------------------------
  19. /// Interface ----------------------------------------------------------
  20. ///---------------------------------------------------------------------
  21.  
  22. concrete_template <
  23.     concrete_instance class Item,
  24.     concrete_instance utility_class Item_Are_In_Order,
  25.         /*!
  26.             implements
  27.                 abstract_instance General_Are_In_Order <Item>
  28.         !*/
  29.     concrete_instance class Queue_Of_Item =
  30.             Queue_Kernel_1a <Item>,
  31.     concrete_instance class Array_Of_Item =
  32.             Array_Exchange_At_1 <
  33.             Item,
  34.             Array_Are_In_Order_At_1 <
  35.                 Item,
  36.                 Item_Are_In_Order,
  37.                 Array_Kernel_1 <Item>
  38.             >
  39.                 >,
  40.     concrete_instance class Rep =
  41.             Representation <
  42.             Boolean,
  43.             Queue_Of_Item,
  44.             Array_Of_Item,
  45.             Integer
  46.         >
  47.     >
  48. class Sorting_Machine_Kernel_2 :
  49.     implements
  50.     abstract_instance Sorting_Machine_Kernel <Item, Item_Are_In_Order>,
  51.     encapsulates
  52.     concrete_instance Rep
  53. {
  54. private:
  55.  
  56.     rep_field_name (Rep, 0, Boolean, inserting_rep);
  57.     rep_field_name (Rep, 1, Queue_Of_Item, queue);
  58.     rep_field_name (Rep, 2, Array_Of_Item, array);
  59.     rep_field_name (Rep, 3, Integer, heap_size);
  60.  
  61.     /*!
  62.         math definition IS_ORDERED (
  63.                 s: string of Item
  64.             ): boolean is
  65.         for all u, v: Item where (<u> * <v> is substring of s)
  66.         (ARE_IN_ORDER (u, v))
  67.  
  68.         math definition LOCATIONS_OF_SUB_TREE_ELEMENTS (
  69.         a: ARRAY_MODEL
  70.         start: integer
  71.         stop: integer
  72.         ): finite set of integer satisfies
  73.         if a.lb <= start <= stop <= a.ub
  74.         then
  75.         LOCATIONS_OF_SUB_TREE_ELEMENTS (a,start,stop) =
  76.             {start} union
  77.             LOCATIONS_OF_SUB_TREE_ELEMENTS (a,2 * start,stop) union
  78.             LOCATIONS_OF_SUB_TREE_ELEMENTS (a,2 * start + 1,stop)
  79.         else
  80.         LOCATIONS_OF_SUB_TREE_ELEMENTS (a,start,stop) = empty_set
  81.        
  82.         math definition SUB_TREE_ARRAY_ELEMENTS (
  83.         a: ARRAY_MODEL
  84.         start: integer
  85.         stop: integer
  86.         ): finite multiset of Item satisfies
  87.         for all x: Item
  88.         (x is in SUB_TREE_ARRAY_ELEMENTS (a, start, stop)  iff
  89.          there exists i: integer
  90.              (i is in LOCATIONS_OF_SUB_TREE_ELEMENTS (
  91.                   a, start, stop)  and
  92.               (i, x) is in a.table))
  93.  
  94.     math definition SUB_TREE_IS_ORDERED (
  95.         a: ARRAY_MODEL
  96.         start: integer
  97.         stop: integer
  98.         ): boolean satisfies
  99.         if a.lb <= start and 2 * start + 1 <= stop and stop <= a.ub
  100.         then
  101.         for all x, y, z: Item
  102.         where ((start, x) is in a.table  and
  103.                (2 * start, y) is in a.table  and
  104.                (2 * start + 1, z) is in a.table)
  105.             (SUB_TREE_IS_ORDERED (a, start, stop) =
  106.              SUB_TREE_IS_ORDERED (a, 2 * start, stop)  and
  107.              SUB_TREE_IS_ORDERED (a, 2 * start + 1, stop)  and
  108.              ARE_IN_ORDER (x, y)  and  ARE_IN_ORDER (x, z))
  109.         else if a.lb <= start and 2 * start <= stop and stop <= a.ub
  110.         then
  111.         for all x, y: Item
  112.         where ((start, x) is in a.table  and
  113.                (2 * start, y) is in a.table)
  114.             (SUB_TREE_IS_ORDERED (a, start, stop) =
  115.              SUB_TREE_IS_ORDERED (a, 2 * start, stop)  and
  116.              ARE_IN_ORDER (x, y))
  117.         else
  118.         SUB_TREE_IS_ORDERED (a, start, stop) = true    
  119.  
  120.     convention
  121.         if self.inserting_rep
  122.         then
  123.         self.heap_size = 0  and
  124.         self.array = (1, 0, empty_set)
  125.         else
  126.         self.array.lb = 1  and
  127.         0 <= self.heap_size  and
  128.         self.heap_size <= self.array.ub  and
  129.         SUB_TREE_IS_ORDERED (self.array, 1, self.heap_size)  and
  130.         self.queue = empty_string
  131.        
  132.     correspondence
  133.         self.inserting = self.inserting_rep  and
  134.         if self.inserting
  135.         then
  136.         self.contents = multiset_elements (self.queue)
  137.         else
  138.         for all x: Item
  139.             (x is in self.contents  iff
  140.              there exists i: integer
  141.              (self.array.lb <= i  and
  142.               i <= self.heap_size  and
  143.               (i,x) is in self.array.table))
  144.     !*/
  145.  
  146.     local_procedure_body Initialize ()
  147.     {
  148.        // Students to fill this in
  149.  
  150.     self[inserting_rep] = true;
  151.     }
  152.  
  153.     // Add other local operations here
  154.  
  155.  
  156.     local_procedure_body Arrayify (
  157.     consumes Queue_Of_Item& queue,
  158.     produces Array_Of_Item& array
  159.     )
  160.     /*!
  161.       requires
  162.           A Queue_Of_Item with .Length() > 0
  163.       ensures
  164.           There exists an Array_Of_Item with the lowest item in
  165.           position [1].
  166.           Queue_Of_Item.Length() = 0.
  167.          
  168.     !*/
  169.     {
  170.     object Item temp;
  171.     object Integer count = 1;
  172.    
  173.     array.Set_Bounds (1, queue.Length());
  174.  
  175.     while (queue.Length() > 0)
  176.     {
  177.         queue.Dequeue (temp);
  178.         array[count] &= temp;
  179.         count++;
  180.     }
  181.     }
  182.  
  183.     local_procedure_body Sift_Root_Down (
  184.     alters Array_Of_Item& array,
  185.     preserves Integer start,
  186.     preserves Integer end
  187.     )
  188.     /*!
  189.       requires
  190.       ensures
  191.      !*/
  192.     {
  193.     object Integer root = start;
  194.    
  195.     while (root * 2 <= end)
  196.     {
  197.         object Integer count = (root * 2);
  198.         if ((count < end) and (array.Are_In_Order_At(count, count + 1)))
  199.         {
  200.         count++;
  201.         }
  202.         if (array.Are_In_Order_At(root, count))
  203.         {
  204.         array.Exchange_At (root, count);
  205.         root = count;
  206.         }
  207.         else
  208.         {
  209.         return;
  210.         }
  211.            
  212.     }
  213.     }
  214.  
  215.     local_procedure_body Heapify (
  216.     alters Array_Of_Item& array,
  217.     alters Integer start
  218.     )
  219.     /*!
  220.       requires
  221.       ensures
  222.      !*/
  223.     {
  224.     while (start > 0)
  225.     {  
  226.         Sift_Root_Down (array, start, self[heap_size]);
  227.         start--;
  228.     }
  229.     }
  230.    
  231.      
  232.  
  233. public:
  234.  
  235.     standard_concrete_operations (Sorting_Machine_Kernel_2);
  236.  
  237.     procedure_body Insert (
  238.         consumes Item& x
  239.     )
  240.     {
  241.        // Students to fill this in
  242.  
  243.     self[queue].Enqueue(x);
  244.    
  245.     }
  246.  
  247.     procedure_body Change_To_Extraction_Phase ()
  248.     {
  249.        // Students to fill this in
  250.  
  251.     self[inserting_rep] = false;
  252.     Arrayify (self[queue], self[array]);
  253.     Heapify (self[array], self[array].Upper_Bound() / 2);
  254.     self[heap_size] = self[array].Upper_Bound();
  255.    
  256.     }
  257.    
  258.     procedure_body Remove_First (
  259.         produces Item& x
  260.     )
  261.     {
  262.        // Students to fill this in
  263.     x.Clear();
  264.  
  265.     if (not self[inserting_rep])
  266.     {
  267.         x &= self[array][1];
  268.         self[array].Exchange_At (self[array].Lower_Bound(), self[heap_size]);
  269.         if(self[heap_size] > 1)
  270.         {
  271.         Sift_Root_Down (self[array], self[array].Lower_Bound(), self[heap_size]);
  272.         }
  273.         self[heap_size]--;
  274.     }
  275.     }
  276.  
  277.     procedure_body Remove_Any (
  278.         produces Item& x
  279.     )
  280.     {    
  281.        // Students to fill this in
  282.     x.Clear();
  283.  
  284.     if (not self[inserting_rep])
  285.     {
  286.        
  287.         x &= self[array][self[heap_size]];
  288.         self[heap_size]--;
  289.     }
  290.     else
  291.     {
  292.         self[queue].Dequeue(x);
  293.     }
  294.     }
  295.  
  296.     function_body Boolean Is_In_Extraction_Phase ()
  297.     {
  298.        // Students to fill this in
  299.  
  300.     return not self[inserting_rep];
  301.     }
  302.  
  303.     function_body Integer Size ()
  304.     {
  305.        // Students to fill this in
  306.     if (not self[inserting_rep])
  307.     {
  308.         return self[heap_size];
  309.     }
  310.     else
  311.     {
  312.         return (self[queue].Length());
  313.     }
  314.     }
  315.  
  316. };
  317.  
  318. //----------------------------------------------------------------------
  319.  
  320. #endif // CT_SORTING_MACHINE_KERNEL_2
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top