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'.

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 require and ensure, provides a fixed name for the return value of any method or property

• old - avail in ensure, provides an object reference that captures the original state of the object before the method/property executed. Use to validate a state change.

In addition there is an additional expression construct

• 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 derivedClass 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.

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