1 Análisis de especificaciones Z

2 Análisis La idea es verificar propiedades a partir de la especificación o descubrir que propiedades que se creían válidas en realidad no lo son. Existen ciertas verificaciones estándar y otras que dependen de cada especificación o del lenguaje utilizado o del interés del desarrollador. También, algunos teoremas pueden usarse como documentación de ciertas propiedades del modelo que de otra forma quedarían implícitas.

3 El teorema de inicialización Si la especificación es consistente el estado inicial debe satisfacer el invariante de estado:  Ö SystemState × InitSystem  Ö Editor × Init  Ö left, right: TEXT | #(leftÊright) ã maxsize × left = right = ÏÐ  Ö left, right: TEXT × #(leftÊright) ã maxsize Ù left = right = ÏÐ #(ÏÐ Ê ÏÐ) ã maxsize 0 ã maxsize

4 En Z/EVES theorem EditorInit E Editor ¥ Init proof of EditorInit prove by reducemaxsize  0  true Este comando aplica una combinación usual de otros comandos de prueba (prenex, rearrange, equality substitution y reduce), hasta que la prueba finaliza (true) o no hay más progreso. No puede probarse pues maxsize fue definido en una definición axiomática como un natural y Z/EVES sabe muy poco de los naturales como para deducir automáticamente esta desigualdad; Z/EVES sabe mucho de los enteros.

5 proof of EditorInit invoke E Editor ¥ left e seq CHAR ¦ right e seq CHAR ¦ # ( left ^ right ) ø maxsize ¦ left = right ¦ right = ãñ rewriteEditor[left := ãñ, right := ãñ ] ¦ 0  maxsize invoke ãñ e seq CHAR ¦ ãñ e seq CHAR ¦ # (ãñ ^ ãñ) ø maxsize ¦ 0 ø maxsize reduce0 ø maxsize ¦ true use maxsize$declarationmaxsize    0 ø maxsize invoke  maxsize e { n: Z | n ù 0 } Þ 0 ø maxsize reducetrue Una prueba más detallada de EditorInit

6 theorem grule maxsizeBound //regla de suposición 0 ø maxsize proof of maxsizeBound use maxsize$declarationif maxsize   then 0 ø maxsize else true invoke  if maxsize e { n: Z | n ù 0 } then 0 ø maxsize else true reducetrue theorem EditorInit E Editor ¥ Init proof of EditorInit prove by reducetrue Otra prueba de EditorInit

7 invoke name Si name es el nombre de un esquema o el nombre de un término introducido en una definición, todas las apariciones del nombre en el gol actual son reemplazadas por su definición. Si no se especifica ningún nombre todos los nombres de definiciones y esquemas son invocados. invoke predicate name

8 rewrite Al re-escribir, Z/EVES simplifica y aplica reglas de re-escritura siempre que sea posible. Una regla de re-escritura es un teorema de la forma Condición  Patrón = Reemplazo. El toolkit de Z está lleno de reglas de re-escritura: theorem disabled rule capSubsetLeft[X] S  [X] T  S  T = S theorem rule eqTuple2 (x,y) = (x',y')  x = x'  y = y’ Enteros, igualdad, lógica proposicional, tautologías

9 apply theorem-name Las reglas de re-escritura pueden aplicarse mediante el comando apply o seleccionando una expresión, pulsando el botón derecho del mouse y examinando la opción “Apply to expresion”. Las reglas habilitadas son aplicadas automática- mente por el asistente de pruebas.

10 reduce Al reducir, Z/EVES simplifica y re-escribe, y si una subfórmula es un esquema o el nombre de una abreviatura, la subfórmula será reemplazada por la definición y el resultado será reducido nuevamente.

11 use theorem-name ··· La sintaxis más general es algo compleja pues se deben instanciar los parámetros y variables del teorema a ser usado. Por ejemplo si tenemos: theorem rule inDom [X, Y]  R: X  Y  x  dom R  (  y: Y  (x, y)  R) y estamos probando un teorema sobre f:    use inDom [ ,  ] [R:=f]

12 use theorem-name ··· (2) El teorema usado es agregado como hipótesis del gol actual de manera que los comandos simplify, reduce o rewrite lo usarán para hacer avanzar la prueba. Si el gol, Q, no es una implicación entonces “ use A” lo transforma en A  Q. Si el gol es la implicación P  Q, entonces “ use A” lo transforma en A  P  Q.

13 Errores de dominio El sistema de tipos de Z no es tan poderoso como para garantizar que todas las expresiones sean significativas. –1 div 0, max , # , etc. Por este motivo, Z/EVES verifica cada párrafo y determina si es necesaria una comprobación de dominio, en cuyo caso plantea una obligación de prueba que debe ser descargada.

14 Ejemplo È_ Ejemplo ________ ® f: Z § Z Ç__________ ®A z: Z ¥ f z < 5 Ð_____________ È_ EjemploCorr ______ ® f: Z § Z Ç__________ ®A z: Z | z e dom f ¥ f z < 5 Ð_____________ proof of Ejemplo$domainCheck f e Z § Z ¦ z e Z Þ z e dom f Es imposible de probar. proof of Ejemplo$domainCheck f e Z § Z ¦ z e Z ¦ z e dom f Þ z e dom f Se pueba facilmente con simplify La mayoría de las obligaciones de prueba provienen de expresiones donde intervienen aplicaciones de funciones parciales

15 Satisfacción de esquemas Un error posible es definir un esquema cuyo predicado sea (siempre) falso, es decir un esquema insatisfacible. Para evitar ese error, se debe probar:  Ö Schema; Inputs? × true Si el esquema erróneo corresponde: –al estado, entonces el sistema es imposible; –a una operación, entonces esta nunca puede ser invocada exitosamente.

16 È_ Ascensor _______________ ® sentido: SENTIDOS ® puerta: ESTPUERTA Ç_______________ ® sentido ë Parado Þ puerta = Cerrada Ð_____________________ È_ AbrirPuerta __________ ®  Ascensor Ç____________ ® sentido = Arriba ® puerta = Cerrada ® puerta' = Abierta ® sentido' = sentido Ð_________________ theorem AbrirPuertaInsat E AbrirPuerta ¥ true proof of AbrirPuertaInsat instantiate sentido == Arriba,AbrirPuerta[puerta := Cerrada, puerta == Cerrada, puerta' := Abierta, sentido := Arriba, sentido' == Arriba, sentido' := Arriba] puerta' == Abierta v (E AbrirPuerta ¥ true ) invokeArriba  Parado  Abierta = Cerrada Instancia variables cuantificadas existencialmente con valores constantes ya definidos.

17 Cálculo de precondiciones La precondición de una operación es un predicado que describe todos los estados de partida en los que la operación está definida. Así, la precondición sólo contiene variables de estado no primadas y variables de entrada. La precondición de una operación es:  SystemState’; Outputs!  Op o en Z/EVES,  SystemState; Inputs?  pre Op

18 Es conveniente documentar la precondición, P, de cada operación:  SystemState; Inputs? | P  pre Op È_ FDoc _______________ ® miembros: DNI © NAME ® prohibidos: P DNI Ç_______________ ® prohibidos z dom miembros Ð___________________ È_ AddMember __________________ ®  FDoc ® candidato?: NAME ® doc!: DNI Ç_______________ ® candidato? ä ran miembros ® doc! ä dom miembros ® miembros' = miembros U {( doc! Œ candidato? )} ® prohibidos' = prohibidos Ð_________________________

19 Ö Fdoc’; doc!: DOC × AddMember   Ö miembros’:DOC « PERSONAS; prohibidos’:¡DOC; doc!:DOC × prohibidos’ º dom miembros’ Ù candidato? ´ ran miembros Ù doc! ´ dom miembros Ù prohibidos’ = prohibidos Ù miembros’ = miembros ¼ {doc! § candidato?}  Ö doc!: DOC × [Regla One-point con miembros’ y prohibidos’] prohibidos º dom miembros ¼ {doc! § candidato?} Ù candidato? ´ ran miembros Ù doc! ´ dom miembros  Ö doc!: DOC × [Fdoc asegura que prohibidos º dom miembros ] candidato? ´ ran miembros Ù doc! ´ dom miembros  candidato? ´ ran miembros Ù Ö doc!: DOC × doc! ´ dom miembros  candidato? ´ ran miembros Ù dom miembros µ DOC

20 En Z/EVES theorem AddMemberPre A FDoc; candidato?: NAME ¥ pre AddMember proof of AddMemberPre prove by reducetipos Þ (E doc!: DNI ¥ miembros U {( doc!, candidato? )} e DNI © NAME ¦ ! candidato? e ran miembros ¦ ! doc! e dom miembros ) apply cupInPinjun predicado muy largo provetipos Þ (E doc!: DNI ¥ ! candidato? e ran miembros ¦ ! doc! e dom miembros )

21 Propiedades de un modelo Estas propiedades pueden haberse establecido en los requerimientos informales o pueden ser puntos clave de la especificación. È_ BanMember ______________ ®  FDoc ® mem?: DNI Ç_________ ® mem? e dom miembros ® prohibidos' = prohibidos U { mem? } ® miembros' = miembros Ð_____________________

22 BanMember | proh? ³ prohibidos  ôFdoc   óFdoc; proh?: ID | proh? ³ dom miembros prohibidos’ = prohibidos ¼ {proh?} miembros’ = miembros Ù proh? ³ prohibidos  ôFdoc   óFdoc; proh?: ID | proh? ³ dom miembros prohibidos’ = prohibidos ¼ {proh?} miembros’ = miembros Ù proh? ³ prohibidos  miembros’ = miembros Ù prohibidos’ = prohibidos ¿ AddMember  candidato? ´ miembrosÓprohibidosÔ ?

23 En Z/EVES theorem YaEstaProhibido A mem?: DNI ¥ BanMember ¦ mem? e prohibidos Þ  FDoc proof of YaEstaProhibido prove by reduce... ¦ mem? e prohibidos ¦ prohibidos' = prohibidos U { mem? } Þ prohibidos = prohibidos U { mem? } apply cupSubsetRight to expression prohibidos U { mem? }... ¦ mem? e prohibidos ¦ prohibidos' =if { mem? } z prohibidos then prohibidos else prohibidos U { mem? } Þ prohibidos = if { mem? } z prohibidos then prohibidos else prohibidos U { mem? } provetrue

24 Rage against the machine The teacher stands in front of the class But the lesson plan he cant’t recall The student’s eyes don’t perceive the lies Bouncing off every fucking wall His composture is well kept I guess he fears playing the fool The complacent students sit and listen to the Bullshit that he learned in school FIN