Algebraic tables : abstract computability and system documentation

• Main Author: Wilder, A. J.
• Published: Swansea University 1998
• Subjects: 519
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.636599

This thesis builds on the work of D. Parnas and other collaborators on the Naval Research Laboratory's pilot Software Cost Reduction Scheme for the A-7E aircraft. This thesis incorporates the tabular approach pioneered by this project into an algebraic environment to benefit the writers of algebraic specifications. Using generic techniques from research from the Software Engineering Research Group at McMaster this thesis defines six classes of function tables which may be used to define algebraic operations. Four of the six classes of function tables are: simple (finite non-recursive), nested, infinite and recursive. The remaining two are constructed by combining nested infinite and nested recursive function tables. Using Effective Definition Schemes (eds) of Friedman as a model of computation, we define the semantics of the classes of infinite function tables (simple or nested). For the class of finite function tables we restrict eds to finite eds. For the class of recursive function tables we extend eds to recursive eds. For all three models of computation we compare their computability with While and Straight Line high level programs. In addition, for the recursive eds we construct both their denotional and operational semantics and prove, in detail, their equivalence. The thesis concludes by applying the defined function tables to specifying embedded-systems, or interactive deterministic systems, which are not necessarily safety-critical. The hope is that these techniques can be used to engineer software to higher standards at the design stage of a project to reduce expensive maintenance costs. To illustrate the feasibility of this aim, we describe our experiences (with the supporting company Digita International) at applying these algebraic tables to documenting a commercial software feature.