Loop Variant - Rule of Inference For Total Correctness

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:

\frac{< \textrm{\ is\ well-founded},\;\;S\;} {\;\mathbf{while}\;C\; \mathbf{do}\; S \;},

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:

    “The principle of majority rule is the mildest form in which the force of numbers can be exercised. It is a pacific substitute for civil war in which the opposing armies are counted and the victory is awarded to the larger before any blood is shed. Except in the sacred tests of democracy and in the incantations of the orators, we hardly take the trouble to pretend that the rule of the majority is not at bottom a rule of force.”
    —Walter Lippmann (1889–1974)

    “Totalitarianism is never content to rule by external means, namely, through the state and a machinery of violence; thanks to its peculiar ideology and the role assigned to it in this apparatus of coercion, totalitarianism has discovered a means of dominating and terrorizing human beings from within.”
    —Hannah Arendt (1906–1975)

    “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)

    “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)