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 . 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
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,
(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
(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
(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