Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: DoubleListQueue.vdmpp Sprache: VDM

Original von: VDM^©

/*
* Queue using 2 sequences.
* Usage:
* make empty queue as following:
* let Q0 = DoubleListQueue`empty[int]() in ...
*
* append an element to queue:
* DoubleListQueue`enQueue(1, Q0)
*
*/

class DoubleListQueue

functions
static public empty[@T] : () -> seq of @T * seq of @T
empty() == mk_([], []);

static public isEmpty[@T] : (seq of @T * seq of @T) -> bool
isEmpty(s) == s = mk_([], []);

static public enQueue[@T] : @T * (seq of @T * seq of @T) -> seq of @T * seq of @T
enQueue(anElem, mk_(aHeads, aTails)) == mk_(aHeads, [anElem] ^ aTails);

static public deQueue[@T] : (seq of @T * seq of @T) -> [seq of @T * seq of @T]
deQueue(mk_(aHeads, aTails)) ==
cases aHeads:
  [-] ^ aTailsOfHeads -> mk_(aTailsOfHeads, aTails),
  [] ->
   cases aTails:
    []  -> nil,
    others -> mk_(tl Sequence`freverse[@T](aTails), [])
   end
end;

static public top[@T] : (seq of @T * seq of @T) -> [@T]
top(mk_(aHeads, aTails)) ==
cases aHeads:
  [h] ^ - -> h,
  [] ->
   cases aTails:
    []  -> nil,
    others -> hd Sequence`freverse[@T](aTails)
   end
end;

static public fromList[@T] : seq of @T * (seq of @T * seq of @T) -> seq of @T * seq of @T
fromList(aSeq, aQueue) ==
cases aSeq:
  []    -> aQueue,
  [h] ^ aTailsOfSeq  -> fromList[@T](aTailsOfSeq, enQueue[@T](h, aQueue))
end
measure fromListMeasure;

static fromListMeasure[@T] : seq of @T *  (seq of @T * seq of @T) +> nat
fromListMeasure(s, -) == len s;

static public toList[@T] : (seq of @T * seq of @T) -> seq of @T
toList(aaQueue) ==
cases aaQueue:
  (mk_([], [])) -> [],
  aQueue -> [top[@T](aQueue)] ^ toList[@T](deQueue[@T](aQueue))
end
measure toListMeasure;

static toListMeasure[@T] :  (seq of @T * seq of @T) +> nat
toListMeasure(mk_(s1, s2)) == len s1 + len s2;

end DoubleListQueue

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.