A Formal System for Reasoning about Programs Accessing a Relational Database

• 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

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.