Wiki

Changes between Version 6 and Version 7 of Methods

Show
Ignore:
Timestamp:
01/08/13 00:20:29 (11 years ago)
Author:
hopscc
Comment:

clarify syntax requirements for method tests, contracts and body

Legend:

Unmodified
Added
Removed
Modified
  • Methods

    v6 v7  
    9494 * Enumerator '''enumerate''' enumerate as T* 
    9595 
     96== Method Body == 
     97A method body is the code that implements the methods actions or behaviour.[[BR]] 
     98 
     99In 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. 
     100 
     101Contract prerequisites are tagged with the keyword suffix '''require'''. [[BR]] 
     102Postconditions are suffixed with keyword '''ensure'''.[[BR]] 
     103Both of these may be a single expression (on the same line as keyword) or an indented clause on line following the keyword.[[BR]] 
     104Tests are always in an indented clause following the '''test''' suffix keyword. 
     105 
     106Inherited methods may augment contracts provided on ancestor methods.[[BR]] 
     107Prerequisites may be relaxed, postconditions can only be increased (??). [[BR]] 
     108Such augmentation is noted by an extra leading suffix :[[BR]] 
     109giving '''or require''' for preconditions, '''and ensure''' for postconditions[[BR]]  
     110otherwise contracts on submethods replace any contracts on ancestor methods. 
     111 
     112If 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. 
     113 
     114Examples 
     115  
     116{{{ 
     117#!cobra 
     118def simpleBump(i as int) as int 
     119   require i >0  # prerequisite contract - single expression 
     120   .counter += 1 # method body starts here - not indented  
     121   .val += i 
     122   return .val      
     123 
     124def simpleBump(i as int) as int 
     125   require i >0            # prerequisite contract - single expression 
     126   ensure .val > old .val  # postcondition contract - single expression 
     127   .counter += 1           # method body - not additionally indented 
     128   .val += i 
     129   return .val      
     130 
     131def simpleBump(i as int) as int 
     132   test          # unit test clause 
     133       a = Inst() 
     134       assert a.counter == 0 
     135       assert a.val == 0 
     136       a.simpleBump(1) 
     137       assert a.counter ==1 
     138       assert a.val == 1 
     139   body            ##method body - tagged and additionally indented 
     140      .counter += 1  
     141      .val += i 
     142      return .val      
     143 
     144 
     145def simpleBump(i as int) as int 
     146   require  # prerequisite contract - in indented clause (1 or many expressions) 
     147      i >0                
     148   body       # method body must be tagged and indented 
     149      .counter += 1 
     150      .val += i 
     151      return .val      
     152 
     153# this emits a syntax error - method body must be tagged and indented 
     154def simpleBump(i as int) as int 
     155   require  # prerequisite contract - in indented clause (1 or many expressions) 
     156      i >0                
     157   .counter += 1 #method body - not additionally indented 
     158   .val += i 
     159   return .val      
     160}}}