Rule of Inference For Total Correctness
In order to formally state the rule of inference for the termination of a while loop we have demonstrated above, recall that in Floyd–Hoare logic, the rule for expressing the partial correctness of a while loop is:
where I is the invariant, C is the condition, and S is the body of the loop. To express total correctness, we write instead:
where, in addition, V is the variant, and by convention the unbound symbol z is taken to be universally quantified.
Read more about this topic: Loop Variant
Famous quotes containing the words rule of, rule, inference, total and/or correctness:
“Do I dare set forth here the most important, the most useful rule of all education? it is not to save time, but to squander it.”
—Jean-Jacques Rousseau (1712–1778)
“As long as fathers rule but do not nurture, as long as mothers nurture but do not rule, the conditions favoring the development of father-daughter incest will prevail.”
—Judith Lewis Herman (b. 1942)
“I shouldn’t want you to be surprised, or to draw any particular inference from my making speeches, or not making speeches, out there. I don’t recall any candidate for President that ever injured himself very much by not talking.”
—Calvin Coolidge (1872–1933)
“Nothing is so perfectly amusing as a total change of ideas.”
—Laurence Sterne (1713–1768)
“The surest guide to the correctness of the path that women take is joy in the struggle. Revolution is the festival of the oppressed.”
—Germaine Greer (b. 1939)