1.8.1. Preconditions and postconditions

Functions can be given preconditions:
Start C++ section to tut/examples/tut107a.flx[1 /1 ]
     1: include "std";
     2: fun guarded_div(a:int, b:int when b!=0) =
     3: {
     4:   return a/b;
     5: }
     6: print (guarded_div(2,4)); print "\n";
     7: 
End C++ section to tut/examples/tut107a.flx[1]
Functions can also be given postconditions:
Start C++ section to tut/examples/tut107b.flx[1 /1 ]
     1: include "std";
     2: fun abs_div(a:int, b:int when b!=0) expect result >=0 =
     3: {
     4:   return abs(a/b);
     5: }
     6: print (abs_div(2,4)); print "\n";
     7: 
End C++ section to tut/examples/tut107b.flx[1]
Note the special identifier 'result' may be used to refer to the function result.

If a pre or post condition is not met, a C++ exception is thrown. Typically this will result in a diagnostic error being printed the thread terminated by the driver. However it is driver dependent.

At present (Felix 1.1.1) recovery is not possible, nor is it possible to catch the exception.