Version 11 (modified by Charles, 12 years ago) |
---|
Contracts
Cobra supports contracts which are expressed through lists of assertion expressions
(must-evaluate-true) attached to objects and methods (and properties).
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.
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
<conditional-expr> implies <assertion-expr>
e.g.
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.
They check or constrain the state of the current object and/or the state and values of any arguments.
Keyword is require
e.g.
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.
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.
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).
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
... .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 How To Declare Contracts
See Also
- Cobra's contracts are primarily designed after Eiffel.
- Design by contract at Wikipedia