Agree if the invariant that I may want to write is like "@ensures(valueField >=0)" .
However, I don't think I'll write this invariant.
I may want to write rather an invariant like this: @ensures (value==valueField) (http://en.wikipedia.org/wik...,
That will still ensure that the valueField will be "sound" anytime in any future implementation/subclass , even when constructor preconditions are weaker.