/*
  Carrol Morgan's calculator  
  7/2/2010 Kuat Dafny version
  8/22/2010 translated into Chalice
*/ 

class Calc0 {  
  var vals: seq<int>;
  
  method reset() 
    requires acc(vals);
    ensures acc(vals);
  {
    vals := [];
  }
  
  method add(x: int) 
    requires acc(vals);
    ensures acc(vals);
  {
    vals := [x] ++ vals;    
  }
  
  method mean() returns (m: int)     
    requires acc(vals) && |vals| > 0;
    ensures acc(vals);
  {
    m := total(vals)/|vals|;
  }

  unlimited function total(s: seq<int>): int
  {
    |s| == 0 ? 0 : s[0] + total(s[1..])
  }  
}



class Calc1 refines Calc0 {  
  var sum: int;
  var num: int;
  replaces vals by acc(sum) && acc(num) && sum == total(vals) && num == |vals|;

  refines reset()   
  {
    sum := 0;
    num := 0;
  }

  refines add(x: int)    
  {
    sum := sum + x;
    num := num + 1;
  }

  refines mean() returns (m: int)  
  {
    m := sum/num;
  }
}