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:
“The first rule of venture capitalism should be Shoot the Inventor.”
—Richard, Sir Storey (b. 1937)
“As long as fathers rule but do not nurture, as long as mothers nurture but do not rule, the conditions favoring the development of father-daughter incest will prevail.”
—Judith Lewis Herman (b. 1942)
“I shouldn’t want you to be surprised, or to draw any particular inference from my making speeches, or not making speeches, out there. I don’t recall any candidate for President that ever injured himself very much by not talking.”
—Calvin Coolidge (1872–1933)
“I have often thought that if photography were difficult in the true sense of the term—meaning that the creation of a simple photograph would entail as much time and effort as the production of a good watercolor or etching—there would be a vast improvement in total output. The sheer ease with which we can produce a superficial image often leads to creative disaster.”
—Ansel Adams (1902–1984)
“The surest guide to the correctness of the path that women take is joy in the struggle. Revolution is the festival of the oppressed.”
—Germaine Greer (b. 1939)