Semantic Equality of Tables

Kavitha Nadarajah


This thesis presents an algorithm to determine semantic equality of two given tables used in software documentations.

Tabular notation is seen to be a useful method for formal specification of software systems {Parnas92}. Verification of the software specification is an important part of software life cycle when software is used in safety critical environments. Industries such as Ontario Hydro invest time and money to ensure that their design of safety critical software corresponds to specification {Viola95}.

In this thesis we present an algorithm to verify whether two given tabular expressions specify the same relation. This algorithm is useful in verifying whether the design corresponds to specification. This algorithm handles all tables described in {Abraham97}. We also present the design of a prototype tool which implements this algorithm, which can help us automate the verification of software design.