/*
	Vector
*/

data type Vector

|[
	const DIM : int
	var Coord : array[] of double    // aquí guardamos las coordenadas
  // const epsilon=3S

{inv ((DIM > 0) /\ (length(Coord,0) = DIM))}  // aseguramos que solo permitimos vectores de dimensión 3

   fun MakeVector : (in dim: int, in Value : array[] of double) -> Vector  {pre dim > 0 /\ length(Value,0) = dim}
     {post true }
      = Vector(dim, Value)

   fun MakeVector3 : (in a0: double, in a1: double, in a2: double) -> Vector  {pre true}
     {post (MakeVector3.Coord[0] = a0 /\ MakeVector3.Coord[1] = a1 /\ MakeVector3.Coord[2] = a2) }
      = MakeVector(3, [a0, a1, a2])

   fun ZeroV : (in dim: int) -> Vector   {pre dim>0}
      {post (%FORALL i : 0 <= i < dim : (ZeroV.Coord[i] = 0.0)) }
      = Vector( dim, %[j : dim : 0.0]% )

   fun ChsV : (in v:Vector) -> Vector      {pre true}
     {post (%FORALL i : 0 <= i < v.DIM : (ChsV.Coord[i] = -v.Coord[i])) }
      = Vector( v.DIM, %[ j : v.DIM :  -v.Coord[j] ]% )
//      = Vector([ -v.Coord[0],-v.Coord[1],-v.Coord[2] ])      // Alternativo
   
   fun ProdEsc : (in x:Vector, in y:Vector) -> double   {pre x.DIM = y.DIM}  {post true}
      = (%SIGMA i: 0 <= i < x.DIM:  x.Coord[i] * y.Coord[i])
//      = x.Coord[0]*y.Coord[0] + x.Coord[1]*y.Coord[1] + x.Coord[2]*y.Coord[2]      // Alternativo

   fun ProdVect : (in x:Vector, in y:Vector) -> Vector   {pre x.DIM = y.DIM}
      {post ProdEsc(x,ProdVect) = 0.0 /\ ProdEsc(y,ProdVect) = 0.0}
      = Vector( x.DIM, %[ i : x.DIM : x.Coord[(i+1) mod x.DIM] * y.Coord[(i+2) mod y.DIM] - x.Coord[(i+2) mod x.DIM] * y.Coord[(i+1) mod y.DIM] ]% )
//      = Vector( [x.Coord[1]*y.Coord[2] - x.Coord[2]*y.Coord[1],
//                  x.Coord[2]*y.Coord[0] - x.Coord[0]*y.Coord[2],
//                  x.Coord[0]*y.Coord[1] - x.Coord[1]*y.Coord[0] ] )      // Alternativo

   fun Modulo : (in v:Vector) -> double   {post Modulo >= 0.0}
      = sqrt(ProdEsc(v,v))
//      = sqrt(%SIGMA i: 0 <= i < v.DIM: v.Coord[i]*v.Coord[i])      // Alternativo
//      = sqrt(v.Coord[0]*v.Coord[0] + v.Coord[1]*v.Coord[1] + v.Coord[2]*v.Coord[2])      // Alternativo

   fun MultEscV : (in e:double, in v:Vector) -> Vector    {pre true}  
      {post (%FORALL i : 0 <= i < v.DIM : (MultEscV.Coord[i] = e * v.Coord[i])) }
      = Vector( v.DIM, %[ j : v.DIM : e * v.Coord[j] ]% )
//      = Vector( v.DIM, [ e * v.Coord[0], e * v.Coord[1], e * v.Coord[2] ] )      // Alternativo

   fun NormalizeV : (in v:Vector) -> Vector   {pre true}  {post true}
      = MultEscV (1.0/Modulo(v), v)
      
   fun SumaV : (in x:Vector, in y:Vector) -> Vector    {pre x.DIM = y.DIM}  {post true}
      = Vector( x.DIM, %[i : x.DIM :  x.Coord[i] + y.Coord[i] ]% )
//      = Vector( [x.Coord[0] + y.Coord[0], x.Coord[1] + y.Coord[1], x.Coord[2] + y.Coord[2]] )      // Alternativo
   
   fun RestaV : (in x:Vector, in y:Vector) -> Vector    {pre x.DIM = y.DIM}  {post true}
      = SumaV(x, ChsV(y))
//      = Vector( %[i : v.DIM :  x.Coord[i] - y.Coord[i] ]% )      // Alternativo
//      = Vector( [x.Coord[0] - y.Coord[0], x.Coord[1] - y.Coord[1], x.Coord[2] - y.Coord[2]] )      // Alternativo
   
   fun IgualV : (in x:Vector, in y:Vector) -> boolean    {pre x.DIM = y.DIM}  {post true}
      = (%FORALL i : 0 <= i < x.DIM : (x.Coord[i] = y.Coord[i]))
//		= (Modulo( RestaV( x, y)) = 0.0 )    // Alternativo
//      = ( x.Coord[0] = y.Coord[0] /\ x.Coord[1] = y.Coord[1] /\ x.Coord[2] = y.Coord[2] )    // Alternativo

   proc printVector : (in msg:String, in v:Vector)   {pre true}  {post true}   |[
	  write(msg + " [ " + v.Coord[0] + (%SIGMA j: 1 <= j < v.DIM : ", " + v.Coord[j]) + " ]" )
//      write(msg + " [ " + v.Coord[0] + ", " + v.Coord[1] + ", "+ v.Coord[2] + " ]")   // Alternativo
   ]| 
   
/*
   meth showme:(in msg:String)   {pre true}  {post true}   |[
      write(msg + " [" + Coord[0] + ", " + Coord[1] + ", "+ Coord[2] + "]")
   ]| 
*/
	  
/*******************************************
************** Casos de Prueba *************
*******************************************/

/*
   var V1 := ZeroV(3) : Vector;
   printVector("V1 = ", V1);

   V1 := MakeVector3(1.0, 2.0, 1.0);
   printVector("V1 = ", V1);
   
   var V2 := MakeVector3(-1.0, 2.0, 3.0) : Vector;
   printVector("V2 = ", V2);
   
   var V3 := SumaV(V1, V2): Vector;
   printVector("V3 = ", V3);
   
   var V4 := MultEscV(1.0/Modulo(RestaV(V1, V2)), RestaV(V1, V2)): Vector;
   printVector("V4 = ", V4);
   
   write(Modulo(V4));
   
   write ("V4 · V5 = " + ProdEsc(V4,V3));
   
   printVector("V4 x V4 = ",ProdVect(V4,V4));
   
   skip
*/

]|