Raymond F. Boyce, Donald D. Chamberlin, et al.
CACM
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.
Raymond F. Boyce, Donald D. Chamberlin, et al.
CACM
Kafai Lai, Alan E. Rosenbluth, et al.
SPIE Advanced Lithography 2007
S.M. Sadjadi, S. Chen, et al.
TAPIA 2009
Liqun Chen, Matthias Enzmann, et al.
FC 2005