A Lambda-Calculus Model for Generating Verification Conditions.

Abstract

A lambda-calculus-based method is developed for the automatic generation of verification conditions. A programming language is specified in which inductive assertions associated with a program are incorporated within the body of the program by means of assert and maintain-while statements. This programming language includes the following features: assignments, conditionals, loops, compounds, ALGOL-type block structure. A model is developed which consists of rules to translate each statement in this programming language into the lambda-calculus. The model is such that the lambda-expression translation of any program reduces to a list (tuple) of lambda-expression representations of all verification conditions of the program. A proof of this property is given. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1981
Accession Number
ADA103751

Entities

People

  • Franz Winkler
  • S. Kamal Abdali

Organizations

  • Rensselaer Polytechnic Institute

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Automatic
  • Calculus
  • Computer Programming
  • Computer Programs
  • Computers
  • Demographic Cohorts
  • Environment
  • Language
  • Mathematics
  • New York
  • Programming Languages
  • Side Effects
  • Square Roots
  • Test And Evaluation
  • Translations
  • Verification

Fields of Study

  • Computer science

Readers

  • Computational Linguistics