|
Abstract:
|
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. |
