Invariants called too many times and in wrong order

[nevdelap]

class A
	cue init
		base.init
		print 'inside init of A'

	def m1 as bool
		print 'inside invariant of A'
		return true

	invariant
		.m1

class B inherits A

	cue init
		base.init
		print 'inside init of B'

	def m2 as bool
		print 'inside invariant of B'
		return true

	invariant
		.m2

class P
	def main is shared
		B()

Actual result

inside init of A         (1)
inside invariant of A    (2)
inside init of B
inside invariant of A
inside invariant of A    (3)
inside invariant of B

(1) At the end of the base class constructor the object is not yet constructed and it's invariant need not hold and shouldn't be called.
(2) Additionally if the invariant is called at that point and includes calls to any methods overridden in the derived class they can fail because it hasn't constructed yet and its state is not ready to be used.
(3) Extra test of A's invariant just not needed. I guess it's because I've used calls to methods to show when it's in the invariants, but again, the object is not finished constructing so it need not call the invariant on the exit of that method. (It's finished constructing after the invariant check at the end of the most derived init, not before, so at any time before that, method calls, or whatever used in the init, the invariant shouldn't be called yet.)

Expected result

inside init of A
inside init of B
inside invariant of A
inside invariant of B

BTW: you can hit me up in chat to discuss, instead of us bouncing replies back and forth here. More productive, yeah? Cheers.

nevdelap(at)gmail(dot)com for *both* gmail chat & MSN, or nevdelap in yahoo.

[nevdelap]

(4) Use of methods or properties in the init is also very problematic, with or without inheritance, because the invariant is called prematurely in those cases too. The workaround is to comment out parts of the invariant.

[hopscc]

Re
1) If the base class has invariants then they should be true at the end of base class construction. Even though a derived object is not completely constructed its base class invariants should succeed at this point

2) Yes but familiar problem - similar to the situation calling (overridable) methods in a constructor.
Probably implies not using (helper) methods in invariants - simple expressions only( but see 4))

3) Yes redundant call - unnecessary but not fatal
Could be partially addressed by only having a single guard (protected) on lowest (cobra defined) baseclass out of core libraries rather than current guard on each instance.

(tried, tested and seems to work
gives

end init of Base
helper invariant of Base (_m1)
end init of Derived
helper invariant of Base (_m1)
helper invariant of Derived (_m2)

)

We dont mark cobra declared source (or expose the guard) so this would still generate redundant calls on derived classes based on cobra defined classes used from a library - somewhat better but not 100%

4) Yes - similarly problematic to calling overridable (helper) methods from constructors.
This could probably be addressed by allowing developers to optionally mark methods as outside invariant checking - e.g. with an attribute ('NoInvariantCheck' say) - this would also address invariant method helpers as 2) above.

[hopscc]

Change to single cobra baseclass guard.
Add a NoInvariantCheck attribute and code handling to use it

[hopscc]

Patch to provide and support an Attribute (renamed to SuppressInvariantChecks(attribute) from above) that allows suppression of invariant checks inserted on methods.
Use on invariant helper methods and constructor/initializer helper methods called before the invariants have been established.

2 test cases pinning current behaviours (invariants called on all methods) and ability to suppress invariant checks on marked methods.

I left off the change that pushes the guard to the lowest baseclass in the inheritance hierarchy ( tho the commented code is in the patch) - I suspect it would be incorrect (not called) with nested methods/helpers ( tho this may actually be more desirable) and the same capability can be done explicitly with the SuppressInvariantCheck method tagging - see the test case..

[Charles]

bump