Contract clarification

[Charles]

Cobra has support for contracts which are declared with keywords like invariant, require and ensure. The last two are used on methods and also known by the names preconditions and postconditions.

I want to clarify that contracts are considered part of the public interface of a type and they should not refer to local variables in methods. Instead, contracts refer to:
-- the state of the object
-- the arguments (especially for require/preconditions)
-- the "result" (for ensure/postconditions only)

If you want to verify something about your local variables such as "x < y" then feel free to use assert in the method's implementation.

Currently, Cobra lacks error checking for usage of local vars in contracts, but I'll be adding one soon.

If you want to read more about contracts, check out the HowTo and this forum thread which links to some reading material.

[gauthier]

Hello Chuck,

thanks for the clarification, cobra is actually the first practical language that I used with contracts, and I got it wrong (ticket 198).

I think I've some amount of unit tests to fix because I've used it as a way to separate the Assert in the AAA paradigm.

To replace that with a convinient syntax, would it be possible to support such construct:

def method
    ... method body...
    assert
       assertion1
       assertion2
       ...

instead of

def method
    ... method body...
    assert assertion1
    assert assertion2
    assert ...

[Charles]

I don't see why not. The "print" statement already supports both a single-line form and an indented form:

# single line
print to tw, 'Hi'
print to tw, 'There'

# multiline
print to tw
    print 'Hi'
    print 'There'
    obj.foo  # prints inside obj.foo will also print to tw

So it would not even be new to offer both forms for a statement.

Anyone have any comments or objections?