Behavioral constraints -- signature versus assertions

• $f(x:9..11)\; :\; 3..5\; \{\; ...\; \}$

    int f(int x) {
       require( 9 <= x  && x <= 11 );
       ...
       promise( 3 <= result && result <= 5);
       return result;
       }