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:
“There were some schools, so called [in my youth]; but no qualification was ever required of a teacher, beyond “readin, writin, and cipherin,” to the Rule of Three. If a straggler supposed to understand latin, happened to sojourn in the neighborhood, he was looked upon as a wizzard. There was absolutely nothing to excite ambition for education.”
—Abraham Lincoln (1809–1865)
“When great changes occur in history, when great principles are involved, as a rule the majority are wrong.”
—Eugene V. Debs (1855–1926)
“Rules and particular inferences alike are justified by being brought into agreement with each other. A rule is amended if it yields an inference we are unwilling to accept; an inference is rejected if it violates a rule we are unwilling to amend. The process of justification is the delicate one of making mutual adjustments between rules and accepted inferences; and in the agreement achieved lies the only justification needed for either.”
—Nelson Goodman (b. 1906)
“Parents need to recognize that the negative behavior accompanying certain stages is just a small part of the total child. It should not become the main focus or be pushed into the limelight.”
—Saf Lerman (20th century)
“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)