Automatic Synthesis of Implementations for Abstract Data Types from Algebraic Specifications.

Abstract

This thesis explores an automatic method of synthesizing implementations for data types for their algebraic specifications. The inputs to the synthesis procedure consist of a specification for the implemented type, a specification for each of the implementing types, and a formal description of the representation scheme to be used by the implementation. The output of the procedure consists of an implementation for each of the operations of the implemented type in a simple applicative language. The inputs and the output of the synthesis procedure are precisely characterized. A formal basis for the method employed by the procedure is developed. The method is based on the principle of reversing the technique of proving the correctness of an implementation of a data type. The restrictions on the inputs, and the conditions under which the procedure synthesizes an implementation successfully are formally characterized.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1982
Accession Number
ADA121520

Entities

People

  • Mandayam K. Srivas

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • C4I
  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Applied Mathematics
  • Artificial Intelligence
  • Computational Science
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Equations
  • Formal Languages
  • Language
  • Mathematics
  • Programming Languages
  • Recursive Functions
  • Sequences

Readers

  • Computational Linguistics
  • Computer Science.