/[eiffelstudio]/FreeELKS/tags/EiffelSoftware/Eiffel_66/library/structures/dispenser/heap_priority_queue.e
ViewVC logotype

Diff of /FreeELKS/tags/EiffelSoftware/Eiffel_66/library/structures/dispenser/heap_priority_queue.e

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 91893 by manus_eiffel, Mon May 24 22:24:19 2010 UTC revision 91894 by manus_eiffel, Mon Jun 28 17:16:55 2010 UTC
# Line 338  feature {NONE} -- Comparison Line 338  feature {NONE} -- Comparison
338                                  Result := False                                  Result := False
339                          end                          end
340                  ensure                  ensure
341                          definition: (a /= Void and b /= Void) implies Result = (a < b)                          asymmetric: Result implies not safe_less_than (b, a)
                         left_void_definition: (a = Void and b /= Void) implies Result  
                         right_void_definition: (a /= Void and b = Void) implies not Result  
342                  end                  end
343    
344  invariant  invariant

Legend:
Removed from v.91893  
changed lines
  Added in v.91894

  ViewVC Help
Powered by ViewVC 1.1.23