I currently am struggling to figure out, how to show that a program, which includes a loop, is correct. I am working on the basis of wp, vc and pc.
The loops in question are:
wp(while(i<n) i = i+1; | i >= n)
wp(while(true) x=4; |x=4)
where everything befeore the ";" is the program and everything after the "|" is the postcondition.
I heard in my lectures that you have to find the invariants as well as the terminating function of the program, but i currently do not really know how to do this intuitively. I heard, that you need to train this, but i did not see a example on this yet, mostly just theory. If someone could help me explain the verification of loops, that would be really kind.
I appreciate every bit of help.