""" 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 |
How To Declare Contracts