A Formal Method for the Abstract Specification of Software

Abstract

An intuitive presentation of the trace method for the abstract specification of software contains sample specifications, syntactic and semantic definitions of consistency and totalness, methods for proving specifications consistent and total, and a comparison of the method with the algebraic approach to specification. This intuitive presentation is underpinned by a formal syntax, semantics, and derivation system for the method. Completeness and soundness theorems establish the correctness of the derivation system vis -a -vis the semantics, the coextensiveness of the syntactic definitions of consistency and totalness with their semantic counterparts, and the correctness of the proof methods presented. Areas for future research are discussed.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1984
Accession Number
ADA462691

Entities

People

  • John A. McLean

Organizations

  • United States Naval Research Laboratory

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Boolean Algebra
  • Buildings And Structures
  • Computers
  • Consistency
  • Formal Languages
  • Language
  • Linguistics
  • Military Research
  • Number Theory
  • Programming Languages
  • Semantics
  • Specifications
  • Standards
  • Theorems
  • Vocabulary

Fields of Study

  • Computer science
  • Engineering

Readers

  • Mathematical Modeling and Probability Theory.
  • Software Engineering.