/*@ requires 0 <= t <= 1;
  @ ensures t == 1.f ==> \result == b;
  @ ensures t == 0.f ==> \result == a;
  @ ensures \min(a,b) <= \result <= \max(a,b);
  @ assigns \nothing;
 */
float interpolate(float a, float b, float t) {
    float t2 = 1.0f - t;
    float left = a*t2;
    float right = b*t;
    return left+right;
}