I guess it's nice to have such consistency but, as it happen, I would be very happy if there was some way to use the locals introduced in a precondition even if, to use it in a redefinition, I had some syntactic overhead. For instance, I think the following kind of declaration would be totally justified:

class SOME_CHILD 
 
inherit
    SOME_PARENT
        redefine
            some_routine
        end
 
feature
 
    some_routine is
        local from {SOME_PARENT}.some_routine
            object_test_local: STRING
        do
            ...
        end
 
end

where object_test_local would be the name given to the attached entity resulting from an object test in the precondition of {SOME_PARENT}.some_routine. I expect that it could be smoothly extended for the case where a routine is a redefinition of more than one routine. For example, there could be a renaming clause to merge or separate object test locals. Also, in the case of a set of disjuncted preconditions, I would expect that, to be useable, an object test local would have to be bound in each of the precondition and it would keep the binding created by the first precondition to be completely evaluated to true. It might seem a bit complicated but I am certain that it is completely worth the trouble just to be able to profit from the object tests in preconditions. The alternative that I had to use so far was to repeat the object test in the body of the routine. This is very inconvenient.

Has any such alternative been studied so far? If so, on what ground was it rejected?

Having remote anchored types (like a.b.c) is basically a good extension to the language and in reflects a need in programming generic classes (not often needed; but if needed, it is very practical).

However the form `like a.b.c' is not sufficient. In some cases there is no argumentless query `a' in a generic `class C[G] ...' to start the remotely anchored type. Sometimes only the formal generic type `G' is available to start the anchor chain.

Therefore I would like to see the extension

 like {G}.some_query

to anchor a type within a generic `class C[G->CONSTRAINT]' to the result type of some query of its formal generic `G'

or alternatively (but more confusing)

too allow the start of the anchor chain `a' to be a query with arguments of the surrounding class.

A need of this extension is described (though not in detail) within my blog http://eiffelroom.com/node/396 which gives a solution to the catcall problem.

I re-coded my example of a MAYBE class using the new check form of assertion:

note
 
	description: "Objects that might contain another object"
 
	author: "Colin Adams"
	last_editor: "$Author: $"
	date: "$Date: $"
	revision: "$Revision: $"
	path: "$File: $"
 
class MAYBE [G]
 
create
 
	make,
	make_nothing
 
feature {NONE} -- Implementation
 
	make_nothing is
			-- Create as object absent.
		do
		ensure
			no_object_present: is_nothing
		end
 
	make (a_object: !G) is
			-- Create with object.
		do
			object := a_object
		ensure
			object_present: is_just
			object_set: object = a_object
		end
 
feature -- Access
 
	from_just: !G is
			-- Contained object
		require
			object_present: is_just
		do
			check  attached object as l_object then
					-- From precondition
				Result := l_object
			end
		end
 
feature -- Status report
 
	is_nothing: BOOLEAN is
			-- Is an object absent?
		do
			Result := (object = Void)
		ensure
			definition: Result = (object = Void)
		end
 
	is_just: BOOLEAN is
			-- Is an object present?
		do
			Result := not is_nothing
		ensure
			definition: Result = not is_nothing
			object_not_void: Result implies object /= Void
		end
 
feature {NONE} -- Implementation
 
	object: ?G
			-- Possible contained object
 
end

Finally the program actually behaves as it is supposed to. That is, a caller of from_just, when the precondition does not hold, get a pre-condition violation (if pre-conditions are monitored), or otherwise an assertion violation (even with all assertion monitoring disabled).

Looking at the code for from_just, the noise is confined to the check statement block (equivalent to an if statement). I still maintain this is too much noise. The pre-condition should act as a CAP, and so we should not have to perform an object test (that is, we ought to be able to simplify the body to Result := object). And while the type checker remains insufficiently powerful to prove that the precondition always holds, it can generate the same runtime-check (in void-safe mode) that the check block generates.