2.8.1. Preconditions and postconditions

Functions can be given preconditions:
Start felix section to tut/tutorial/tut-1.08.01-0.flx[1 /1 ]
     1: #line 415 "./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";
End felix section to tut/tutorial/tut-1.08.01-0.flx[1]
Start data section to tut/tutorial/tut-1.08.01-0.expect[1 /1 ]
     1: 0
End data section to tut/tutorial/tut-1.08.01-0.expect[1]
Functions can also be given postconditions:
Start felix section to tut/tutorial/tut-1.08.01-1.flx[1 /1 ]
     1: #line 430 "./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";
End felix section to tut/tutorial/tut-1.08.01-1.flx[1]
Start data section to tut/tutorial/tut-1.08.01-1.expect[1 /1 ]
     1: 0
End data section to tut/tutorial/tut-1.08.01-1.expect[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.