SSL Buffer.vdmpp Sprache: 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

quality89%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.