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...
Published in: | ACM Transactions on Programming Languages and Systems |
---|---|
Main Authors: | , |
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Association for Computing Machinery (ACM)
1980
|
Subjects: | |
Online Access: | http://dx.doi.org/10.1145/357103.357111 https://dl.acm.org/doi/pdf/10.1145/357103.357111 |
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. |
---|