buffersPP

Author: Yves Ledru

This model is made by Yves Ledru et al. in a paper illustrating the combinatorial testing tool called Tobias. In this model the traces to be used for combinatorial testing purposes have been redone by Peter Gorm Larsen. For more information see:

Filtering TOBIAS Combinatorial Test Suites, Yves Ledru, Lydie du Bousquet, Olivier Maury and Pierre Bontron, In Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, Springer, ISSN 0302-9743 (Print) 1611-3349 (Online), Volume 2984/2004.

Properties	Values
Language Version:	classic
Entry point :	new Buffers().getBuffers()

buffers2.vdmpp

              
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
            

Overture Tool

Formal Modelling in VDM

buffersPP

buffers2.vdmpp