Eine Implementierung der Prioritätenschlange

• Übernahme aus FIFO:
  • empty-queue
  • is-empty-queue?
  • first-of
  • remove-from

• Neu zu schreiben: add-p-elem

  

• Zum Korrektheitsbeweis:

  • Man zeigt zunächst, daß die beiden Konstruktoren nur Warteschlangen erzeugen, in denen die Elemente nach fallender Priorität geordnet sind.

  • Dann beweist man, daß aus dieser Aussage die ,,Axiome`` folgen.