How To Declare Contracts
Print Hello World
Write Basic Syntax
Use Properties
Make An If Else Ladder
Make A Branch Statement
Declare Inits
Use Lists
Use Arrays
Make A Class Hierarchy
Use Nil And Nilable Types
Use Dynamic Typing
Declare Variable Number Of Args
Read And Write Files
Check Inheritance And Implementation
Customize Object Equality
Pass References To Methods
Translate Pseudo Code To Cobra 1
Translate Pseudo Code To Cobra 2
Implement IEnumerable 1
Implement IEnumerable 2
Iterate Through Recursive Data With Yield
Make A Collection Class
Declare Contracts
Threads
Win Forms
WPF
GTK
Qyoto
Access MySQL
XNA
Open TK
 
"""
Cobra supports contracts which are expressed through lists of truthful
expressions attached to objects and methods (and properties). They act as
documentation, specification and run-time assertions.

Cobra's approach to contracts is modeled directly after Eiffel.

Like the other How To's, this program demonstrates language features with
explanatory comments. It is not a practical sample.

Keywords and implicit variables related to contracts include:
    invariant, require, ensure
    result, old, implies
    or require
    and ensure

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' will show the values of 'x' and 'y'.

You may wish to turn off contracts before shipping software in order to boost
run-time performance and/or reduce executable size. From the command line, you
can turn off contracts with:
    cobra -contracts:none foo.cobra

See also a forum post on contracts:
http://cobra-language.com/forums/viewtopic.php?f=4&t=26
"""

class Entity

    # 'invariant' is followed by a list of truthful expressions
    # These are executed at the end of each code member (initializer, method,
    # property, etc.). They speak to the state of the object.
    invariant
        .serialNum >= 1000
        .name.length > 0
        .actionCount >= 0

    cue init(serialNum as int, name as String)
        require
            serialNum > 0
            name.length > 0
        body
            base.init
            _serialNum = serialNum
            _name = name

    get serialNum from var as int
    
    get name from var as String

    pro isActive from var as bool

    get actionCount from var as int

    def act(ctx as Context)
        require           # Requirements can speak to...
            .isActive     #   the state of the current object
            ctx.isActive  #   the state of the arguments
        ensure
            # Can refer to 'old' values in 'ensure'
            .actionCount == old .actionCount + 1
        body
            _actionCount += 1

    # Properties can have contracts too:
    get upperName as String
        ensure
            # 'result' is an implicit variable in the 'ensure' clause
            result.length == .name.length
        body
            return .name.toUpper


class Context
    """
    Dummy support class.
    """

    get isActive as bool
        return true


class Utils

    shared

        def compute(x as float, y as float) as float
            require
                x > 0
                y > 0
            ensure
                result > 0   
            body
                return x.sqrt + y.sqrt

        def compute(numbers as IList<of number>) as number
            # Overloaded methods get their own contracts independent of
            # other overloads.
            # Also the 'all' and 'any' operators can be use to check
            # conditions on a series of elements.
            require
                all for n in numbers get n > 0
            body
                return numbers.random

        def compute(s as String) as String
            # If a condition is too complex to express directly,
            # just break it out to a utility method.
            require
                .isComputable(s)
            body
                return s.toUpper

        def isComputable(s as String) as bool
            """ Returns true if ... """
            # complex logic here
            return true

        def normalizeName(name as String) as String
            # If a contract has only one condition, you can write it
            # on one line and skip 'body'.
            require name.trim.length
            ensure result.length <= name.length
            return Utils.capped(name.trim)

        def capped(s as String) as String
            """
            Returns the string with the first character capitalized.
            Returns a blank string for a blank string.
            """
            ensure
                result.length == s.length
                result.length implies result[0] == result[0].toUpper
            test
                # Unit tests can enhance contracts by showing example
                # invocations and verifying behavior.
                assert Utils.capped('chuck')=='Chuck'
                assert Utils.capped('Chuck')=='Chuck'
                assert Utils.capped('')==''
                assert Utils.capped(' foo')==' foo'
                assert Utils.capped('f')=='F'
                assert Utils.capped('1aoeu')=='1aoeu'
            body
                if s.length
                    return s[0:1].toUpper + s[1:]
                else
                    return s


class BaseClass

    def normalizeName(name as String) as String
        require name.trim.length
        return Utils.capped(name.trim)


class DerivedClass inherits BaseClass

    def normalizeName(name as String) as String is override
        # When method contracts are inherited, the 'require' can be weakened 
        # through 'or require' meaning that the DerivedClass is more flexible 
        # about what conditions the work can be done in. The 'ensure' can be 
        # strengthened with 'and ensure' meaning that DerivedClass can 
        # guarantee additional conditions about the results of the work.
        or require
            true   # take any kind of string
        and ensure
            name.trim.length == 0 implies result == '(noname)'
        body
            return Utils.capped(if(name.trim.length, name.trim, '(noname)'))


class Program

    def main
        expect RequireException
            Utils.normalizeName('')  # contract violations throw exceptions