Using Trace Specifications for Program Semantics and Verification.

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 10, 1987
Accession Number
ADA179845

Entities

People

  • John A. McLean

Organizations

  • United States Naval Research Laboratory

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Classification
  • Computer Program Verification
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Language
  • Military Research
  • Number Theory
  • Procedural Programming
  • Procedural Programming Language
  • Programming Languages
  • Security
  • Semantics
  • Specifications
  • Standards

Fields of Study

  • Computer science
  • Engineering

Readers

  • Artificial Intelligence
  • Software Engineering
  • Strategic Security Studies