Bag

The Z notation is a formal specification language used for describing and mod-elling computing systems. Z notation was proposed by Abrial et al in 1974. Tools are available for simulation and validation of the model specified in Z. The Z no-tation is based upon set theory and mathematical logic. The mathematical logic is a first-order predicate calculus. Mathematical objects and their properties can be collected together in schemas- patterns of declarations and constraints [2]. The schema language can be used to describe the state of a system, and the ways in which a state may change. The state of the system can be modelled in Z on a component basis in a bottom up fashion. A schema specification modelling a component of the system state includes two parts- declaration part which specifies the fields or variables of the compo-nent (for example the declaration part of the schema Bag in Figure 1(a) specifies elements as a set of natural numbers) and a constraint part which specifies the invariants on the component (for example the constraint part of the schema Bag in Figure 1 specifies that each member in the set elements is either 1 or 2). A state change in the system is modelled with a schema called operation schema. An operation schema specifies the state change w.r.t. the schema mod-elling the system state. The state change is specified as a relation between the the pre-state and post-state of the schema modelling the system state. We cal