// again, no object manipulation here
// we'd be tempted to put algebraic (numerical?) invariants here...

spec module Acc_double {
  proc readval() returns d:float ensures true;
  proc writeval(d:float) ensures true;
  proc addval(d:float) ensures true;
}