On forward and backward proof rules for program verification : (prepublication)
L. Ammeraal · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1976
The notions of "strongest verifiable consequent" and "weakest precondition", introduced by Floyd and Dijkstra, respectively, suggest a partition of proof rules into forward and backward rules.New notations for such rules are proposed and motivated.The paper advocates the "total correctness" point of view.Forward and backward rules are specified for assignment statements, conditional statements and while statements.Proof rules may be related to one another; some of such relationships are presented with reference to set theory.