Proposal: Implementing contracts in Boo

time to read 12 min | 2298 words

(This is a suggestion I'm making for the Boo's mailing list, about a proposed syntax for Eiffel's like contracts for Boo)

[This proposal require inherited Ast attributes, which provides some challanges in the implementation. More on this in a moment.]

The idea is to allow to use attribute markup to create pre & post conditions for a method. Here are the sematics or this proposal:

  • Pre conditions apply to the current method and all the method that override it:
    • Considerring that difficulities in checking in compile time that a class accept equal to or wider range of parameters (rather than a narrow range) I don't think that this practical.
    • It's not hard to implement this check in run time where you can ensure that if the base method pre condition has passed then the method must accept it or violate its contract. So this what this proposal does. An exception (with very silly name) is raise if a parent's base condition is satisfied but the child condition has failed.
  • Post conditions apply to the current method and all the methods that override it:
    • Again, statically checking the correctness of the post condition is prohibitive, and much simpler to do on run time.
    • Post conditions are stacked, and a post condition that allows something that the base method wouldn't allow will cause a contract exception

Without further ado, here is the proposed code and the final translation (see more comments about the implementation below):

public class ClassWithContract:     
#post & pre are Inherited AstAttributes
[post(PerformComplexVerification(result))]
virtual def FirstMethod([pre(foo.Property == "object")]foo as someType) as anotherType:
return DoWork(arg)
public class DerivedClassWithNoOverridingContract(ClassWithContract):     
override def FirstMethod(foo as someType) as anotherType:
return DoDerivedWork()
public class DerivedClassOverrideContract(ClassWithContract):     
[post(PerformValidationForDerived(result)]
override def FirstMethod([pre(foo.Property is not null)] foo as someType) as anotherType:
return DoDerivedWork2()

The above would be translated into the following:

public class ClassWithContract:     
protected virtual def post_FirstMethod(result as anotherType) as bool:
return PerformComplexVeriication(result)
    # the syntax for this is pre_<method name>_<arguments>_<arguments this method check>     
# this is done in order to handle overloading
protected virtual def pre_FirstMethod_someType_arg(foo as someType) as bool:
return foo == "object"
    # this attribute is check by the ocmpiler and if found it will invoke the specified     
# attribute on any overloading method and then apply to it the same AST attribute
[InheritorUseAstAttribute("Boo.Lang.Useful.PostAttribute, Boo.Lang.Useful")]
[InheritorUseAstAttribute("Boo.Lang.Useful.PreAttribute, Boo.Lang.Useful")]
virtual def FirstMethod(arg as someType) as anotherType:
raise PreConditionFailedException("arg") if not pre_FirstMethod_someType_arg(arg)
__result = DoWork(arg) raise PostConditionFailedException() if not post_FirstMethod(__result)
return __result
public class DerivedClassWithNoOverridingContract(ClassWithContract): 
    # pre condition of base method is enforced     
# post condition is enforced
# this doesn't have any special pre/post condtions of its own
override def FirstMethod(foo as someType) as anotherType:
raise PreConditionFailedException("arg") if not pre_FirstMethod_someType_arg(arg)
__result = DoDerivedWork()
raise PostConditionFailedException() if not post_FirstMethod(__result)
return __result
public class DerivedClassOverrideContract(ClassWithContract): 
    # override the parent post condition and then call it:     
protected override def post_FirstMethod(result as anotherType) as bool:
currentCondition = PerformComplexVeriication(result)
baseCondition = super(result)
raise ContractViolationChildDontAcceptSuperDoesException() if currntCondition
and not baseCondition

return currentCondition
 protected override def pre_FirstMethod_someType_arg(foo as someType) as bool:     
baseCondition = super(foo)
currentCondition = foo .Property is not null
# need to work on the name of this exception :-)
raise ContractViolationChildDontAcceptSuperDoesException() if baseCondition and not currentCondition
return currentCondition
    [InheritorUseAstAttribute("Boo.Lang.Useful.PostAttribute, Boo.Lang.Useful")]     
[InheritorUseAstAttribute("Boo.Lang.Useful.PreAttribute, Boo.Lang.Useful")]
override def FirstMethod(foo as someType) as anotherType:
raise PreConditionFailedException("arg") if not pre_FirstMethod_someType_arg(arg)
__result = DoDerivedWork2()
raise PostConditionFailedException() if not post_FirstMethod(__result)
return __result

A few comments about the proposal:

  • Adding a class invariant would be a very simple matter if we take this approach
  • Setting a contract for an interface may be problematic, since there is no place to put the methods, in this case I propose that a utility class will be created and used by all the classes that implement the interface.
  • What happen when a post/pre condition raise an exception?
  • I don't like the idea of easing the limitation, or of not implementing the contract exception. The reasoning is very simple, right now a post / pre condition need to takes into account each and every parent's condition. I suggest that we would simply stack them together, and if any fail the Pre/Post condition exception would be raised, without checking for the correctness of the contract.
  • How do you debug this?
  • How do you get the contract from a compiled dll so you would know what it is? Do we rely on documentation or should we live something in the IL to be read later?

What is needed to implement this?

Not much, actually :-) which is very good. I played with my mind a little with this and this is what is needed to create this proposal:

  • An abstract attribute (AbstractInheritedAstAttribute) that inherit from AbstractAstAttribute that will handle inheritance to overriding methods (or derived class, if we wants class invariants as well). This attribute will "tag" any method/class that it is used upon with a normal attribute (in the sample InheritorUseAstAttributeAttribute which will have the full type name of the Ast attribute.
  • Adding a compiler step that will process any method/class that has this attribute in their parentage chain and call the Ast attribute on the current memeber.

[This is a rough draft that was mainly formulate during IRC discussion early this morning.]