FORMAL SPECIFICATION AND DECISION-SUPPORT

To gain widespread acceptance, decision support systems must be built to the highest possible standards. We believe techniques of formal specification and refinement have a valuable role to play in the development of certain components of decision support systems. We present a tutorial study of the use of formal specification focused on a system for maintaining deductive extensions of a knowledge base. The system is specified using an object-oriented variant of the specification language Z. The relationship of the formal specification with existing theoretical work in AI is discussed together with its refinement into a demonstrably correct implementation.