4. Redundant invariants
•Given
     0 £ i £ j •Redundant
     a[i] Î a[0..j]
     max(a[0..i]) £ max(a[0..j])
•
•Redundant invariants are logically implied
•Implementation contains many such tests
[Say “greater than or equal to”, not “greater than”.]
May be implied by one other invariant or by a collection of other invariants.