Invariant example

[vprevosto]

Give an example of data invariant that express initialization properties over a global variable, such as an array containing pairwise distinct values.