Talk:Invariant (computer science)

Are final/const variables like in C++/Java not also a form of invariants? Wouter Lievens 12:00, 30 Mar 2005 (UTC) In Java, final primatives are indeed invariants. However, final object references are not unless the referenced class is immutable.

An invariant is a logical predicate really. It usually is a statement about a program, not part of it. For constants and finals, the invariant is simply that these variables don't change value. E.g. if we have int f(const int i) { ... } then an invariant throughout function f(n) should be { i == n }. For the same function f(int i) this would still be the invariant without the const qualifier in the declaration, the const qualifier just helps the compiler realize this, and may act as a hint to the caller.Pieter-Bas 13:21, 7 June 2007 (UTC)

final references

A final reference is an invariant. The object it references may not be. If the object is mutable, the reference can be considered an invariant and the object not an invariant. If the object is immutable, both become invariants. This is an important distinction when a program needs a reference to remain constant, yet needs the data it references to be mutable.

The Object Invariant page seems to be saying the same as the Class Invariant page, but even less coherently. A class invariant is something that is always maintained over the lifetime of every instance of that class. It's enforced by the language's runtime system or sometimes (e.g. in C++) it has to be enforced using various tricks or explicit code. I would just delete it and beef up the article on Class Invariance. Wouter - const (in C++) is a kind of invariance, but class invariance is guaranteed by private data - state that can be guaranteed to be consistent no matter what clients do with the public interface.

Are constant invariants?

The explanation doesn't tell about the difference between constants and invariants althoughj it seems that const. r also a form of invariants oly. —The preceding unsigned comment was added by Rohitm 001 (talk • contribs) 13:26, 19 January 2007 (UTC).

A constant is not an invariant, but a the fact that a constant must have a value is.

What kind of Latin is that?

In Latin, in means "in" or "on" or "into" or "onto," but not "not." LandruBek 20:30, 4 October 2007 (UTC)

did i miss something?

"Given that there is a single I in the starting string MI, and one is not a multiple of three, it's impossible to go from MI to MU as zero is a multiple of three."

Zero is a multiple of three? —Preceding unsigned comment added by 75.79.69.67 (talk) 19:03, 21 January 2010 (UTC)

Yes, this part is a bit confusing. Could anyone clarify this bit

yes, 0 is a multiple of every integer since 0=x.z where z can represent every number and x must be 0. Ethereal1m (talk) 07:15, 13 December 2011 (UTC)

Edit or eliminate example?

The article on this puzzle is stated using a valid typeface for the capital "I" (the letter after "H") that makes it unambiguously not an "L" (as in Louis) or a digit "1" (half of two). The same should be done here, or the entire example should be scrubbed in favor of a reference to the puzzle and a brief summary used here. (This reader's default browsing typeface shows all of the above as an unadorned vertical bar also indistinguishable from the symbol for "or" in many computer languages.)MartinRinehart (talk) 13:24, 9 April 2011 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Invariant (computer science). 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) 10:05, 12 April 2017 (UTC)

Softening assertions

I think some of the language is a little strong. Sentences like "..which is one of the reasons for that task being still extremely tedious". I am sure I would find that task tedious for some programs, perhaps not for short ones. "Tedious" is a subjective thing and an unnecessary judgement here, some people enjoy doing things that others find tedious. And here: "More sophisticated invariants generally have to be provided manually.", I think the addition of "generally" helps but it is possible in the future we could find sophisticated invariants automatically (undecideability doesn't prevent us from finding many useful invariants automatically, although we obviously don't seem to be very good at it).Maneesh (talk) 18:33, 23 August 2018 (UTC)

I used "tedious" to express that the task requires a lot of manual work, I didn't mean a subjective aspect. Maybe there is a better word to express this? (I'm not a native English speaker.) —

As for "more sophisticated invariants ...", I wanted to warn about too optimistic expectations. As far as I know, due to undecidibility issues it is even impossible to find all invariants expressible with +, *, ==, program variables, and constants. Of course, this doesn't exclude that some of them can be found. What about saying that the current state of the art doesn't allow for automatic detection of "more sophisticated" invariants, that research is going on to improve this, but that even for very simple classes of expressions not all of them can be detected due to undecidibility issues? Would that be ok for you? - Jochen Burghardt (talk) 11:29, 24 August 2018 (UTC)

Yes definitely know what you mean here and agree with the intention, I think the wording just needs to be a touch more careful to avoid making claims that aren't supported by the underlying reasoning. Another way of expressing might be "which is one of the reasons this is generally impractical for most programming tasks" (I think you'll have to refer to "practice", or "impractical", to refer to the idea that using invariants in a day-to-day sense is hard). No doubt that proving invariants isn't very useful in many practical scenarios. Undecidability says that there are classes of invariants that are true that we can't prove but it could be that all or many useful strong invariants can be proven and we just haven't found the right program to do it yet. Do my assertions seem true to you?Maneesh (talk) 16:40, 25 August 2018 (UTC)

I changed the wording in the article to your suggestion (except that I used "program" instead of "programming task", since only the former can have invariants). - I think the task of proving invariants should be distinguished from that of detecting them. In the former task, both the source code and the formulas are given, in the latter task, only the source code is given. Abstract interpretation can perform that latter task, but can detect only formulas from some simple classes. As a side remark, undicidability means that we know that we can never prove all formulas from some class, so we can't hope to find the right program for that in the future. However I believe (and guess you agree) that we can hope to obtain tools that are at least as good as trained humans in invariant detection and proving. - Jochen Burghardt (talk) 17:46, 25 August 2018 (UTC)

Perhaps it is worth differentiating between "generating sound invariants" vs. "generating likely invariants", and important distinction in the state of the art (e.g. Daikon generates likely invariants based on execution while other tools may generate sound invariants but they may not be relevant to execution). Yes agree, there is nothing in principle that makes it impossible to one day make tools that generate likely and/or sound (i.e., proven) invariants that are comparable to (or much much better) what a clever human could come up with.Maneesh (talk) 23:36, 25 August 2018 (UTC)