[ Home Page ] [ Eiffel Archive ] [ Eiffel Classes and Clusters ]

MPQ: A Minimum Priority Queue Class

Written by stimuli@shadow.netJeffrey Straszheim.

Extracted from eSockets by Geoff Eldridge

• Targets SmallEiffel -0.77b5 or newer.
• Version 0.2, 31 December 1999.
• Eiffel Forum Freeware License.

minimum_priority_queue_0_2.zip (7,000 bytes) source code

MPQ: A Minimum Priority Queue Class

Class extracted from the eSockets distribution for those wanting a MINIMUM_PRIORITY_QUEUE class with SmallEiffel. The interface follows:

class interface MINIMUM_PRIORITY_QUEUE[G->COMPARABLE]
   -- 
   --  A priority queue. item will always be the least element within this
   --  structure.
   -- 

creation
   make (initial_capacity: INTEGER)
      --  Create with initial_capacity.
      require
         positive: initial_capacity > 0
      ensure
         empty: count = 0;
         not_iterating: off

feature(s) from MINIMUM_PRIORITY_QUEUE
   --  Accessors

   empty: BOOLEAN
      --  Is the queue empty?

   count: INTEGER
      --  The number of elements in the queue

   item: G
      --  The minimum item in the queue
      require
         not_empty: not empty

   has (t: like item): BOOLEAN
      --  Is t in the queue?
      ensure
         sanity: Result implies not empty;
         priority_condition: Result implies item <= t

feature(s) from MINIMUM_PRIORITY_QUEUE
   --  Modifiers

   clear
      --  Empty the queue.
      require
         not_iterating: off
      ensure
         now_empty: empty

   put (t: like item)
      --  Add t to the queue.
      require
         not_void: t /= Void;
         not_iterating: off
      ensure
         size_increased: count = old count + 1;
         now_in_queue: has(t)

   remove (t: like item)
      --  Remove an t from the queue.
      require
         present: has(t);
         not_iterating: off
      ensure
         size_decreased: count = old count - 1;
         priority_condition: old item /= t and not empty implies item = old item

feature(s) from MINIMUM_PRIORITY_QUEUE
   --  Iteration

   start
      --  Begin iteration.
      ensure
         at_max: not off implies iter_item = item;
         boundry_behavior: empty = off

   forth
      --  Advance position
      require
         now_on: not off

   stop
      --  Force off.
      require
         now_on: not off
      ensure
         now_off: off

   off: BOOLEAN
      --  Have we finished?

   iter_item: like item
      --  The current item of iteration
      require
         now_on: not off
      ensure
         actual_item: Result /= Void

   iter_variant: INTEGER
      --  A variant for iterations

invariant

    non_negative: count >= 0;

    sensible_iterator: not off implies count > 0; -- 	priority_behavior: (not off) implies (iter_item <= item)
 --     Some problem with this assertion when iterating over the queue
 --     Needs to be fixed.

    empty_definition: empty = count = 0;

    good_fit: count = data.count;

    set_beginning: data.lower = 1;

    sensible_index: not off implies iter_index > 0 and iter_index <= count;

end of MINIMUM_PRIORITY_QUEUE[G->COMPARABLE]

The SmallEiffel web site is:

http://SmallEiffel.loria.fr/

[ Home Page ] [ Eiffel Archive ] [ Eiffel Classes and Clusters ]