[contract] the volatile issue

1 Oct 2011

      Hello all,

N1962 does not indicate that contracts for volatile members should be
handled in any special way (in fact, volatile is not discussed at all
in N1962).

My library does the following for volatile members:
1) The object `this` is const volatile (and not just const) while
checking preconditions, postconditions, and invariants for a volatile
member.
2) By default, class invariants of volatile members are the same as
for non-volatile members. However, programmers can specify a different
set of class invariants for volatile and non-volatile members if they
wish to do so.

The reason for 2) is that when programming a volatile member that
overloads a non-volatile member, programmers can already specify a
different set of preconditions and postconditions. Therefore, it
seemed reasonable to give the option to also specify a different set
of class invariants for volatile and non-volatile members (otherwise
why would the pre/postcondition of a volatile member be different from
the ones of its non-volatile version while the class invariants are
forced to remain the same?).

For example, consider a very strange number class which is
non-negative (>= 0) when used in non-volatile context but it is
non-positive (<= 0) when used in volatile context (probably not a
real-life example but still...). The contracts could read:

#include <contract.hpp>

CONTRACT_CLASS(
class (num)
) {
    CONTRACT_CLASS_INVARIANT(
        get() >= 0, // (1)
        volatile class( get() <= 0 ) // (2)
    )

public:
    CONTRACT_FUNCTION(
    public void (set) ( int x )
        precondition( x >= 0 ) // 3)
        postcondition( get() == x )
    ) {
        x_ = x;
    }

    CONTRACT_FUNCTION(
    public void (set) ( int x ) volatile
        precondition( x <= 0 ) // (4)
        postcondition( get() == x )
    ) {
        x_ = x;
    }

    CONTRACT_FUNCTION(
    public int (get) ( void ) const
    ) {
        return x_;
    }

    CONTRACT_FUNCTION(
    public int (get) ( void ) const volatile
    ) {
        return x_;
    }

    num ( ) : x_(0) {}
private:
    int x_;
};

int main ( ) {
    num p;
    p.set(3);

    num volatile v;
    v.set(-3);

    return 0;
}

Note that via function overloading it is automatically possible to
specify a different set of preconditions (and eventually
postconditions) for the volatile member (4) than for the non-volatile
member (5). Therefore, my library also allows to specify a different
set of class invariants for volatile members (2) than for non-volatile
members (1) so that the entire contract (including class invariants)
can be programmed differently for volatile members if programmers wish
to do so. However, if `volatile class(...)` is not used (default) the
class invariants:

CONTRACT_CLASS_INVARIANT( get() >= 0 )

are applied by the library to all members volatile and non-volatile.
(In this case, this invariant is compiled in const volatile context
iff the class has one or more volatile functions so a volatile verion
of get() is only requirement if a volatile version of set() is
introduced.)

What do you think?

Thanks,
--Lorenzo

Lorenzo Caminiti

Nevin Liber

Lorenzo Caminiti

tags

participants (2)