On ProofAnnotationsForBubbleSort there was a point about value ranges on parameters (array-length in particular). I will try to elaborate on this one here by using a simple example with arithmetic.


  int mac(int a, int b, int c)
  {
    // variant a) [int.min <= a*b+c <= int.max]
    // variant b) [abs(a) < short.max && abs(b) < short.max-1 && abs(c) < int.max/2]

    int r = a*b+c;

    // [r == (num)a * (num)b + (num)c]
    return r;
  }

The usual problem with arithmetic on real hardware is overflow. At least it is, if proofs are considered. Here we have a simple MultiplyAccumulate with limited machine types ("int"), that can overflow (say, because we want the code to be correct, but fast). It may overflow the "int" range (say 32 bit) due to both multiplication or addition. But we want the result to be correct, i.e. equal to the 'same' calculation on true integer types ("num", see proof annotation before the return). 

How do we ensure this? For some values we definitly will have overflow. 
* Variant a) simply defines (in form of a precondition), that this will not occur by ensuring, that the result will always fit in the range. This has the advantage of being easily written and discarding no range at all, but moves the full proof obligation to the caller (having proven nothing really).
* Variant b) shows another way. Here we intentionally restrict the ranges on the input parameters such that the result will fit - which can and will be checked by the proof checker automatically. This discards a lot of range, but simplifies the task for the caller.

See ProofsCanBeSimple, AutomatedTheoremProving, ProofOfCorrectness