/* Matriz */ import Vector data type Matriz |[ const DIM : int var Coord : array[][] of double // aquí guardamos las Coordenadas {inv ((DIM > 0) /\ (length(Coord,0) = DIM) /\ (length(Coord,1) = DIM)) } // aseguramos que solo permitimos vectores de dimensión DIM fun MakeMatriz3x3S : (in a00:double, in a01:double, in a02: double, in a10:double, in a11:double, in a12: double, in a20:double, in a21:double, in a22: double) -> Matriz {pre true} {post true } = Matriz( 3, [ [a00, a01, a02], [a10, a11, a12], [a20, a21, a22] ] ) // 1ra, 2da y 3ra fila fun MakeMatriz3x3V : (in v0:Vector, in v1:Vector, in v2: Vector) -> Matriz {pre true} {post true } = Matriz( 3, [ [ v0.Coord[0], v1.Coord[0], v2.Coord[0] ], // 1ra fila, [ v0.Coord[1], v1.Coord[1], v2.Coord[1] ], // 2da fila y [ v0.Coord[2], v1.Coord[2], v2.Coord[2] ] ] ) // 3ra fila fun MakeMatrizM : (in d:int, in m: array[][] of double) -> Matriz {pre d > 1} {post true } = Matriz( d, m ) // 3ra fila fun Ident : (in dim: int) -> Matriz {pre dim > 0} {post true} // Matriz Identidad = Matriz ( dim, %[ i, j : dim, dim : (i=j) => 1.0 | 0.0 ]% ) fun ZeroM : (in dim: int) -> Matriz {pre dim > 0} {post true} // Matriz cero = Matriz ( dim, %[ i,j : dim, dim : 0.0 ]% ) fun Transpuesta : (in m: Matriz) -> Matriz {pre true} // Matriz transpuesta {post (%FORALL i,k: 0 <= i < m.DIM, 0 <= k < m.DIM : Transpuesta.Coord[k][i] = m.Coord[i][k]) } = Matriz ( m.DIM, %[ i, k : m.DIM, m.DIM : m.Coord[k][i] ]% ) fun ChsM : (in m: Matriz) -> Matriz {pre true} // Cambio Signo {post (%FORALL i,k: 0 <= i < m.DIM, 0 <= k < m.DIM : ChsM.Coord[i][k] = -m.Coord[i][k]) } = Matriz ( m.DIM, %[ i, k : m.DIM, m.DIM : -m.Coord[i][k] ]% ) fun SumaM : (in x: Matriz, in y: Matriz) -> Matriz {pre x.DIM = y.DIM} {post true} // Matriz Suma = Matriz ( x.DIM, %[ i, j : x.DIM, x.DIM : x.Coord[i][j] + y.Coord[i][j] ]% ) fun RestaM : (in x: Matriz, in y: Matriz) -> Matriz {pre x.DIM = y.DIM} {post true} // Matriz Resta = Matriz ( x.DIM, %[ i, j : x.DIM, x.DIM : x.Coord[i][j] - y.Coord[i][j] ]% ) // = SumaM ( x, ChsM(y)) // Otra manera de hacerlo fun MultM : (in x: Matriz, in y: Matriz) -> Matriz {pre x.DIM = y.DIM} {post true} // Matriz Producto = Matriz ( 3, %[ i, j : x.DIM, x.DIM : (%SIGMA k : 0 <= k < x.DIM : x.Coord[i][k] * y.Coord[k][j]) ]% ) fun MultEscM : (in e:double, in m:Matriz) -> Matriz {pre true} {post (%FORALL i,j : 0 <= i < m.DIM, 0 <= j < m.DIM : (MultEscM.Coord[i][j] = e * m.Coord[i][j])) } = Matriz( m.DIM, %[ i,j : m.DIM, m.DIM : e * m.Coord[i][j] ]% ) fun MultEscF : (in e: double, in fila: int, in m: Matriz) -> Matriz {pre 0 <= fila < m.DIM} {post (%FORALL i,j : 0 <= i < m.DIM, 0 <= j < m.DIM : (i=fila) => (MultEscF.Coord[i][j] = e * m.Coord[i][j]) | (MultEscF.Coord[i][j] = m.Coord[i][j])) } = Matriz( m.DIM, %[ i,j : m.DIM, m.DIM : ((i=fila) => e * m.Coord[i][j] | m.Coord[i][j]) ]% ) fun MultEscC : (in e: double, in col: int, in m: Matriz) -> Matriz {pre 0 <= col < m.DIM} {post (%FORALL i,j : 0 <= i < m.DIM, 0 <= j < m.DIM : (j=col) => (MultEscC.Coord[i][j] = e * m.Coord[i][j]) | (MultEscC.Coord[i][j] = m.Coord[i][j])) } = Matriz( m.DIM, %[ i,j : m.DIM, m.DIM : ((j=col) => e * m.Coord[i][j] | m.Coord[i][j]) ]% ) fun MultMV : (in m: Matriz, in v: Vector) -> Vector {pre m.DIM = v.DIM} {post (%FORALL i : 0 <= i < m.DIM : (MultMV.Coord[i] = (%SIGMA j : 0 <= j < v.DIM : m.Coord[i][j] * v.Coord[j]) )) } = MakeVector( v.DIM, %[ i : m.DIM : (%SIGMA j : 0 <= j < v.DIM : m.Coord[i][j] * v.Coord[j]) ]% ) fun Determinante : (in m: Matriz) -> double {pre m.DIM = 3} {post true} // Determinante Matriz (Solo 3x3) = ( %SIGMA k,i,j : 0 <= k < m.DIM, (k+1)mod 3 <= i <= (k+1)mod 3, (k+2)mod 3 <= j <= (k+2)mod 3 : m.Coord[0][k] * (m.Coord[1][i] * m.Coord[2][j] - m.Coord[1][j] * m.Coord[2][i]) ) // Buen Truco // = ( %SIGMA k : 0 <= k < m.DIM : m.Coord[0][k] * (m.Coord[1][(k+1)mod 3] * m.Coord[2][(k+2)mod 3] - m.Coord[1][(k+2)mod 3] * m.Coord[2][(k+1)mod 3]) ) /* fun Determinante : (in m: Matriz) -> double {pre m.DIM = 3} {post true} // Determinante Matriz (Solo 3x3) |[ // Esta es la manera usando un lazo var k:= 0: int; var det := 0.0: double; {bound 3-k} do k < 3 -> var i := (k+1) mod 3 : int; var j := (k+2) mod 3 : int; det := det + m.Coord[0][k] * (m.Coord[1][i] * m.Coord[2][j] - m.Coord[1][j] * m.Coord[2][i]); k := k + 1 od >> det ]| // Y esta la manera usando el determinante tradicional fun Determinante : (in m: Matriz) -> double {pre m.DIM = 3} {post true} // Determinante Matriz (Solo 3x3) = m.Coord[0][0] * m.Coord[1][1] * m.Coord[2][2] + m.Coord[0][1] * m.Coord[1][2] * m.Coord[2][0] + m.Coord[0][2] * m.Coord[1][0] * m.Coord[2][1] - m.Coord[0][2] * m.Coord[1][1] * m.Coord[2][1] - m.Coord[0][1] * m.Coord[1][0] * m.Coord[2][2] - m.Coord[0][0] * m.Coord[1][2] * m.Coord[2][1] */ fun IgualM : (in x: Matriz, in y: Matriz) -> boolean {pre x.DIM = y.DIM} {post (%FORALL i,k: 0 <= i < x.DIM, 0 <= k < x.DIM : abs (x.Coord[i][k] - y.Coord[i][k]) < 0.000001 ) \/ (%EXISTS i,k: 0 <= i < x.DIM, 0 <= k < x.DIM : abs (x.Coord[i][k] - y.Coord[i][k]) > 0.000001 ) } // Matriz Producto // = (%FORALL i,k: 0 <= i < x.DIM, 0 <= k < x.DIM : x.Coord[i][k] = y.Coord[i][k]) proc printMatriz:(in msg:String, in m: Matriz ) {pre true} {post true} |[ write(msg); var k:=0:int; {bound m.DIM - k} do k < m.DIM -> write( " [ " + m.Coord[k][0] + (%SIGMA j: 1 <= j < m.DIM : ", " + m.Coord[k][j]) + " ]" ); // write( " [ " + m.Coord[k][0] + ", " + m.Coord[k][1] + ", " + m.Coord[k][2]) + " ]" ); k := k + 1 od ]| // Porque no podemos añadir un String P = write2string("lo que sea" + cpa + z[a]) /******************************************* ************** Casos de Prueba ************* *******************************************/ ]|