Reasoning about the Properties of an Enterprise Information System.

Abstract

A condensed specification of a multi-level marketing enterprise in the Z specification language is presented and a number of proof obligations that result from operations on the state is stated. The feasibility of using certain reasoning heuristics for discharging proof obligations emerging from the specification is investigated and we show how two important proof obligations arising from the specification of a real-life enterprise may successfully be discharged using a suite of well-chosen heuristics.