Accession Number:

ADA179845

Title:

Using Trace Specifications for Program Semantics and Verification.

Descriptive Note:

Interim rept. Oct 85-Sep 86,

Corporate Author:

NAVAL RESEARCH LAB WASHINGTON DC

Personal Author(s):

Report Date:

1987-04-10

Pagination or Media Count:

16.0

Abstract:

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE