Abstraction and Verification in Alphard: Introduction to Language and Methodology

Abstract

Alphard is a programming language whose goals include supporting both the development of well-structured programs and the formal verification of these programs. This paper attempts to capture the symbiotic influence of these two goals on the design of the language. To that end the language description is interleaved with the presentation of a proof technique and discussion of programming methodology. Examples to illustrate both the language and the verification technique are included.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 14, 1976
Accession Number
ADA028365

Entities

People

  • Mary Shaw
  • Ralph L. London
  • William A. Wulf

Organizations

  • University of Southern California

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Algorithms
  • Applied Mathematics
  • California
  • Complex Variables
  • Computational Science
  • Computer Programming
  • Computers
  • Engineering
  • High Level Languages
  • Information Science
  • Language
  • Programming Languages
  • Software Development
  • Structured Programming
  • Trees (Data Structures)
  • Universities
  • Verification

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications