Formula simplification in relation to program verification
L. Ammeraal · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1977
Predicate transformers associated with assignment statements and conditional statements are straightforward and can easily be mechanized.Except for some simple cases, it is a non-trivial task to simplify the resulting predicates automatically.It appears that formula simplification is the heart of automatic aids for program verification.This paper shows how predicate transformations and formula simplifications can be expressed in ALGOL 68, a high-level programming language which has appropriate facilities for data structuring.