Date: 11/27/06 (Algorithms)    Keywords: no keywords

I'm trying to understand program verification using Hoare logic. I've looked through all the resources I could find online, but I'm still a bit lost as to how one actually goes about doing it.

I understand partial verification as: given some pseudocode and the input, prove that the pseudocode produces the desired output. Is that correct?

Now how does one do this? Represent every step of the code by a Hoare triple? If there are blocks within the program, is it all right to verify each block separately? To what extent of detail should you go (eg., element-wise assignment for arrays)? How about loops -- is it enough to show the final change of state after all the runs of the loop, or does it need to be done at each step?

Source: http://community.livejournal.com/algorithms/87401.html