S. Sattanathan, N.C. Narendra, et al.
CONTEXT 2005
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.
S. Sattanathan, N.C. Narendra, et al.
CONTEXT 2005
Elizabeth A. Sholler, Frederick M. Meyer, et al.
SPIE AeroSense 1997
S.M. Sadjadi, S. Chen, et al.
TAPIA 2009
B. Wagle
EJOR