What are invariants, how can they be used, and have you ever used it in your program?

Question

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?

Answer 1

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

Answer 2

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.

Answer 3

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.

Answer 4

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.