Design and verification of information systems
Harry K. T. Wong · 1983
This thesis discusses the syntax and semantics of TAXIS, a language for the design of Interactive Information Systems (IISs). The thesis also examines the design and verification methodologies of programs that TAXIS supports. TAXIS offers (relational) database management facilities, a means of specifying semantic integrity constraints and an exception-handling mechanism, integrated into a single language through the concepts of class, property and the IS-A (generalization) relationship. The formalization of TAXIS involves a denotational semantics and an axiomatic semantics. The former uses simple mathematical concepts such as sets and functions to assign meaning to TAXIS constructs. The latter provides an axiomatization of TAXIS in the spirit of Hoare{69,71}. The two definitions are then shown to be consistent by proving that the denotational semantics satisfies (in the logical sense) the axiomatization. A new design methodology for IISs is also sketched in the thesis. This methodology is based on the concept of stepwise refinement through specialization. According to this method, an IIS is first designed at a fairly high level of abstraction which is later refined by introducing new classes that are specializations of existing ones. This design method is complementary to traditional design method (Wirth{71}) which are based on the concept of stepwise refinement through decomposition. Parallel to the design methodology, a verification methodology of IISs is established in that the correctness of an IIS is shown in a stepwise manner. Each refinement of an IIS can be specified and proven correct by using the results of the previous refinement. Hence, the verification process is considerably simpler.