Changes between Version 7 and Version 8 of Methods

Timestamp:

01/08/13 00:30:03 (12 years ago)

Author:

hopscc

Comment:

--

Methods

@@ -97 +97 @@
 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.
+In addition to the body, a methods contents may also include optional contracts specifications [[BR]]
+(pre method entry prerequisite conditions and post method exit postconditions ) and/or 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]]
+(see wiki:Contracts for an expanded description)
+
 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.
+If tests or contracts are specified and any of these are indented clauses[[BR]]
+(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)[[BR]]
+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