n South African Computer Journal - A multi-level marketing case study : specifying forests and trees in Z : research article
|Article Title||A multi-level marketing case study : specifying forests and trees in Z : research article|
|© Publisher:||South African Computer Society (SAICSIT)|
|Journal||South African Computer Journal|
|Author||J.A. Van der Poll and P. Kotze|
|Publication Date||Jun 2003|
|Pages||17 - 28|
|Keyword(s)||Automated reasoning, D.2.4, Established Strategy, F.3.1, F.4.1, Formal specification, I.2.3, Multi-level marketing, OTTER, Precondition calculation, Resolution, Schema and Z|
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...