I want to know if given a while loop:

x = 0
while(x < 5){
     x = x + 1

I want to show that x (at the a ith iteration of the loop), the value of i is assigned to x and x is never assigned the same value twice. Like we know that running code that the sequence of assignments is 0, 1, 2, 3, 4, 5. But in a theoretic sense a sequence of assignments like 0, 1, 1, 5 will still terminate the loop.

It's easy to do this via induction but I am having difficulty doing this with Hoare logic.

I want to know, if I show the loop invariant holds via induction can I then use the loop invariant in proving the algorithm with the while rule i.e. in the Hoare triple.


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.