Changes between Initial Version and Version 1 of Contracts

Timestamp:

03/20/10 12:35:52 (15 years ago)

Author:

hopscc

Comment:

--

Contracts

@@ +1 @@
+= 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'.
+
+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. 
+
+== 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.[[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.
+    {{{
+    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.
+   {{{
+    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
+{{{
+    ...
+    .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 [http://cobra-language.com/how-to/DeclareContracts/ How To Declare Contracts]
+
+