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, total and/or correctness:
“America is hard to see.
Less partial witnesses than he
In book on book have testified
They could not see it from outside....”
—Robert Frost (1874–1963)
“I believe in the total depravity of inanimate things ... the elusiveness of soap, the knottiness of strings, the transitory nature of buttons, the inclination of suspenders to twist and of hooks to forsake their lawful eyes, and cleave only unto the hairs of their hapless owner’s head.”
—Katharine Walker (1840–1916)
“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)