Object invariants

[gbluma]

I got sidetracked and ended up working on this for a bit today. Creating a github ticket now so I can refer back to the commits here.

The situation is the following: We want to be able to check invariants at various times to ensure that the object is well-behaved. The times include: after construction, after modification, and possibly others.

Here's a simple example of an invariant format. x in this case should always be above 0. In particular, after construction and after setting the value. This is handled internally using assert, so if it fails to match correctly, that kills the program. Fail early, fail often.

object Foo(x:int) = {
    invariant x > 0;
    proc setX(x2:int) = { x = x2; }
}

This should still work, even though the invariants are curried across multiple blocks.

object Foo(x:int)(y:int) = {
    invariant x > 0;
    invariant y > 0;
    proc setXY(x2:int, y:int) = { x = x2; y = y2; }
}

Some problems to consider:

• [x] Functions with signatures like (x:int)(y:int) can't check both invariants on the first curried form.
• [x] Invariants need to propagate to the methods.
• [x] Ensure invariants get propagated right at each stage of currying
• [ ] Fix outstanding bug where constructor pre-checks aren't asserted
• [x] Tests
• [ ] Documentation

[gbluma]

Current status is a little confusing:

Source code:

object B(x:int)(y:int) = {
  invariant x > 0;
  invariant y > 0;
  method fun getX() => x;
}

println$ (B(-2)(-1)).getX();

ubuntu@gb1:~/felix$ flx oinv2.flx 
inner_bind_expression: SimpleNameNotFound binding expression (land ((land ((case 1 of bool), (> (y, 0)))), (> (x, 0))))
Inner bind expression failed binding (land ((land ((case 1 of bool), (> (y, 0)))), (> (x, 0))))
SIMPLE NAME y NOT FOUND ERROR
In /home/ubuntu/felix/oinv2.flx: line 11, cols 1 to 2
10:   method fun getX() => x;
11: }
    **
12: 

Routine: inner_lookup_name_in_env

What this means, is that it can't find y when it's trying to check invariants on the first constructor. I might need to approach this from a different angle.

[gbluma]

Invariants are actually a bit of an odd duck because we already have a different feature that works better for handling inputs. Preconditions can be assigned to a particular part of a closure with the when keyword. This is better suited to the problem above, but doesn't work check changes after processing.

object C
  (var x:int when x > 0)
  (var y:int when y > 0) =
{
  method proc setX(x2:int) { x = x2; }
  method fun getX() => x;
}

var c = C(3)(3);
c.setX(0);  // works, but shouldn't be allowed
println$ c.getX();  // Outputs 0

I don't think it will work to scan through the invariants and figure out which closure they belong to. Even the scanning and statement manipulation we do already seems uglier than it needs to be.

[skaller]

Invariants apply to the object state. Therefore they are children of the object constructor. The constructor in a curried function is the innermost function of the nested functions. The invariant can be added to the post-conditions (expect clause) of that function.

The when clause doesn't work because Felix cheats and makes a wrapper function that checks it. It looks like the exported method is of the original function, instead of the wrapper. I suspect the same for post-conditions. Not sure.

[skaller]

Some problems to consider:

• Functions with signatures like (x:int)(y:int) can’t check both invariants on the first curried form.

For the constructor, of course they can’t, the object doesn’t exist yet!

It’s tricky! The expect post-condition only applies to the return value which is just a record and cannot have any invariants that do not relate the methods.

So the invariant will have to be inserted just before the return statement.

Actually the invariant refers to the private state of the object NOT to the public interface. That can be handled with post-condition of the constructor.

— john skaller skaller@users.sourceforge.net http://felix-lang.org

[gbluma]

I think the solution is going to to be to propagate the preconditions into the postconditions (for objects only) and for the lifetime of the object. Doing this will solve the locality issue for invariants on params while still being able to treat it as an invariant.

I have this almost working. Just needs some tweaks to get the precondition invariants lined up with the curry--one per curry, as opposed to all or nothing. (The current mode is /all/.)

The following works.

object C
  (var x:int when x > 0)
  (var y:int when y > 0)
  =
{
  invariant x > 1;
  method proc setX(x2:int) { x = x2; }
  method proc setY(y2:int) { y = y2; }
  method fun getX() => x;
}

var c = C(3)(3);
c.setX(2);  
c.setY(0); // triggers the invariant error   
println$ c.getX();

[gbluma]

Oops. That example is almost working. It complains about 'y' not being named because I globbed all of the preconditions together into one check.

I added another change to avoid breaking the build.

[gbluma]

All fixed now. Just need to add some tests and docs for future support, then it's done.

Also, feeling pretty chuffed that I can rework the currying code now. Seemed like a huge ball of yarn for months and months.