n South African Computer Journal - A multi-level marketing case study : specifying forests and trees in Z : research article




A formal specification of a multi-level marketing (MLM) business is presented. Specifying a MLM business boils down to specifying properties of and operations on mathematical forests and trees. The usefulness of the model-based specification language, Z, is investigated as a vehicle for a formal specification of these recursive structures. The specification is presented following a prescribed format, namely the Established Strategy for constructing a Z specification. The Established Strategy is augmented with the notion of proof aimed at corroborating the correctness of critical parts of a specification. We show how attempts at discharging two different proof obligations using the resolution-based, first-order theorem prover OTTER calls for the use of two automated reasoning strategies, namely avoiding equality and using resonance.


Article metrics loading...

This is a required field
Please enter a valid email address
Approval was a Success
Invalid data
An Error Occurred
Approval was partially successful, following selected items could not be processed due to error