Chi-Leung Wong, Zehra Sura, et al.
I-SPAN 2002
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.
Chi-Leung Wong, Zehra Sura, et al.
I-SPAN 2002
S. Sattanathan, N.C. Narendra, et al.
CONTEXT 2005
Eric Price, David P. Woodruff
FOCS 2011
Matthias Kaiserswerth
IEEE/ACM Transactions on Networking