Probar no puede intentarlo todo
En un juego, dos jugadores pueden coger la última entrada en el mismo instante. Pruebas mil veces y funciona. El error necesita un orden exacto de sucesos y aparece en la mil una. Un método formal no prueba casos. Pide a una máquina que los mire todos.
Al terminar esta lección
Nota
Puedo decir qué devuelven un resolutor y un verificador de modelos cuando una propiedad es falsa.
Palabras clave
- Propiedad: una afirmación sobre un sistema que debe ser siempre cierta.
- Resolutor: un programa que encuentra valores que cumplen unas reglas.
- Verificador de modelos: un programa que prueba todos los estados que un modelo puede alcanzar.
- Invariante: una propiedad que debe cumplirse en todos los estados.
- Contraejemplo: una ejecución que muestra que la propiedad es falsa.
- Modelo: una descripción pequeña de un sistema que deja fuera el detalle.
Para empezar: lo que ya sabes
Nota
Responde mentalmente. 1. ¿Qué es una variable? 2. ¿Qué es una condición en un if? 3. ¿Qué puede pasar cuando dos programas cambian lo mismo a la vez? Necesitas la tercera respuesta enseguida.
Antes de empezar
Nota
Pulsa Iniciar el laboratorio en la barra de arriba de esta lección. Este laboratorio es una máquina Ubuntu entera, solo para ti, así que tarda un poco más en arrancar que un contenedor. Cada botón Ejecutar escribe su comando en el terminal de la máquina, uno tras otro en la misma sesión. Si uno dice que la máquina aún está arrancando, espera unos segundos y púlsalo otra vez. La primera ejecución de una herramienta de Java tarda unos segundos. Para verlos, o para escribir los tuyos, pulsa Abrir terminal en la barra.
Un resolutor encuentra valores, o demuestra que no hay
Z3 es un resolutor. Le das reglas y responde sat (satisfacible: hay valores que cumplen) con un ejemplo, o unsat (ningún valor cumple). El primer comando muestra la versión. El segundo pide un número x mayor que 3 y menor que 6: Z3 dice sat y da 4 para x. El tercero pide uno mayor que 5 y menor que 3: Z3 dice unsat. Así demuestra: para probar una afirmación, pide un caso en el que falle y obtén unsat.
z3 --versionSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
echo '(declare-const x Int) (assert (and (> x 3) (< x 6))) (check-sat) (get-model)' | z3 -inSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
echo '(declare-const x Int) (assert (and (> x 5) (< x 3))) (check-sat)' | z3 -inSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Comprueba
Consejo
Z3 dice unsat para unas reglas de un horario. ¿Ha encontrado un horario? Respuesta: no. unsat significa que ningún horario cumple todas las reglas, así que las reglas se contradicen.
Un verificador de modelos encuentra el mal orden
SPIN verifica modelos escritos en Promela. Tu laboratorio tiene uno: dos trabajadores suman 1 a un contador compartido, con un cerrojo que todavía no hace nada. spinrun construye el verificador y lo ejecuta sobre todos los órdenes que pueden seguir los trabajadores. Imprime assertion violated (inside==1) y errors: 1, y guarda una traza. El segundo comando reproduce esa traza paso a paso: los dos trabajadores hicieron inside = (inside+1) antes de que ninguno saliera.
spinrun formal/spin/main.pmlSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
spin -t -p formal/spin/main.pmlSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Un error frecuente
Advertencia
Mucha gente cree que un verificador de modelos demuestra que un programa es correcto. Demuestra que el modelo tiene la propiedad que escribiste, y nada más. Un invariante TRUE nunca se rompe, así que el verificador lo da por bueno al instante y no te dice nada. La propiedad debe decir algo que un sistema defectuoso no cumpliría.
Un invariante puede ser falso de un buen sistema
TLA+ describe un sistema como estados y pasos, y TLC lo verifica. El Lock.tla del laboratorio tiene dos procesos que pueden estar cada uno idle, wait o cs (en la sección crítica). Este invariante dice que nunca están los dos esperando. Eso es falso incluso de un cerrojo correcto: TLC imprime Invariant NotBothWaiting is violated y un contraejemplo de tres estados que acaba con los dos procesos en wait. La tarea real del laboratorio es otro invariante.
tlc formal/tla/Lock NotBothWaitingSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Un contraejemplo puede ser un dibujo de personas
Alloy describe cosas y los vínculos entre ellas, y busca un ejemplo pequeño que rompa una afirmación. Aquí las cosas son personas y quién es amigo de quién. alloy ejecuta los dos comandos del archivo. check Symmetric imprime SAT: Alloy encontró un contraejemplo, dos personas en las que una cuenta a la otra como amiga y no al revés, mostrado como Person$1->Person$0. run Meet también imprime SAT: encontró un ejemplo para mirar. En un check, SAT significa que la afirmación es falsa.
alloy formal/alloy/model.alsSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Ahora haz el laboratorio
Consejo
Has visto un resolutor, una traza, un contraejemplo y una instancia. Tu laboratorio te pide escribir las reglas, el cerrojo, el invariante y la reparación, y luego cada herramienta los comprueba. Abre el README.md de tu carpeta personal con cat README.md en el terminal.
Comprobación final
Consejo
Responde sin mirar atrás. 1. ¿Qué dice Z3 cuando ningún valor cumple las reglas? 2. ¿Qué es un contraejemplo? 3. ¿Qué falla en un invariante TRUE? 4. En un check de Alloy, ¿qué significa SAT? Respuestas: unsat; una ejecución que muestra que la propiedad es falsa; nunca se rompe, así que no demuestra nada; se encontró un contraejemplo.
Para el profesorado
Consejo
Esta lección se trabaja en un laboratorio de VM: cada estudiante tiene su propia máquina Ubuntu con cuatro herramientas de verificación, y un botón Ejecutar escribe en su terminal y muestra lo que imprimió. Ideas clave: 1. Un resolutor responde sat con un ejemplo o unsat sin ninguno. 2. Un verificador de modelos prueba todos los órdenes de sucesos y da un contraejemplo cuando una propiedad falla. 3. Un invariante TRUE no demuestra nada. 4. Un contraejemplo es la prueba de la herramienta, y puede mostrar que la propiedad era la equivocada. Error frecuente: creer que aprobar significa que el sistema es correcto. Material: el laboratorio y un navegador; TLC y Alloy necesitan una VM con la sesión iniciada, que puede llegar a GitHub. Consejo: antes de spinrun, pide a la clase que encuentre a mano el mal orden. El laboratorio tiene su propia comprobación que ejecuta cada herramienta.