Changes between Version 6 and Version 7 of Methods

Timestamp:

01/08/13 00:20:29 (12 years ago)

Author:

hopscc

Comment:

clarify syntax requirements for method tests, contracts and body

Methods

@@ -94 +94 @@
  * Enumerator '''enumerate''' enumerate as T*
 
+== Method Body ==
+A method body is the code that implements the methods actions or behaviour.[[BR]]
+
+In addition to the body, a methods contents may also include optional contracts specifications (pre method entry prerequisite conditions and post method exit postconditions )and optional Test clauses.
+
+Contract prerequisites are tagged with the keyword suffix '''require'''. [[BR]]
+Postconditions are suffixed with keyword '''ensure'''.[[BR]]
+Both of these may be a single expression (on the same line as keyword) or an indented clause on line following the keyword.[[BR]]
+Tests are always in an indented clause following the '''test''' suffix keyword.
+
+Inherited methods may augment contracts provided on ancestor methods.[[BR]]
+Prerequisites may be relaxed, postconditions can only be increased (??). [[BR]]
+Such augmentation is noted by an extra leading suffix :[[BR]]
+giving '''or require''' for preconditions, '''and ensure''' for postconditions[[BR]] 
+otherwise contracts on submethods replace any contracts on ancestor methods.
+
+If tests or contracts are specified and any of these are indented clauses (i.e if any tests are given (always in an indented clause) or single or multiple prerequisite or postcondition  expressions are given (in an indented clause) then the method body ''must'' also be tagged with the keyword suffix '''body''' and the method body code placed in a following indented clause.
+
+Examples
+ 
+{{{
+#!cobra
+def simpleBump(i as int) as int
+   require i >0  # prerequisite contract - single expression
+   .counter += 1 # method body starts here - not indented 
+   .val += i
+   return .val     
+
+def simpleBump(i as int) as int
+   require i >0            # prerequisite contract - single expression
+   ensure .val > old .val  # postcondition contract - single expression
+   .counter += 1           # method body - not additionally indented
+   .val += i
+   return .val     
+
+def simpleBump(i as int) as int
+   test          # unit test clause
+       a = Inst()
+       assert a.counter == 0
+       assert a.val == 0
+       a.simpleBump(1)
+       assert a.counter ==1
+       assert a.val == 1
+   body            ##method body - tagged and additionally indented
+      .counter += 1 
+      .val += i
+      return .val     
+
+
+def simpleBump(i as int) as int
+   require  # prerequisite contract - in indented clause (1 or many expressions)
+      i >0               
+   body       # method body must be tagged and indented
+      .counter += 1
+      .val += i
+      return .val     
+
+# this emits a syntax error - method body must be tagged and indented
+def simpleBump(i as int) as int
+   require  # prerequisite contract - in indented clause (1 or many expressions)
+      i >0               
+   .counter += 1 #method body - not additionally indented
+   .val += i
+   return .val     
+}}}