A Formal System for Reasoning about Programs Accessing a Relational Database

A formal system for proving properties of programs accessing a database is introduced. Proving that a program preserves consistency of the database is one of the possible applications of the system. The formal system is a variant of dynamic logic and incorporates a data definition language (DDL) for...

Full description

Bibliographic Details
Published in:ACM Transactions on Programming Languages and Systems
Main Authors: Casanova, Marco R., Bernstein, Phillip A.
Format: Article in Journal/Newspaper
Language:English
Published: Association for Computing Machinery (ACM) 1980
Subjects:
DML
Online Access:http://dx.doi.org/10.1145/357103.357111
https://dl.acm.org/doi/pdf/10.1145/357103.357111
Description
Summary:A formal system for proving properties of programs accessing a database is introduced. Proving that a program preserves consistency of the database is one of the possible applications of the system. The formal system is a variant of dynamic logic and incorporates a data definition language (DDL) for describing relational databases and a data manipulation language (DML) whose programs access data in a database. The DDL is a many-sorted first-order language that accounts for data aggregations. The DML features a many-sorted assignment in place of the usual data manipulation statements, in addition to the normal programming language constructs.

Similar Items