An elementary and unified approach to program correctness

Abstract

We present through the algorithmic language DHL (Dijkstra-Hehner language), a practical approach to a simple first order theory based on calculational logic, unifying Hoare and Dijkstra's iterative style of programming with Hehner's recursive predicative programming theory, getting the best of the two worlds and without having to recur in any way to higher-order approaches such as predicate transformers, Hoare logic, fixed-point or relational theory.