Kolejki priorytetowe

Zadanie składa się z następujących trzech części:

specyfikacja kolejki priorytetowej,
użycie tej specyfikacji do udowodnienia poprawności generycznego algorytmu sortującego, używającego kolejki priorytetowej,
implementacja specyfikacji za pomocą kopców dwumianowych.

Wszystkie elementy tej modelizacji powinny byc sparametryzowane typem wyposażonym w funkcję porównujacą, czyli przez moduł spełniający specyfikację OrderedType.

Szczegóły:

Ad 1. Coq'owa specyfikacja kolejki priorytetowej QueueSpec powinna byc oparta na specyfikacji Camlowej QUEUE, z nastepujacymi modyfikacjami:

z braku wyjątków typ wyjściowy funkcji find_min i delete_min powinien byc (option cośtam)
należy dopisac specyfikacje poszczególnych funkcji, dokładając, jeśli to konieczne, funkcje pomocnicze

Ad 2. Generyczny algorytm sortujący GenericSort powinien być funktorem o nagłówku:

Module GenericSort[X:OrderedType][Queue:QueueSpec with Module E:=X] <:
  SortSpec with Module E:=X.

gdzie SortSpec jest specyfikacją algorytmu sortującego.

Działanie GenericSort polega oczywiście na włożeniu do kolejki wszystkich elementów listy, a następnie wyjmowaniu ich ``po jednym'' i ustawianiu w posortowaną listę.

Ad 3. Implementacja kolejek priorytetowych za pomoca kopców dwumianowych powinna być funktorem BinHeap o nagłówku:

Module BinHeap[X:OrderedType] <: QueueSpec with Module E:=X.

Implementacja w Coqu powinna odpowiadać Camlowej implementacji funktora BinomialHeap

This document was translated from L^AT_EX by H^EV^EA.