|
\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.58 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
