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. (Author)

Open PDF

Document Details

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

Entities

People

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

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Computational Science
  • Computer Access Control
  • Computer Programming
  • Computer Science
  • Computers
  • Engineering
  • Information Science
  • Language
  • Programming Languages
  • Software Development
  • Structured Programming
  • Trees (Data Structures)
  • Universities
  • Verification

Fields of Study

  • Computer science

Readers

  • Agent-Based Social Robotics and Mobile-Assisted Learning in Virtual Environments.
  • Computational Linguistics
  • Systems Analysis and Design