Using Trace Specifications for Program Semantics and Verification.
McLean,John · Defense Technical Information Center (DTIC) · 1987
Traditional methods for proving program correctness the implementation-dependent specification methods. If abstract specifications are also used, these methods require a leap of faith to bridge the gap between an abstract specification and a program correctness statement. In this report the trace method of software specification is extended to provide a natural semantics for procedural programming languages. This extension is compared with other approaches for the giving program semantics and is seen to provide a method for proving program correctness that avoids the problems of those currently in use. Keywords: computer program verification; trace specification language.