Correctness Of An Iteration

There are several terminologies that I learned this week. Precondition refers to a condition before a loop iteration is starting. Some binary sort algorithm requires the list of numbers to be sorted in a certain way. Postcondition refers to a condition upon termination of the loop. Loop Invariant refers to the condition when an iteration finish. The loop invariant of the last iteration should be equal to the post condition and the every loop invariant should satisfy the precondition. If precondition, loop invariant, and termination happens, post condition is automatically satisfied. Precondition does not need to be proved because the condition depends on the user input. Loop invariant needs to be proved because if the loop invariant does not satisfy, the post condition cannot be satisfied. In order to prove the loop invariant, you let the current iteration to be i and the next iteration to be i+1. Why do we consider the next iteration? It is because the variables at i+1th iteration is same as the variables at the end of ith iteration. Termination needs to be proved too. Mostly, we do not need to use induction to prove because we can refer to the loop invariant to prove the termination. In order to prove the post-condition we simply prove precondition, loop-invariant, and termination. Then we match with the post-condition.
From this, I learned that this will be useful to create an algorithm. Sometimes, a loop falls into a infinite loop. Rather then using trial-and-error method, this proof should take longer but make more senses to me. From now on, I think I will briefly use this method to create a looping algorithm to make sure that the loop terminates and returns the value I wanted.