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:
“Better the rule of One, whom all obey,
Than to let clamorous demagogues betray
Our freedom with the kiss of anarchy.”
—Oscar Wilde (1854–1900)
“The art of being a slave is to rule one’s master.”
—Diogenes of Sinope (c. 410–c. 320 B.C.)
“The inference is, that God has restated the superiority of the West. God always does like that when a thousand white people surround one dark one. Dark people are always “bad” when they do not admit the Divine Plan like that. A certain Javanese man who sticks up for Indonesian Independence is very lowdown by the papers, and suspected of being a Japanese puppet.”
—Zora Neale Hurston (1891–1960)
“The effectiveness of our memory banks is determined not by the total number of facts we take in, but the number we wish to reject.”
—Jon Wynne-Tyson (b. 1924)
“What will happen once the authentic mass man takes over, we do not know yet, although it may be a fair guess that he will have more in common with the meticulous, calculated correctness of Himmler than with the hysterical fanaticism of Hitler, will more resemble the stubborn dullness of Molotov than the sensual vindictive cruelty of Stalin.”
—Hannah Arendt (1906–1975)