Talk:Loop invariant

I'm rewriting the description of loop invariants in Floyd-Hoare logic. Most of the existing text got deleted. I'm saving an example from the previous revision here, in case someone feels strongly that it should be preserved and wants to re-integrate it into the article. --MarkSweep 01:11, 17 Oct 2004 (UTC)

Example:

f(n)
{
  // {P: n >=0 }
  int k=n;
  int erg=1;
  while (k>0)
  {
    erg=erg*k;
    k=k-1;
  }
  // {Q: erg=k! }
}

Suitable invariant:

{ I: (n!=erg*k!) ^ (k>=0) }

Proof of the 4 points:

1. (n>=0), erg=1; k=n; => n!=n! ^ (n>=0) => (n!=erg*k!) ^ (n>=0)

2. {(n!=erg*k!) ^ (k>=0)} (k>0) => {I}

3. (n!=erg*k!) ^ (k>=0) ^ (k>0)

Now evaluate the program:

(n!=erg*k*(k-1)!) ^ (k>=-1) ^ (k>0)

=> (n!=erg*k!) ^ (k>0) = I ^ b => I

4. (n!=erg*k!) ^ (k>=0) ^ (k<=0)

=>  (n!=erg*k!) ^ (k=0)

=> (n!=erg)

q.e.d

No Floyd or Hoare references

It is strange that, in a discussion like this about loop invariants, there is no reference to Floyd or Hoare in the references.

These have just been added. It is indeed strange that they were not among the very first references added to the article. Deepmath (talk) 01:52, 25 August 2008 (UTC)

The link to [2], "Assigning Meanings to Programs" is broken. A copy exists online at https://classes.soe.ucsc.edu/cmps290g/Fall09/Papers/AssigningMeanings1967.pdf but I don't know how to update the reference properly. 72.68.150.92 (talk) 16:26, 11 November 2017 (UTC)

Update: I added the link but I'm not sure I did it 100% correctly, would appreciate someone checking my edit. Thanks! 72.68.150.92 (talk) 16:29, 11 November 2017 (UTC)

It seems that you deleted the Hoare.1969 reference by accident. I've restored it, and converted the Floyd reference to the {{cite journal}} format, keeping your new URL. - Jochen Burghardt (talk) 18:22, 11 November 2017 (UTC)

"In computer science, a loop invariant is an invariant used to prove properties of loops." When reading this definition, it is almost reads a loop invariant is an invariant loop. Maybe there is a better way to phrase this.

I wonder what this page says in english. 217.150.107.105 (talk) 12:32, 19 April 2010 (UTC)

Eiffel does not support loop invariants

Eiffel does not "support" loop invariants in any real sense; its loop invariants are simply syntactic sugar for assertions at the top of the loop. In particular, Eiffel makes no attempt to show that the invariant is inductive. Nor do the language semantics require a loop invariant to be inductive.

Many (essentially all) deductive verifiers for imperative programs support loop invariants. Erniecohen (talk) 12:45, 17 February 2013 (UTC)

I added your hint in the "Eiffel" section. I also changed the "until" condition there from "x=10" to "x>=10" (hope that's proper Eiffel syntax) to make the example more similar to the earlier C example.

Should some deductive verifiers be mentioned in the article?

Jochen Burghardt (talk) 12:59, 24 May 2013 (UTC)

Two definitions

Aren't there 2 definitions? The one provided, but also the one inferred by the page on Loop-invariant code motion where a loop invariant is code that doesn't depend on the actual loop and can be moved outside with no effect. — Preceding unsigned comment added by 78.22.121.243 (talk) 20:29, 13 August 2015 (UTC)

No, because "loop invariant" is a noun, and "loop-invariant" in "loop-invariant code" is an adverb. All the stuff in here about "loop-invariant code motion" is best left in Loop-invariant code motion. So I'm boldly removing it from here and leaving the short blurb linking to it at the top. 68.2.235.85 (talk) 21:34, 3 May 2016 (UTC)

@68.2.235.85: As a reaction to 78.22.121.243's above question and 2 edits of Nbarth on 4 Mar 2016, I'd written the section you deleted. It doesn't just duplicate Loop-invariant code motion#Example; instead, it tries to explain the fundamental difference of, and the relation between, "loop invariant" and "loop invariant code". Therefore, I still consider it worth to be included in this article, and I reinsert it here. Imho, saying only "both concepts are different" is unsatisfactory, since (1) it leaves the reader with the question "Why then are both named almost similar", and (2) there is some relation between them (something doesn't change between successive loop iterations) which I tried to explain. I think that these explanations can still be improved (constructive edit are welcome), but they shouldn't be completely deleted. - Jochen Burghardt (talk) 11:53, 4 May 2016 (UTC)

To concur with Jochen (thanks for the explanation!): these are closely related but distinct notions, and thus should have their own articles and merit explanation of the connection and distinction, exactly as has been done. One can quibble about the level of detail, but some explanation is warranted somewhere!

—Nils von Barth (nbarth) (talk) 05:41, 9 May 2016 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Loop invariant. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20160304013345/http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf to http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 20:39, 25 May 2017 (UTC)