= Contracts = Cobra supports contracts which are expressed through lists of assertion expressions (must-evaluate-true) attached to objects and methods (and properties).[[BR]] They act as documentation, specification and run-time assertions and should be viewed as part of the public interface of the items they are associated with. When a contract condition fails, an exception is raised.[[BR]] The exception message shows the value of each subexpression in the condition, just like the Cobra 'assert' exception. For example, 'x > y' failing will show the values of 'x' and 'y': {{{ Unhandled Exception: Cobra.Lang.RequireException: sourceSite = demo.cobra:5 in Demo.subtract for object Demo info = nil this = Demo (x > y) = false x = 3 y = 6 }}} You can turn off contracts when building shipping software in order to boost run-time performance and/or reduce executable size via the -contracts compiler switch. == Boolean Expressions == Cobra gives '''and''' and '''or''' equal precedence, therefore requiring explicit parentheses for expressions that use both operators but need an order of evaluation other than simple left to right. This is in contrast to boolean logic notation and most other programming languages, so bear this in mind when writing your preconditions, postconditions and invariants. == Keywords == Class instance invariants are specified as part of the class definition and use the keyword '''invariant'''. Code member preconditions are specified on the code member and use the keyword '''require'''. Code member postconditions are also specified on the code member and use the keyword '''ensure'''. == Implicit variables related to contracts == To make writing contracts easier some implicitly declared variables are available for use in expressions within contracts: * '''result''' - available in '''ensure''', provides a fixed name for the return value of any method or property * '''old''' - available in '''ensure''', provides an object reference that captures the original state of the expression before the method/property executed. Use to validate a state change. In addition, there is a boolean operator commonly used in contracts: * '''implies''' - available in all contracts. allows an assertion to be triggered only if a condition is true. Grammar is implies e.g. {{{ #!cobra result.count implies result[0].length # non 0-length list item old.value implies old.value < .value # value non zero and increased }}} == Preconditions == Preconditions (requirements) are assertion expressions (expressions must evaluate true) which can be placed on methods and properties.[[BR]] They check or constrain the state of the current object and/or the state and values of any arguments. Keyword is '''require''' e.g. {{{ #!cobra def sqroot(i as int) as float require i > 0 body ... def fraction( numer as int, denom as int) as float require numer > 0 denom <> 0 body ... }}} == Postconditions == Post conditions (guarantees) are also assertion expressions (must evaluate true) and can also be placed on methods and properties.[[BR]] They check/assert/assure the state of the current object or intended state change and/or the state and value of any result. Keyword is '''ensure''' e.g. {{{ #!cobra def sqroot(i as int) as float ensure result > 0 body ... def bumpState( incr as int) as int require incr > 0 ensure result >= incr .state = old.state + incr body .state += incr return .state }}} == Object State == The 'invariant' keyword leads a clause within a class definition and is followed by a list of assertion expressions (must evaluate true).[[BR]] These are executed at the end of each code member (initialiser, method, property, etc.). They speak to the state of the object. Keyword is '''invariant''' == Other == Assertions can be sprinkled through the bodies of code members to verify intermediate state or values of local variables. e.g {{{ #!cobra ... .new = .old + incr assert .new > .old }}} == Inheritance == When code member contracts are inherited (and overridden), the preconditions/requirements ('''require''') can be augmented through an '''or require''' clause meaning that the derived class is more flexible about what conditions the work can be done in. Similarly postconditions ('''ensure''') can be strengthened with an '''and ensure''' clause meaning that the derived class can guarantee additional conditions about the results of the work. Or in other words, an overriding method in a derived class: * Can ''weaken'' the precondition/requirement, but not strengthen it. * Can ''strengthen'' the postcondition/ensurement, but not weaken it. to-do: more explanation and examples are needed here See also ticket:280 for a faux bug report that didn't take into account the rules on inheritance and contracts. In comment #3 is more detailed explanation of what's going on. == Compiler Command Line == The -contracts commandline switch controls contracts code generation: values are * none - suppress contracts code generation entirely * inline (default) - place contracts code inline to the item the contract is associated with * method - place contracts code in a separate method and provide a method call from the associated item Turn off contracts with cobra -contracts:none ... == Grammar == {{{ require BODY ensure BODY invariant BODY }}} If a contract has only one condition, you can write it on one line and skip 'body'. {{{ require EXPR ensure EXPR invariant EXPR }}} == Examples == see !HowTo file [http://cobra-language.com/how-to/DeclareContracts/ How To Declare Contracts] == See Also == * Cobra's contracts are primarily designed after [http://www.eiffel.com/developers/design_by_contract.html Eiffel]. * [http://en.wikipedia.org/wiki/Design_by_contract Design by contract] at Wikipedia