Partial and Total Correctness
Standard Hoare logic proves only partial correctness, while termination needs to be proved separately. Thus the intuitive reading of a Hoare triple is: Whenever P holds of the state before the execution of C, then Q will hold afterwards, or C does not terminate. Note that if C does not terminate, then there is no "after", so Q can be any statement at all. Indeed, one can choose Q to be false to express that C does not terminate.
Total correctness can also be proven with an extended version of the While rule.
Read more about this topic: Hoare Logic
Famous quotes containing the words partial and, partial, total and/or correctness:
“The only coöperation which is commonly possible is exceedingly partial and superficial; and what little true coöperation there is, is as if it were not, being a harmony inaudible to men. If a man has faith, he will coöperate with equal faith everywhere; if he has not faith, he will continue to live like the rest of the world, whatever company he is joined to.”
—Henry David Thoreau (1817–1862)
“You must not be partial in judging: hear out the small and the great alike; you shall not be intimidated by anyone, for the judgment is God’s.”
—Bible: Hebrew, Deuteronomy 1:17.
“Someone once asked me why women don’t gamble as much as men do, and I gave the common-sensical reply that we don’t have as much money. That was a true but incomplete answer. In fact, women’s total instinct for gambling is satisfied by marriage.”
—Gloria Steinem (b. 1934)
“Rather would I have the love songs of romantic ages, rather Don Juan and Madame Venus, rather an elopement by ladder and rope on a moonlight night, followed by the father’s curse, mother’s moans, and the moral comments of neighbors, than correctness and propriety measured by yardsticks.”
—Emma Goldman (1869–1940)