Example Design and Specification
Schemas InitClass1’ and InitClass2’ are the initial state schemas of the specification and the design
The functions append and subtract have the property that if ? and r do not contain any duplicate members then neither does append(?, r) nor subtract (?, r).
Hence we can be sure that ant state obtained from the initial state by the application of the operations Enter2 and Leave2 has the property that the sequence l that it is part of, doesn’t contain any duplicate elements.