0
$\begingroup$

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.

$\endgroup$

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.