Re: [boost] [contract] relaxing preconditions in subcontracting

Subject: Re: [boost] [contract] relaxing preconditions in subcontracting
From: lcaminiti (lorcaminiti_at_[hidden])
Date: 2012-06-26 10:52:27

lcaminiti wrote
> 
> I'm honestly not sure, I need to think about it more and also check what
> Eiffel does... I'll take that as a homework.
> 

I've checked and my current library implementation does what Eiffel does in
this case.

Consider the following Eiffel program:

class
        B
feature
        f ( b: BOOLEAN )
                require
                        b
                do
                        print ("B%N")
                end
end

class
        D1
inherit
        B redefine f end
feature
        f ( b: BOOLEAN )
                require else
                        True
                do
                        print ("D1%N")
                end
end

class
        D2
inherit
        B redefine f end
feature
        f ( b: BOOLEAN )
                require else
                        False
                do
                        print ("D2%N")
                end
end

class
        APPLICATION
inherit
        ARGUMENTS
create
        make
feature {NONE} -- Initialization
        test ( b: B )
                do
                        b.f (False)
                end

        make -- Run application.
                local
                        d1: D1
                        d2: D2
                do
                        create d1
                        create d2
                        test(d1) -- OK: Subcontracted preconditions pass.
                        test(d2) -- Error: Subcontracted preconditins broken.
                end
end

test(d1) passes the subcontracted preconditions while test(d2) does not.
Therefore, the call b.f(False) passes the subcontracted preconditions if b
is an instance of D1 (d1) but it does not pass the subcontracted
preconditions if b is an instance of D2 (d2).

My library does the same thing:

#include <contract.hpp>

CONTRACT_CLASS(
    struct (B)
) {
    CONTRACT_CLASS_INVARIANT( void )

    CONTRACT_FUNCTION(
        public virtual void (f) ( bool b )
            precondition( b )
    ) {
        std::cout << "B" << std::endl;
    }
};

CONTRACT_CLASS(
    struct (D1) extends( B )
) {
    CONTRACT_CLASS_INVARIANT( void )

    CONTRACT_FUNCTION(
        public void (f) ( bool b ) override
            precondition( true )
    ) {
        std::cout << "D1" << std::endl;
    }
};

CONTRACT_CLASS(
    struct (D2) extends( B )
) {
    CONTRACT_CLASS_INVARIANT( void )

    CONTRACT_FUNCTION(
        public void (f) ( bool b ) override
            precondition( false )
    ) {
        std::cout << "D2" << std::endl;
    }
};

void test ( B& b )
{
    b.f(false);
}

int main ( void )
{
    D1 d1;
    D2 d2;
    test(d1); // OK: Subcontracted preconditions pass.
    test(d2); // Error: Subcontracted preconditions broken.
    return 0;
}

Again, I understand how it can be confusing that the call b.f(false) is
valid or not depending on the actual object referenced by b. Such a
confusion comes from the fact that subcontracted preconditions are evaluated
in logic-or (instead of logic-and) as I tried to explain the docs.

However, I'd suggest for my library to:
1) Either, implement subcontracted preconditions as Eiffel does and in
accordance to the substitution principle;
2) Or, disable subcontracted preconditions all together defining
CONTRACT_CONFIG_DO_NOT_SUBCONTRACT_PRECONDITIONS in accordance with N1962.

This way programmers can chose "I find subcontracted preconditions
confusing... then I disable them at compile-time" or "I find subcontracted
preconditions useful*... then I keep them and make them part of my design
but I also fully study and understand them".

(*) For example, a case where subcontracted preconditions _might_ be useful
is when the base class designer want to grant greater control to the derived
class designers using subcontracted preconditions and guarded postconditions
(as I showed in a previous example for unique/multiple_identifiers taken
from [Mitchell02]). But again, it's not clear if subcontracted preconditions
have real practical value as noted in N1962.

Thanks a lot.
--Lorenzo

--
View this message in context: http://boost.2283326.n4.nabble.com/contract-relaxing-preconditions-in-subcontracting-tp4631177p4631994.html
Sent from the Boost - Dev mailing list archive at Nabble.com.