Constructor enforcement

Postconditions and invariants are now checked at the end of constructor
calls