// vectors are always valid, since they just contain floats
// the important part of this spec is that nothing is ever
// modified.  specifying algebraic invariants would just be
// tantamount to repeating oneself between the code and the spec...
spec module Vec {
  format P;

  proc clear(v:P) ensures true;
  proc unit(v:P) ensures true;
  proc add(v:P; r:P) ensures true;
  proc sub(v:P; r:P) ensures true;
  proc load(v:P; r:P) ensures true;
  proc store(v:P; r:P) ensures true;
  proc div(v:P; r:P) ensures true;
  proc prod(v:P; r:P) ensures true;
  proc scale(v:P; s:float) ensures true;
  proc dotProd(v:P; r:P) returns rv:float ensures true;
  proc crossProd(u:P; w:P; r:P) ensures true;
  proc min(v:P; r:P) ensures true;
  proc max(v:P; r:P) ensures true;
  proc norm(v:P) returns rv:float ensures true;
  proc squareNorm(v:P) returns rv:float ensures true;
  proc getX(v:P) returns rv:float ensures true;
  proc getY(v:P) returns rv:float ensures true;
  proc getZ(v:P) returns rv:float ensures true;
  proc setX(v:P; x:float) ensures true;
  proc setY(v:P; y:float) ensures true;
  proc setZ(v:P; z:float) ensures true;
  proc get(v:P; d:int) returns q:float ensures true;
  proc setV(v:P; d:int; val:float) ensures true;
  proc shiftAxis(v:P; i:int; e:float) ensures true;
  proc print(v:P) ensures true;
}