44

I'm reading Coders at Work, and in it there's a lot of talk about invariants. As far as I've understood it, an invariant is a condition which holds both before and after an expression. They're, among other things, useful in proving that loop is correct, if I remember my Logic course correctly.

Is my description correct, or have I missed something? Have you ever used them in your program? And if so, how did they benefit?

  • @Robert Harvey: Yeah, I just read that actually. But it seems to me that invariants are only useful when you're trying to prove something. Is this correct (no pun intended)? – gablin Dec 30 '10 at 21:30
  • That's my understanding; when you're trying to reason about your program, to prove its correctness. – Robert Harvey Dec 30 '10 at 21:46
  • 3
    @user9094: An assertion is a declaration that something is true at a particular point in runtime, and is represented in the code. An invariant is a statement (one hopes well-founded) that will always be true whenever it applies, and is not represented in the code itself. – David Thornley Dec 30 '10 at 21:59
  • 1
    Invariants are indeed useful for proving correctness, but they are not limited to that case. They are also useful for defensive-programming and during debugging. They don't just help prove your code is correct, they help reason about the code and find the location of the bugs close to the origins. – Oddthinking Dec 31 '10 at 0:45
35

In OOP, an invariant is a set of assertions that must always hold true during the life of an object for the program to be valid. It should hold true from the end of the constructor to the start of the destructor whenever the object is not currently executing a method that changes its state.

An example of invariant could be that exactly one of two member variables should be null. Or that if one has a given value, then the set of allowed values for the other is this or that...

I sometime use a member function of the object to check that the invariant holds. If this is not the case, an assert is raised. And the method is called at the start and exit of each method that changes the object (in C++, this is only one line...)

  • 10
    +1 for mentioning invariants need not be true in the middle of a executing method. – Oddthinking Dec 31 '10 at 0:42
  • 1
    @Oddthinking Best to avoid that when possible though. It would be easy to enter an invarient-breaking state and forget to restore everything correctly before returning. Exceptions could also give you trouble. – Alexander Jan 19 '18 at 16:45
  • 3
    @Alexander: For non-trivial invariants, it is almost impossible to avoid. If you need to update more than one variables in a method, as described in the answer, there is a point where only one has been updated and the invariant is false. There are enough constraints on writing good code without adding new ones. – Oddthinking Jan 19 '18 at 22:30
  • @Oddthinking Yeah, it's often quite unavoidable. But for example, if there is a group of variables that logically belong together (e.g. an array, and the index of a "selected" item in the array), then it's probably worth extracting them to a type. From there, mutations of the array or the type can be expressed as a single assignment of a new instance of that type – Alexander Jan 20 '18 at 0:33
9

Well, the stuff I'm seeing in this thread is all great, but I have a definition of an 'invariant' that has been tremendously helpful for me at work.

An invariant is any logical rule that must be obeyed throughout the execution of your program that can be communicated to a human, but not to your compiler.

This definition is helpful because it cleaves out conditions into two groups: those the compiler can be trusted with enforcing, and those that must be documented, discussed, commented, or otherwise communicated to contributors in order for them to interact with the codebase without introducing bugs.

Also, this definition is helpful because it allows you to use the generalization, "Invariants are bad".

As an example, the shifter in a manual transmission car is engineered to avoid an invariant. If I wanted, I could build a transmission with one lever for each gear. This lever could be forward ("engaged") or back ("disengaged"). In such a system, I have created an "invariant", which might be documented as such:

"It is critical that the currently engaged gear be disengaged before a different gear is engaged. To engage any two gears at the same time will cause mechanical stress that will tear the transmission apart. Always disengage the currently engaged gear before engaging another."

And so, one might blame broken transmissions on sloppy driving. Modern cars, however, use a single stick that pivots around among the gears. It's designed in such a way that, on a modern stick-shift car, it is not possible to engage two gears at the same time.

In this way, we could say that the transmission has been engineered to 'remove the invariant', because it does not permit itself to be mechanically configured in a way that violates the logical rule.

Every invariant of this kind that you remove from your code is an improvement, because it lowers the cognitive load of working with it.

  • 1
    If an invariant is any logical rule that must be obeyed throughout the execution of your program, and your logical rule is that no two gears may be engaged at the same time, then is not the invariant that no two gears may be engaged at the same time? Without this invariant, your transmission could be in two gears at the same time, and thus tear itself apart. First, isn't a single stick shifter actually enforcing that invariant? Second, why would an invariant be intrinsically good or bad? – Dustin Cleveland Feb 11 '18 at 20:23
  • 1
    The comparison to car's gears is very clear to me. Thanks! – Marecky Jun 25 '18 at 17:06
  • "An invariant is any logical rule that must be obeyed throughout the execution of your program that can be communicated to a human, but not to your compiler." - I quite like this, concise and easy to remember. – ZeroKnight Aug 22 '18 at 7:40
  • @DustinCleveland I think that in this example, the mechanisms behind the stick shift are the 'compiler' that 'enforces' the rules, whereas the driver that might otherwise cause an incident is one of the many clients that must consume and remember the information that's been "documented, discussed, commented, or otherwise communicated." – ebernard Jul 16 at 15:56
  • Brilliant explanation! I really understand now the reasoning on why having invariants in your code is bad practice. – Ben C Wang Aug 19 at 4:29
3

An invariant (in common sense) means some conditions that must be true at some point in time or even always while your program is executing. e.g. PreConditions and PostConditions can be used to assert some conditions that must be true when a function is called and when it returns. Object invariants can be used to assert that a object must have a valid state throughout the time it exists. This is the design by contract principle.
I have used invariants informally using checks in code. But more recently I am playing with the code contracts library for .Net that directly supports invariants.

3

Based on the following quote from Coders At Work...

But once you know the invariant that it's maintaining, you can see, ah, if we maintain that invariant then we'll get log lookup time.

...I guess "invariant" = "condition you want to maintain to ensure a desired effect".

It seems that invariant has two senses that differ in a subtle way:

  1. Something that stays the same.
  2. Something that you're trying to keep the same, in order to achieve goal X (such as a "log lookup time" above).

So 1 is like an assertion; 2 is like a tool for proving correctness, performance, or other properties - I think. See the Wikipedia article for an example of 2 (proving the correctness of the solution to the MU puzzle).

Actually a 3rd sense of invariant is:

.3. What the program (or module or function) is supposed to do; in other words, its purpose.

From the same Coders At Work interview:

But what makes big software manageable is having some global invariants or big-picture statements about what it's supposed to do and what things are supposed to be true.

1

An invariant is like a rule or an assumption that can be used to dictate the logic of your program.

For example, suppose you have some software application that keeps track of user accounts. Suppose also that user can have multiple account, but for whatever reason you need to differentiate between a user's main account and "alias" accounts.

This could be a DB record or something else, but for now lets assume each user account is represented by a class object.

class userAccount { private char * pUserName; private char * pParentAccountUserName;

... }

An invariant might be the assumption that if pParentAccountUserName is NULL or empty then this object is the parent account. You can use this invariant to distinguish different types of account. There are probably better methods to distinguish different types of user accounts, so keep in mind this is just an example to show how an invariant might be used.

  • Invariants check the state of a program. They're not design decisions. – Xavier Nodet Dec 30 '10 at 23:05
  • 3
    Invariants don't check anything. You can check the state of program to see if an invariant is TRUE or FALSE, but invariants themselves "do" nothing. – Pemdas Dec 30 '10 at 23:27
  • 2
    Typically, in C++ you would see some sort of class invariance such as member x must less than 25 and greater than 0. That is the invariant. Any checks against that invariant are assertions. In the example I have above, my invariant is if pParentAccountUserName is NULL or empty then it is a parent account. Invariants are designed decisions. – Pemdas Dec 30 '10 at 23:41
  • How do you check that if pParentAccountUserName is NULL or empty, this object is the parent account? Your statement only defines what a null/empty value is supposed to represent. The invariant is that the system conforms to that, i.e. that pParentAccountUserName can only be null or empty if it is a parent account. It's a subtle distinction. – Cameron Feb 21 '14 at 1:01
1

Coming from a physics background, in physics we have invariants, which are essentially quantities which do not vary throughout an entire computation/simulation. For instance, in physics, for a closed system total energy is conserved. Or again in physics, if two particle collide, the resulting fragments must contain exactly the energy they started with, and exactly the same momentum (a vector quantity). Usually there aren't enough invariants to totally specify the result. For instance in the 2particle collision, we have four invariants, three momentum components, and an energy component, but the system has six degrees of freedom (six numbers to describe its state). The invariants ought to be conserved to within rounding error, but their conservation does not prove the solution is correct.

So typically, these things are important as sanity checks, but by themselves they can't prove correctness.

  • 1
    -1 Invariants in physics are different. Calculating a solution is not the same as proving that an algorithm is correct. For the latter, invariants can prove correctness. – aaronasterling Dec 30 '10 at 22:52

protected by gnat Jan 19 '18 at 17:23

Thank you for your interest in this question. Because it has attracted low-quality or spam answers that had to be removed, posting an answer now requires 10 reputation on this site (the association bonus does not count).

Would you like to answer one of these unanswered questions instead?

Not the answer you're looking for? Browse other questions tagged or ask your own question.