flux
flux copied to clipboard
Use proc macros for specifications
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(¢ers, 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