Constraints

1 January 1985

proceedings article
Published by Association for Computing Machinery (ACM)

p. 205-216
https://doi.org/10.1145/318593.318640

Abstract

A constraint is a relation among program variables that is maintained throughout execution. Type declarations and a very general form of aliasing can be expressed as constraints. A proof system based upon the interpretation of Hoare triples as temporal logic formulas is given for reasoning about programs with constraints. The proof system is shown to be sound and relatively complete, and example program proofs are given.

Keywords

UNIFORM APPROACH
GENERAL FORM
TEMPORAL LOGIC FORMULA
TYPE DECLARATION
PROGRAM VARIABLE
HOARE TRIPLE
EXAMPLE PROGRAM PROOF
PROOF SYSTEM
TEMPORAL LOGIC
TECHNICAL REPORT
TYPE INFERENCE
COMPUTER SCIENCE

This publication has 0 references indexed in Scilit: