/*@ requires y/2 <= x <= 2*y
@ ensures
@ \result == x-y
@*/
float Sterbenz(float x, float y) {
return x-y;
}
/*@ requires y/2 <= x <= 2*y
@ ensures
@ \result == x-y
@*/
float Sterbenz(float x, float y) {
return x-y;
}
::
::
::
