1.8.1. Preconditions and postconditions

Functions can be given preconditions:
Start felix section to tut/examples/tut_beg107a.flx[1 /1 ]
     1: #line 307 "./lpsrc/flx_tutorial.pak"
     2: #import <flx.flxh>
     3: fun guarded_div(a:int, b:int when b!=0) =
     4: {
     5:   return a/b;
     6: }
     7: print (guarded_div(2,4)); print "\n";
     8: 
End felix section to tut/examples/tut_beg107a.flx[1]
Functions can also be given postconditions:
Start felix section to tut/examples/tut_beg107b.flx[1 /1 ]
     1: #line 318 "./lpsrc/flx_tutorial.pak"
     2: #import <flx.flxh>
     3: fun abs_div(a:int, b:int when b!=0) expect result >=0 =
     4: {
     5:   return abs(a/b);
     6: }
     7: print (abs_div(2,4)); print "\n";
     8: 
End felix section to tut/examples/tut_beg107b.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.