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

26 Jun 2012

      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-subcon...
Sent from the Boost - Dev mailing list archive at Nabble.com.