Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Item.vdmpp Sprache: VDM

Original von: VDM^©

class Buffer

instance variables

data : [nat] := nil

operations

public Buffer: () ==> Buffer
Buffer() ==
data := nil;

public Write: nat ==> ()
Write(newData) ==
  (IO`print("Writer wrote: "); IO`print(newData); IO`print("\n");
   data := newData;
  );

public Read: () ==> nat
Read() ==
  let oldData : nat = data
  in
    (IO`print("Reader read: "); IO`print(oldData); IO`print("\n");
     data := nil;
     return oldData;
    );

public IsFinished: () ==> ()
IsFinished() == skip;

sync

per Write => #fin(Read) = #fin(Write);
per Read => (#fin(Read) + 1) = #fin(Write);
--per Write => data = nil;
--per Read => data <> nil;
per IsFinished => #fin(Read) = 3;

end Buffer

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.