Abstract:
This paper reports on an ongoing experiment whose main
purpose is to investigate to what extent object orientation might
solve the existing or potential problems inherent in the verification
and validation of KBSs, when these investigations are carried out at a
level higher than the implementation level. Techniques for specifying
and reasoning about properties of KBSs have been described in previous
literature. The main contribution of this paper consists of applying
recent work on algebraic theory of object-oriented programming to the
specification and design of KBSs. We argue that algebraic
specification as a hybrid knowledge specification formalism together
with the object-oriented design method provide the properties that can
support formal reasoning for KBSs. We refer to the class of KBSs whose
development start from an explicit model of expertise. We describe a
framework where the explicit model can be formalized and then
refined. Refinement proceeds from a high-level to a low-level
specification in a correctness preserving manner, towards an
implementation. We present a minimal theory of refinement which allows
one to establish via formal argument that system requirements, class
specifications and classes are connected by a series of refinements.