Alternative Trace Axioms for the WHILE Construct

Abstract

In NRL Report 9033 John McLean presents a programming language semantics, the extended trace language, based on the trace specification language. The simple programming language discussed in NRL Report 9033 contains the WHILE construct, and McLean gives this construct a natural and correct recursive treatment. This report shows that it is possible to use the extended trace language to give the WHILE construct two other quite different semantic treatments. One of these is based on the Hoare-style semantics for WHILE; the second is an alternative to the recursive axiom that could be used in cases where the verifier can discern at what point a given loop will terminate. It is significant that when using the extended trace language a verifier of software can choose from several different but equivalent semantic treatments of WHILE. The ability to choose an axiom for WHILE that fits the problem at hand makes the extended trace language an attractive software verification formalism.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 21, 1988
Accession Number
ADA200346

Entities

People

  • C. B. Cross

Organizations

  • United States Naval Research Laboratory

Tags

DTIC Thesaurus Topics

  • Arithmetic
  • Classification
  • Computer Programming
  • Identities
  • Information Systems
  • Invariance
  • Language
  • Military Research
  • Notation
  • Programming Languages
  • Security
  • Semantics
  • Specifications
  • Standards
  • Verification
  • Words (Language)

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.
  • Technical Research and Report Writing.