Please help me understand how I would prove the partial correctness of the below pseudocode with respect to the following predicates:

Pre: {n>=0}

Post: {a^2 <= n and n < (a+1)^2)

That is,

   x:= 0;
   y:= 1;
   z:= 1;
   while y <= n do
      x:= x+1;
      z:= z+2;
      y:= y+z;
   a:= x;

An explanation would be much appreciated. I've read various PPTs and PDFs and still can't fully make sense of how to do this.

From what I can tell, I think that if the code is executed satisfying the precondition, then everything holds true. The problem is that I'm not sure how to formally prove that.

Considering Hoare's logic, would the Composition rule be applied here? Would each line of pseudocode be a consecutive "program" in the Hoare Triple? I guess one of the things confusing me is how to solve for multiple lines of code. Most examples I've come across are more simplified: { x + 1 = 43 } y := x + 1 { y = 43 }

  • $\begingroup$ Welcome to CS.SE! It's hard to know how to help you, as the question doesn''t give us much to go on: it doesn't tell us what has you confused, or what partial approaches you've made, or what approaches you've considered, or what your thoughts are. We want to help you understand concepts, not do an exercise for you. Can you try editing the question to ask about some conceptual uncertainty that is preventing you from doing this exercise, and show us how far you were able to get on your own? $\endgroup$ – D.W. Apr 22 '16 at 15:09
  • $\begingroup$ @D.W. Thank you for the response. By no means am I looking to have anyone complete an exercise for me, I'm just not sure where to begin I guess. A walk-through or explanation of a different problem to help me understand would also be appreciated. $\endgroup$ – JBenzie Apr 22 '16 at 15:13
  • 1
    $\begingroup$ @JBenzie: it may be helpful to look at the Wikipedia article on Hoar Logic. Section 3 explains the rules and gives some examples. However, note that for a different language, the inference rules would be different. (But I can see that the language you're using is essentially the same that Hoare used originally, and the same on the Wikipedia article) $\endgroup$ – Jay Apr 22 '16 at 15:34
  • 1
    $\begingroup$ @JBenzie: by the way, please double-check your pseudo-code. You use a begin..end pair for the whole probram, but seems to use indentation-delimited blocks for the while body. It would be better to keep block delimiting syntax uniform (including begin..end in the while body would fix that) $\endgroup$ – Jay Apr 22 '16 at 15:38
  • 1
    $\begingroup$ @Jay: Thank you for your time and patience. It's beginning to make sense to me now. Just took a little while for me to get my head wrapped around it... $\endgroup$ – JBenzie Apr 22 '16 at 18:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.