spec module Util { 
  proc sign(a:float;b:float) returns rv:float ensures true;
}