Author: Kevin Blackburn



This specification was produced during a VDM-SL course presented by Peter 
Gorm Larsen to ICL Enterprise Engineering in 1994. The modelling of bags 
was one of the exercises the attendees (including the author Kevin Blackburn) 
was confronted with during the course. This specification is mainly 
intended for the purpose of illustrating how bags can be used. This is
modelled using an executable subset and a collection of small tests are
included.


Language Version: classic
Entry point     : BAGTEST`TestBagAll()