Using Trace Specifications for Program Semantics and Verification

摘要

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.