Especificación,Verificación yDerivación Formalde ProgramasJavier Álvez Xabier Arregi José Gaintzarain Paqui Lucio Monste Maritxalar