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?