#41 destructors could have static postconditions

[Lorenzo Caminiti]

Destructors could have static postconditions (still non-static postconditions are not possible because no object after destruction, and preconditions are not possible because a destructor can be called for any properly constructed object at any time so only class invariants need to hold).

For example, a destructor could decrement a static counter:

    static int counter;
    CONTRACT_DESTRUCTOR(
        (~instance_counter) ( void )
            postcondition(
                auto old_counter = CONTRACT_OLDOF counter,
                counter = old_counter - 1
            )
    ) {
        counter--; // One less object exists.
    }

This change will be fully backward compatible (existing destructors, without any postcondition, will still work as expected).

[Lorenzo Caminiti]

• milestone changed from Release to Future

[Lorenzo Caminiti]

• priority changed from major to trivial
• status changed from new to accepted

The use cases for this feature are probably very limited (only one of the many examples I have programmed for the library).