Vicente:
Have you considered to add block invariants? Maybe you can complete the table Contract Programming Feature Comparison.
I think block invariants could be added if there was interest. Indeed, I have already implemented a class for Eiffel-like loop-contract with both invariants and variants (but I never use it in real code). In the Contract Programming proposal for the C++ standard, block invariants are interesting also because they allow for additional compiler optimization but this benefit does not apply to a library.
If I have understood your library require the type is CopyConstructible to manage with postconditions. Have you considered to relax this constraint?
Yes, the library requires that a type T is ConstantCopyConstructible in order for a variable of such a type to have old value in postconditions. However, this constraint only applies for a type T tagged copyable by programmers by copyable<T>. Therefore, if T is not ConstantCopyConstructible, or simply if its old value is not needed in postconditions, programmers do not tag T copyable and the library does not add any constraint on T (plus there is no extra copy overhead for old). ConstantCopyConstructible is same as the CopyConstructible concept but the copy constructor must operate on a *const* source object "T::T(T const& source)". Regards, Lorenzo