Precondition and Postcondition

Procedures can also include preconditions; which are a set of conditions that must be met before the body of a method can be executed. They are useful for validating input parameters and the state of global variables. When writing a procedure call you can use the preconditions to understand constraints to help you set up parameters.

When a precondition fails it can either raise a fault or a managed exception. Preconditions are simply another way to raise an exception in a method.

   precondition                :Begin a precondition clause.
      Name ~= "";               ERROR:  A name was not given.
      Size > 3  fault;          FAULT:  The size must be over 3.
      Id  => 0  pass Id;        ERROR:  The ID is unknown.
   .                           :A period ends a precondition block.

There is also a postcondition construct, but note that it differs from the conventional definition. A postcondition in Gilda is a block of commands that are always executed before leaving a method; whether a normal return, after a handler has completed, or when unwinding the call stack. They help ensure that any resources are cleaned up that were aquired by a method regardless of the outcome.

   postcondition               :Begin a postcondition clause.
      Command sequence ...     :Command to execute.
   return                      :Return from the procedure.

Catch Exception

Class File