Return commands leave a procedure and resume past the command that called it.
A Return is required as the last command in a procedure body, an
postcondition <Command Block> return
A Postcondition consists a block of commands to be run when exiting a procedure. It is intended to be used to free any resources allocated within a the procedure. The Postcondition is run when leaving a procedure either by the primary return or while processing an exception. That can include the Return command in an exception handler or when the procedure is unwound while processing an exception in a called procedure. Only one Postcondition block can be declared in a procedure in conjunction with the primary Return.
Commands within a Postcondition block should not raise exceptions. If that does happen, a Double Exception Fault will be raised. Any procedures called from a precondition block must be declared as Pure. Remember that Fault Assertions can be raised anywhere at any time. If a Fault occurs in a Postcondition block then control is passed to the Fault handler if present.
Should a double Fault (Fault.Retry) occur within a Postcondition the system is considered to be in a corrupt state. Usually a resource to be released by the Postcondition may not have been properly managed. A Fault tolerant system will need to compensate for resource corruption after a double Fault.
Postconditions came from logic programming in which logic rules satisfy a set of paired precondition and postcondition states. When the precondition state is met the postcondition state is established. In procedural programming executable commands in the body of the procedure establish the postcondition state. This differs from postconditions used in software testing to perform integrity checks.
At the end of an exception handler the return command can also have an operand, Raise, to continue unwinding the exception. Without it the handler returns to the caller and resumes the program.
return [raise]
Trace Variables
