= 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 '''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. 
{{{ 
#!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]