Summary: Loop variants are a means of specifying bounded monotonic "progress" towards loop termination.

Loop variants (in the context of this discussion topic) are a means of specifying an expression that must change after each sequential loop iteration in a monotonic manner.

For example, if a loop is intended to iteratively refine an approximation

		 do 
		 {
		 	// adjust delta
		 	delta /= 2;
	

fuzzy = calculateFuzzy(estimate + delta);

		 } while (fuzzy > desiredFuzzy) variant Old(delta) > delta > 0;
	

This type of construct allows specification that not only must delta always be greater than 0, but that after each iterations (where the termination conditions is not met) that delta must take on a new value that satisfies "Old(delta) > delta" (i.e. monotonically decreasing) and "delta > 0" (i.e. bound).

From a program proof goal, this is important in that it aids proving that the loop will progress, and terminate. A far more detailed syntactic construct could be implemented that included separate handlers for multiple termination conditions, but that is a much larger deviation from standard C#. For example,

		 do 
		 {
		 	// adjust delta
		 	delta /= 2;
	

fuzzy = calculateFuzzy(estimate + delta);

		 } while (fuzzy > desiredFuzzy) {
	

// Handler for fuzzy <= desiredFuzzy

		 } variant Old(delta) > delta > 0 {
	

// Handler to catch violation of variant without an exception

		 }