Improvements to the Trace Assertion Method for Software Engineering

Andrew C.P. Dookhan


Many formal methods have been suggested for documenting software work assignments, some are discussed in [19]. This thesis presents a new version of Trace Assertion Method [1,10]. We refer to this new version as ITAM. TAM originated in 1977, [1,2]. Although TAM is sound, TAM specifications seem inappropriately complex. The complexity of a specification is not proportional to the complexity of the concepts being described. In this thesis we reintroduce TAM to document software work assignments, (i.e. module interface specifications). This thesis suggests improvements to TAM (ITAM) for programmers and specification writers. In doing this we :- (a) allow specification method writers to represent the state of an object, using sets. (b) view the collection of objects implemented by one module, as a single object (refer to as a primary object,) which may be composed of other objects. (c) presents objects' state representation semantics and a syntax that is more in tune with programmers' perceptions. (d) provide a tool that checks the syntax describing the canonical representation of an object's state. (e) provide commonly used predefined auxiliary functions to reduce redundant mathematical notation. (f) provide predefined auxiliary functions to be used when it is necessary to "check type" and "check availability" of an object, before performing operations on an object. (g) provide a method of abbreviating, long and duplicate, mathematical expressions. (h) use tables which can be easily checked for completeness and consistency, when we describe state changes of a module's objects, caused by invocations of that module's programs, (operation tables). (i) show that it is possible for ITAM to document polymorphic and non-deterministic module specifications. (j) provide a common compact and systematic document format for ITAM's module interface specifications.