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:
“If our vaunted “rule of the people” does not breed nobler men and women than monarchies have done—it must and will inevitably give place to something better.”
—Anna Julia Cooper (1859–1964)
“When great changes occur in history, when great principles are involved, as a rule the majority are wrong.”
—Eugene V. Debs (1855–1926)
“I have heard that whoever loves is in no condition old. I have heard that whenever the name of man is spoken, the doctrine of immortality is announced; it cleaves to his constitution. The mode of it baffles our wit, and no whisper comes to us from the other side. But the inference from the working of intellect, hiving knowledge, hiving skill,—at the end of life just ready to be born,—affirms the inspirations of affection and of the moral sentiment.”
—Ralph Waldo Emerson (1803–1882)
“Unlike Descartes, we own and use our beliefs of the moment, even in the midst of philosophizing, until by what is vaguely called scientific method we change them here and there for the better. Within our own total evolving doctrine, we can judge truth as earnestly and absolutely as can be, subject to correction, but that goes without saying.”
—Willard Van Orman Quine (b. 1908)
“With impressive proof on all sides of magnificent progress, no one can rightly deny the fundamental correctness of our economic system.”
—Herbert Hoover (1874–1964)