invariants and derived classes

[jonathandavid]

[Edit: I think I've found an answer to my question myself. Skip to the end of my third post to go straight to my conclusion -- Manuel]

Shouldn't the following code throw an InvariantException?

class B
    var __x = 1
    pro x from __x
class D
    inherits B
    invariant
        .x <> 0
    def main is shared
        d = D()
        d.x = 0

As you must have guessed, it does not.

I would have expected D to "override" the invariant of B, so the line "d.x = 0" checked the invariant of D, not of B as it seems to do in the current implementation.

Regards,
Manuel

[jonathandavid]

Ok, I've found a mechanism to achieve the behavior I intended:

class B
    var __x = 1
    pro x from __x
    def check as bool
        return true
    invariant
        .check
class D
    inherits B
    def check as bool is override
        return .x <> 0
    def main is shared
        d = D()
        d.x = 0

Now the invariant violation is properly discovered.

The problem is that in order to make this work I've had to modify the base class, which is not always desirable or even possible (it might be defined in a library to which I don't have access). It would be nice if Cobra could apply this mechanism automatically, so that the code I posted in my initial code would behave as the code in the current post (i.e., Cobra would implement this "overriden 'check' method" trick under the hoods).

In case the base class had its own invariant, it could be called automatically (as with the default constructor), or it could be called manually by the implementer of the derived class, using a construct like "base.invariant". Under the hoods, this would amount of course to a call to "base.check" for the compiler generated "check" method:

class B
    var __x = 1
    pro x from __x
    invariant               # This would translate to:
        __x < 100           # def check as bool
                        #   return __x < 100
                        # invariant
                        #   .check
class D
    inherits B
    invariant
            base.invariant              #  This would translate to: 
            return .x <> 0          #  def check as bool
                            #       return __x <> 100                              
                            #  invariant
                            #       base.check
                            #       .check

    def main is shared
        d = D()
        d.x = 101             
                     catch InvariantException, print 'Base invariant violation detected'
        d.x = 0
                     catch InvariantException, print 'Derived invariant violation detected'

On second thoughts I'm pretty sure that the "call" to base.invariant should be automatic, otherwise it would be too easy for a derived class to "bypass" the invariant of its base, which could be perceived as a security hole. How does Eiffel deal with this?

In the last snippet I've used the simplified catch syntax that Chuck proposed in an old post. I don't know if that's supported by the compiler already, but I have to say I like it a lot.

Regards,
Manuel

[jonathandavid]

Here's a practical example in which what I propose would be useful:

class Real
    var __value = 0f
    pro value from __value

    cue init
        pass
    cue init(v as float)
        __value = v

class PositiveReal
    inherits Real

    invariant
        .value >= 0f

    def main is shared
        x = PositiveReal()
        x.value = -1   # I'd like this to throw; it does not in current version

Anyway, I think now I understand why what I propose is not feasible: it could not be made to work when the base class is not a pure Cobra class, as in that case the "check" virtual function would not be present and the compiler would have no way to add it. That is, the above example would be possible, because the base class is a Cobra class, but it would not have been possible if "Real" was a .net framework class. I guess that's the problem of being tied to a particular object model (of course, the benefits of working on top of .NET certainly pay off).

Regards,
Manuel

[Charles]

This still feels wrong to me--meaning that I agree with your original post. Why doesn't that program throw an exception?

Yes, if your base class is a non-Cobra class then you cannot make that class check the invariants. Although you could override a virtual member to accomplish that effect.

But within Cobra, invariants are supposed to be ANDed meaning they should all be required to pass. Btw the implicit invariant of a class is the expression "true".

So looking at the generated code for your example, I see various problems:

(1) Cobra's default -contracts: option value of "inline" means that base classes will never respect the invariants of derived classes which they cannot see.

(2) Even with "cobra -contracts:methods ...", the generated code only invokes the invariants of its class and ancestor classes with no hook or virtual method for the subclasses.

(3) If (2) is fixed then (1) will still be broken. Inlined contracts would have different semantics which is unacceptable. So I think fixing (2) will also mean fixing (1) such that it does not inline the invariants (only require and ensure).

Unless I have this wrong and Eiffel does not respect invariants of derived classes in a base class' method. I mean philosophically, maybe it should not have to because the method was not designed and implemented in the context of the derived class. Anyone care to fire up their Eiffel compiler?

[Charles]

I've downloaded SmartEiffel and started banging out an example, but it's somewhat slow going as I don't know Eiffel's syntax and peculiarities. Their compiler error messages aren't particularly useful, unlike some compilers I know of.

[Charles]

I finally got the Eiffel code working and the invariant of a derived class is respected even when invoking a method ("feature" in Eiffel) in the base class. This matches my first instinct when presented with your original post, as well as yours when you encountered this.

I'm currently working on the fix.

[jonathandavid]

I've tried the same thing in Nemerle, and it doesn't work as expected. In particular, the following program does not throw an invariant exception:

Code: Select all

// THIS IS NOT COBRA CODE!!

using Nemerle.Assertions;
using System.Console;

public class Real
{
  protected mutable _x = 0.0;
 
  public set_x(x : double) : void
  {
   _x = x;
  }
}

public class Positive : Real
invariant _x >= 0.0
{
  public static Main() : void
  {
     def p = Positive();
     p.set_x(-1);
  }
}


I think this is due to the fact that DbC is still not fully implemented in Nemerle, especially the part on class invariants (they admit it their web site). Besides, they implement DbC using syntactic macros, which might keep them from being able to implement some advanced features.

I think Spec# has a much more solid DbC implementation, I will install it and see how it deals with the real/positive scenario.

BTW, having to write all those curly braces and semicolons was a real pain after getting accustomed to Cobra's syntax!

[jonathandavid]

I have downloaded and installed Spec#, but I cannot make any sense of it. There is just not enough online documentation, and the language seems complex enough and different enough from most mainstream languages to make a good deal of documentation necessary.

Anyway I'm sure my Real/Positive example would work as expected in Spec# (i.e., like Eiffel). In fact I've been reading a little bit about DbC in Eiffel and I think I understand what goes on. A class invariant is simply a postcondition that is added automatically to all methods. In derived classes, it is right to strengthen a postcondition, but it is not right to weaken it. In our class, adding the "value>=0" invariant to the derived class means that the invariant (postcondition) is being strengthen, which is as I said perfectly sound. Therefore Cobra should allow this and see that said invariant is enforced (that's way the behaviour I reported initially was indeed a bug).

On the other hand, a derived class must always have as invariant the invariant of its base class. Otherwise, the invariant (postcondition) of the base class could be easily weakened, which as I said is forbidden. This means Cobra must ensure that the invariant of a derived class is combined, or added, to the invariant of its base class.

From what I've said, I think it is clear how invariants should be implemented in Cobra (I'm sure that's how they're implemented in Eiffel too). The following code:

class A
   var _x = 0
   invariant
       _x >= 0

class B inherits A
   var _y = 10
   invariant
      _y >= 10
      _x < 100

should be translated to:

class A
   var _x = 0

   def invariant_impl as bool 
       return _x >= 0
   
   invariant                   # will be checked at the end of each method
       .invariant_impl
       

class B inherits A
   var _y = 10

   def invariant_impl as bool is override
        if not base.invariant_impl
              return false
        return _y >= 10 and _ 
                  _x < 100

When things are implemented this way, it is easy for a derived class to strengthen the invariant of its base class (see how B adds the condition x < 100), which is perfectly fine. In addition, thanks to the implicit call to the base class version of "invariant_impl", it is impossible to weaken the invariant of the base class, which would be dangerous.


Chuck: I'm sure this is all obvious to you. Also, you've probably already implemented things this way (you said you were already fixing the problem reported in my initial post). However, I felt I had to post my conclusions here, as they might be useful for people that visit this thread in the future.

I'm still concerned about the mix of non-Cobra classes and invariants. Maybe a Cobra class that inherits a non-Cobra class should not be allowed to use any base class fields in its invariant, as that would lead to things not working as expected. Consider for example:

class C inherits List<of int>
    invariant .count == 0

    def main is shared
        c = C()
        c.add(1)      # breaks the invariant but nothing happens, because the base class is not "DbC aware"

What I propose is that the compiler detects this problematic situation, and rejects the code with a message along the lines of "Error: inherited member .count cannot be used in the invariant of derived class C, because base class List<of int> is not a pure Cobra class".

[Charles]

Well the situation for providing the fix became quite complex. Making the invariant a virtual method that subclasses could override, invoke base and add more conditions too is indeed the route I went. But we have a problem with initializers. The following pre-existing test case in Cobra fails:

class A

    invariant
        .x > 0
        .name.length
    
    var _x as int
    
    def init
        _x = 1

    pro x from var
    
    get name as String
        return .getType.name

    def violateX
        _x = 0


class B
    inherits A

    invariant
        .y > 0

    var _y as int
    
    def init
        _y = 1

    get y from var

    def violateY
        _y = 0

    def violateBaseClassInvariant
        _x = 0


class Test

    def main is shared
        a = A()
        expect InvariantException
            a.violateX
        a = A()
        expect AssertException  # The ancestor class to InvariantException
            a.violateX
        expect InvariantException
            a.x = -1  # .x is a "from var" decl

        b = B()
        expect InvariantException
            b.violateX
        b = B()
        expect InvariantException
            b.violateY
        b = B()
        expect InvariantException
            b.violateBaseClassInvariant

The run-time exception is:

>cobra -debug e

Unhandled Exception: Cobra.Lang.InvariantException:
sourceSite = C:\Documents and Settings\Chuck\My Documents\Projects\Cobra\Workspace-Misc\Source\e.cobra:25 in B.invariant for objec
meType)
info = nil
this = B (RuntimeType)
(.y > 0) = false
.y = 0

at B._ih_invariant() in c:\Documents and Settings\Chuck\My Documents\Projects\Cobra\Workspace-Misc\Source\e.cobra:line 25
at A..ctor() in c:\Documents and Settings\Chuck\My Documents\Projects\Cobra\Workspace-Misc\Source\e.cobra:line 9
at B..ctor() in c:\Documents and Settings\Chuck\My Documents\Projects\Cobra\Workspace-Misc\Source\e.cobra:line 29
at Test.Main() in c:\Documents and Settings\Chuck\My Documents\Projects\Cobra\Workspace-Misc\Source\e.cobra:line 53


The problem is that "BaseClass.init" will invoke the invariant which will fail because "SubClass.init" has not completed. Normally this is easy to solve by having a int object var used as a guard. You can inc at the top of SubClass' method and dec it at the bottom, plus you wrap calls to the invariant with a guard that the var == 0. However, the problem is that C# will not allow *any* code at the top of a constructor except the invocation of another constructor (this or base). (I verified that the VM does not have this restriction so when we move to byte code some day, we will not be affected.)

Is there any other way to solve this? Yes, you can examine the .NET stack. Unfortunately, doing so makes programs over 10 X slower. When I produced a new cobra.exe with the stack examination approach, running "cobra hello.cobra" took > 12 seconds.

We may have to live with imperfect invariants until a later date. They don't completely disrespect inheritance, they just don't support every test case they should.

I've yet to determine if/how I want to clean up my existing enhancements and check them in. I can break one invariant test case or another...

[jonathandavid]

Wouldn't the problem be solved if we make the call to invariant_impl non-polymorphical in constructors? This way your class "A" above would translate to:

class A
    def invariant_impl as bool
        return .x > 0 _
             and .name.length

    var _x as int

    def init
        _x = 1
        assert A.invariant_impl        # compiler generated invariant check. Notice we get rid of 
                                                  # polymorphism by explicitly saying we want A's version of the method
     # ...

    def violateX
        _x = 0
        assert .invariant_impl         # compiler generated invariant check. Notice that this one IS polymorphical,
                                                  # because we are not inside a constructor

Does that make any sense?