Using Trace Specifications for Program Semantics and Verification.
Interim rept. Oct 85-Sep 86,
NAVAL RESEARCH LAB WASHINGTON DC
Pagination or Media Count:
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.
- Computer Programming and Software