5
$\begingroup$

One of the topics that I've struggled to grasp the most in my basic computer theory course is that of making a loop invariant to prove correctness of an algorithm. Even with what should be fairly straightforward algorithms, I just don't really understand what sort of properties I should be using in order to make an effective loop invariant that helps to prove algorithm correctness.

Here's an example of some basic pseudocode that I can't create a loop invariant for:

FUNCTION(a, b): p <- 1 l <- 0 while p < a:     p <- p * b     l <- l + 1 return l 

Does anyone have some tips or resources that would help me get a better grasp on making loop invariants?

3 Answers 3