About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
Theoretical Computer Science
Paper
Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
Abstract
The simple set WL of deterministic while programs is defined and a number of known methods for proving the correctness of these programs are surveyed. Emphasis is placed on the tradeoff existing between data-directed and syntax-directed methods, and on providing, especially for the latter, a uniform description enabling comparison and assessment. Among the works considered are the Floyd/Hoare invariant assertion method for partial correctness, Floyd's well-founded sets method for termination, Dijkstra's notion of weakest precondition, the Burstall/Manna and Waldinger intermittent assertion method and more. Also, a brief comparison is carried out between three logics of programs: dynamic logic, algorithmic logic and programming logic. © 1980, All rights reserved.