Software Engineering Stack Exchange is a question and answer site for professionals, academics, and students working within the systems development life cycle. It only takes a minute to sign up.
Sign up to join this community
I understand 'invariant' in its literal sense. I also recognize them when I type code. But I don't think I understand the importance of this term in the context of computer science.
Whenever I read conversations\white papers about language design from famous programmers\computer scientists, the term 'invariant' keeps popping up as a jargon; and that is the part I don't understand. What is so special about it?
An algorithm is a repeatable process. If it is repeatable, it has to have attributes that do not change with repetition. These are your invariants. The invariants are combined with and/or operate on the (potentially) varying data that will be fed into your algorithm.
Thus the whole point of programming is to identify what does not vary--that is essentially your program.
In object-oriented program, there is a notion that each object should do a single thing well. This essentially means that (for class-based OOP) a class defines the invariants for a single algorithm, along with place-holders (variables) for any variant data that its objects might need. Ideally in OO, you would isolate what varies as much as possible, so that each object is mostly invariant.
The notion of invariant is strongly linked with 'side effects'. I believe it was promoted by Bertrand Meyer's 'Design by Contract (DbC)' approach for software design.
DbC enriches Abstract Data Types (backbone of classes) with 3 important notions, preconditions, postconditions, invariants. It is easily explained when referring to procedures, so I'll try to explain in reference with it:
A precondition represents the condition input data for a procedure must respect in order to call that procedure. This precondition must be respected and enforced by the client of that particular procedure. The procedure designer might however defend from clients that do not respect the precondition by asserting that condition as first lines in the procedure. For example having a method double divide(double dividend, double divisor) a precondition might be divisor != 0.
A postcondition represents the a condition on the output data after the procedure returns; it is entirely the job of the procedure designer to respect this postcondition provided the precondition was respected; in a defense programming style before returning, the postcondition can be asserted.
An invariant can be regarded as a both a precondition and a postcondition, but with different understanding for precondition and postcondition from above concepts. An invariant basically says that the if the input has a particular condition met before the procedure was called, then that particular condition is valid after the procedure is called. For example a valid invariant for a procedure boolean search(int term, int array[]) might say that the state of array before the call is the same as it is after the call.
Enforcing invariants on procedures (and not only procedures) is a great thing since it reduces side effects; this is useful since side effects are a great evil in programming. A particular procedure might change the state of the input arguments, or change the state of some global variables, or depend on some global variables; this might lead to nasty situations where two identical calls on the same procedure (with the same input) might yield different outputs. This leads to knowing the history of the calls and is very hard to debug especially in a multithreading context.
An invariant is a logical property that is preserved by some operation(s).
You need invariants to reason about loops. Since you don't know beforehand how many iterations there will be (or you wouldn't need a loop), each iteration must preserve the invariant, so that at the end you can prove some useful property about the loop.
You need invariants to reason about properties of encapsulated data. Often the various data inside a module or object need to satisfy certain properties for correct operation (for example, a list representing a set must always be sorted). You want that each function or method operating on the data preserves these properties, so they are invariants, too.
From what i know the importance of invariant comes from the fact that it is the building block for proving that an algorithm does compute a certain function. For example you have developed a new sorting algorithm but how can you be so sure that it really sorts with every input or with every correct output. The next step is to construct invariants that correspond to do flow of the algorithm and prove that it sorts using the invariants.
In the context of a programming language's type system, an invariant type is a non-convertible type. For example in java, when overloading a method, all parameters are invariant, while the return type is covariant (may be the same or a subtype).
