Use proc macros for specifications

[ranjitjhala]

Would be rather nice to be able to write stuff like

#[flux]
fn assert(b:bool[true]) {}

#[flux]
fn inc(x: &mut i32{v:0<=v}) {
    *x += 1
}

#[flux]
fn inc(x: &mut i32[v]) ensures x: i32[v+1] {
    *x += 1
}

#[flux]
fn dist(x: &Point[@n], y: &Point[n]) -> f32 {
  let mut res = 0.0;
  for i in range(0, x.len()) {
    let di = x[i] - y[i];
    res += di * di;
  }
  res
}

#[flux]
fn inc(x: &mut i32{v:0 < v})
{
    *x += 1
}

#[flux]
fn kmeans(n: usize, mut centers:RVec<Point[n]>[@k], points: RVec<Point[n]>) 
   requires 0 < k 
{
  for _ in 0..100 {
    let point_centers = mr::map(&points, |x| nearest(&centers, x));
    let center_clusters = mr::group(point_centers);
    let weighted_centers = mr::reduce(center_clusters, |p1, p2| centroid(p1, p2));
    for (i, (x, w)) in weighted_centers {
      centers.set(i, x.map(|xi| fdiv(*xi, w)))
    }
  }
}

### Tasks