Invariants for sequences

[treiher]

It should be possible to define invariants for sequences, e.g. show that a sequence contains no duplicates:

type Extensions is sequence of Extension with
   Invariant => (for all I in Extensions => 
                   (for all J in Extensions =>
                      (if I /= J then Extensions (I) /= Extensions (J))));

For #8 / #1254 we also need a way to specify invariants that are checked for each element (e.g. while parsing):

   type Variable_Byte_Integer is sequence of Variable_Byte_Integer_Element
   with
      Value => 
         (Initial => 0,
          Next => Variable_Byte_Integer'Current * 128 + Variable_Byte_Integer'Element.Value,
          Until => (Variable_Byte_Integer'Element.More = False)),
      Element_Invariant => Variable_Byte_Integer'Position <= 4;