method Name  [pure]

 entry Parameter, ...       :Parameters that can not be modified by the Method

change Parameter, ...       :Parameters that can be modified

  exit [@]Result            :Parameters that are returned from the Method

return

A Method can have multiple Entry, Change, or Exit parameters or none. They can be listed in any order and there can be more than one of each kind. A Method can optionally be declared to be Pure. A Pure Method has restricts so that they do not have side effects.

• They cannot perform input nor output, but Trace commands are allowed for debugging.


• They cannot raise Error exceptions, however Faults can always be raised anywhere in a program. A Precondition or any Assertion command within them can only raise a fault. They cannot contain Catch exception procedures.


• They only have read access to global variables and constants. Consequently they can include Use declarations, but not Alter declarations.


• Only Functions or pure Methods and Sequences can be called from within them.