| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/buffersPP/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 1 kB |
|
Quelle buffers2.vdmpp Sprache: VDM |
|||||||||
|
\begin{vdm_al}
class Buffers instance variables b1 : nat := 0; b2 : nat := 0; b3 : nat := 0; inv b1 + b2 + b3 <= 40 and b1 <= b2 and b2 <= b3 and b3 - b1 <= 15 operations public Add: nat ==> () Add(x) == if x + b1 < b2 then b1 := b1 + x elseif b2 + x <= b3 then b2 := b2 + x else b3 := b3 + x pre x <= 5 and b1 + b2 + b3 + x <= 40 post b1 + b2 + b3 = b1~ + b2~ + b3~ + x; public Remove: nat ==> () Remove(x) == if x + b2 <= b3 then b3 := b3 - x elseif x + b1 <= b2 then b2 := b2 - x else b1 := b1 - x pre x <= 5 and x <= b1 + b2 + b3 post b1 + b2 + b3 + x = b1~ + b2~ + b3~; public getBuffers: () ==> nat * nat * nat getBuffers() == return mk_(b1,b2,b3) end Buffers class UseBuffers instance variables b : Buffers := new Buffers() traces S1: let x in set {1,...,5} in b.Add(x); b.getBuffers() S1': b.Add(1); (b.Add(2) | b.Add(3)); b.Add(4) S2: b.Add(2); ((let x in set {1,...,5} in b.Add(x)) | (let y in set {1,3,5} in b.Remove(y))){1,2}; b.getBuffers() S3: b.Add(5){7}; ((let x in set {1,...,5} in b.Add(x)) | (let y in set {1,3,5} in b.Remove(y))){1,2}; b.getBuffers() S4: let x in set {1,...,5} in b.Add(x); ((let x in set {1,...,5} in b.Add(x)) | (let y in set {1,3,5} in b.Remove(y))){1,3}; b.getBuffers() end UseBuffers \end{vdm_al} ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28