M3y4 - Metodos Formales.pdf

Métodos Formales METODOS FORMALES FECHAS IMPORTANTES Trabajo Práctico Trabajo Práctico Fecha Clase (Clase) (Canvas) 20 y 21/may M1 27 y 28/may...

Métodos Formales METODOS FORMALES FECHAS IMPORTANTES Trabajo Práctico Trabajo Práctico Fecha Clase (Clase) (Canvas) 20 y 21/may M1 27 y 28/may M1 Y M2 3 y 4/jun 1 Parcial 7/jun TP1 10 y 11/jun M3 17 y 18/jun M3 Y M4 17/jun TP1 y TP2 24 y 25/jun M4 28/jun TP2 1 y 2/jul 2 Parcial 8 y 9/jul - 8/jul TP3 y TP4 15 y 16/jul Recuperatorio  METODOS FORMALES METODOS FORMALES Son una serie de técnicas lógicas y matemáticas con las que es posible especificar, diseñar, implementar y verificar programas. El álgebra trata cantidades representadas por medio de letras y signos. Generaliza las operaciones aritméticas. La teoría de conjuntos estudia colecciones de objetos analizando las propiedades y las relaciones entre sus elementos La lógica de primer orden trata a los predicados como funciones que no solo toman números como argumentos, sino expresiones.  MÉTODOS FORMALES ARIANE 5 En 1996, se lanzó el cohete Ariane 5. A los 40 segundos del lanzamiento y 3.700 metros de altitud "la lanzadera Ariane se desvió de su ruta, se partió y explotó". El problema fue al convertir un número almacenado en 'coma flotante de 64 bits’ a un 'entero de 16 bits’. Esa parte del código sólo se usaba durante la preparación para el despegue, pero sin embargo continuaba funcionando durante 40 segundos tras el despegue debido a que el Ariane 4 si lo usaba con valores muy diferentes. El costo fue de USD 500MM. 4  MÉTODOS FORMALES SISTEMA DE TRENES, FRANCIA Hasta 1998 se utilizaba el lenguaje informal para las especificaciones del Sistema de Seguridad de trenes de Francia. Observando los siguientes inconvenientes: Diseño dependiente del punto de vista Especificaciones ambiguas, no legibles, no coherentes, no completes Problemas de validación: No se podia determiner cuanto testing functional era suficiente realizar. 5  MÉTODOS FORMALES METODOS FORMALES Los métodos formales permiten verificar que un sistema se comporta de acuerdo a su especificación utilizando procedimientos matemáticos y lógicos.. Especificación formal, proporciona una descripción precisa de lo que debe hacer el programa Verificación formal, utilizando reglas precisas (matemáticas y lógicas) para demostrar que el software cumple la especificación formal Desarrollo formal, diseñando software de una forma segura que satisfaga las especificaciones formales. Simplificar la automatización de pruebas por su principio matemático 6  MÉTODOS FORMALES METODOS FORMALES Especificación La Ingeniería de software busca acercarse a la especificación de comportamientos. Los métodos formales proporcionan una descripción precisa de lo que debe hacer el programa Verificación ¿Se está construyendo el producto correctamente? Con los métodos de testing se logran eliminar los errores y defectos mas evidentes. Las técnicas de verificación formal dependen de especificaciones matemáticas precisas. 7  MÉTODOS FORMALES METODOS FORMALES Validación ¿Se está construyendo el producto correcto? Los métodos formales se utilizan principalmente en sistemas complejos donde una falla es crítica: equipamento médico, o software de control de veículos, protocolos, etc. 8 MÉTODOS FORMALES LÓGICA PROPOSICIONAL Y DE PRIMER ORDEN 9 MÉTODOS FORMALES LOGICA DE PRIMER ORDEN Es un sistema formal de lógica que permite representar y razonar sobre proposiciones que involucran objetos, propiedades y relaciones. Lenguaje Conectores lógicos: como la negación, conjunción, disyunción, implicación, etc. Cuantificadores: universal (∀) y existencial (∃) Sintaxis: Reglas para construir fórmulas bien formadas, atómicas (con predicados) o compuestas (con conectores lógicos y cuantificadores). Semántica: Asignan significado a los símbolos del lenguaje. Deducción: Reglas de inferencia para realizar razonamientos y demostraciones. 10 MÉTODOS FORMALES LOGICA DE PRIMER ORDEN - APLICACIONES Representación de Especificación y conocimiento en verificación de sistemas sistemas expertos y de software. inteligencia artificial. Modelado de fenómenos en diversas áreas como Análisis de algoritmos y matemáticas, ciencias estructuras de datos. naturales, economía, etc. 11  MÉTODOS FORMALES LOGICA DE PRIMER ORDEN Funciones Lógica de predicados Una función es una regla de correspondencia entre dos conjuntos de tal manera que a cada elemento del primer conjunto le corresponde uno y sólo un elemento del segundo conjunto. 12  MÉTODOS FORMALES ESPECIFICACIONES FORMALES Las especificaciones formales de programas pueden tomar diversas formas. Las mismas suelen describirse por triplas, de la siguiente forma: { Precondición } Prog Programa { Postcondición } Pre Pos Programa: es el programa que queremos verificar Precondición/Postcondición: son dos fórmulas, en general lógica de primer orden, que constituyen la especificación del comportamiento esperado del programa La combinación de programa y especificación se denomina Terna de Hoare 13  MÉTODOS FORMALES ESPECIFICACIONES FORMALES La prueba formal de programas, es una técnica que se basa en el cálculo de predicados. Una prueba formal asegura que el programa es correcto con respecto a una especificación para todas las entradas. P y Q son aserciones de precondición y {pre} s {pos} postcondición {P} s {Q} S programa o bloque a probar {P} s {Q} se denomina especificación Terna de Hoare formal de S Si la ejecución de S empieza en un estado dado por P y S termina, entonces terminará en un estado dado por Q. La corrección total es equivalente a la corrección parcial y la exigencia adicional de 14 que toda ejecución que comienza en un estado que satisface pre, termina.  MÉTODOS FORMALES TERNA DE HOARE Una terna de Hoare { pre } Prog { post } es una aseveración, puede ser verdadera o falsa y su validez exige una demostración. Toda ejecución del programa Prog que comienza en un estado que satisface pre, cuando termina, lo hace en un estado que satisface post Ejemplos: { x == X & y == Y } {x0} { x >= 0 & x < Integer.MAX_VALUE } aux = x; res = x/y x=x+1 x = y; { res < 0 } {x>0} y = aux; { x == Y & y == 15 X}  MÉTODOS FORMALES VERDADERO O FALSO {x==1} Esta terna es verdadera, ya que si se toma el estado inicial 1 x=x+1 {x==1} que cumple la precondición y se ejecuta el programa, se {x==2} obtiene el estado final {x==2}, como indica la postcondición { true } Esta terna es verdadera, cualquiera sea el estado previo a la 2 x = 0; ejecución del programa (true es una propiedad que satisfacen { x >= 0 } todos los estados), luego de asignar cero a x, se llega a un estado en el cual x es mayor o igual que cero {x==X, y==Y} Paso 0. {x==X, y==Y} x=y; 3 Paso 1. {x==Y, y==Y} y=x; Paso 2. {x==Y, y==Y} {x==Y, y==X} Esta terna es falsa (a menos que x = y). Las variables x e y no intercambian sus valores 16 MÉTODOS FORMALES TERNA DE HOARE Y PRECONDICIÓN MAS DÉBIL 17  MÉTODOS FORMALES LOGICA DE HOARE Y WP Lógica de Hoare: Tiene un enfoque orientado a la demostración Luego de construir el programa lo que se queremos ver es si es correcto Intenta demostrar que un programa hace lo que debería (es correcto, valida especificación) {pre} s {pos} Precondición mas débil de Dijkstra Tiene un enfoque orientado a la construcción Si se construye un programa verificando todas sus etapas, seguro se tendrá un programa verificado y correcto. La función WP (weak precondiction) devuelve la precondición mas débil {w-pre} = WP( s , post) 18  MÉTODOS FORMALES TERNA DE HOARE Una terna de Hoare { pre } Prog { post } es una afirmación lógica que puede ser verdadera o falsa. Su validez exige una demostración. Toda ejecución del programa Prog que comienza en un estado que satisface pre, cuando termina, lo hace en un estado que satisface post La terna {pre} Prog {post} equivale a decir que para todo par de estados de programa s y s’, si s y s’ están relacionados por Prog y s satisface pre, entonces s’ satisface post. 19  MÉTODOS FORMALES WP DE LA ASIGNACIÓN Ejemplo: Usamos WP para verificar una aserción de corrección: {x > 10} x=x+1 {x > 0} WP( x = exp, post) = post[exp/x] WP(x = x+1, (x > 0)) = { definición de WP para la asignación } (x > 0)[x+1/x] = { sustitución } (x+1 > 0) = { aritmética } x > -1 Comprobamos que la precondición, x > 10, implica a la precondición más débil que acabamos de calcular, es decir que: VERFICACIÓN FORMAL: Todo entero x x > 10 => x > -1 mayor a diez es mayor a -1 20 MÉTODOS FORMALES COMPOSICIÓN DE FUNCIONES La composición de funciones es el resultado de la aplicación sucesiva de dos o más funciones sobre un mismo elemento x. La composición de funciones se realiza aplicando dichas funciones en orden de derecha a izquierda, de manera que en (g o f)(x) primero actúa la función f y luego la g sobre f(x). 21 MÉTODOS FORMALES WP DE COMPOSICIÓN SECUENCIAL El WP de una composición secuencial se define a través de la composición de WP. WP( prog1 ; prog2, post ) = WP(prog1, WP(prog2, post)) Si el programa es una secuencia de acciones, entonces comenzamos calculando WP para la última acción, y a partir de ese WP el de la acción anterior, y así sucesivamente. 22  MÉTODOS FORMALES WP DE COMPOSICIÓN SECUENCIAL Ejemplo: Usaremos WP para verificar la siguiente terna: {aux >= 0} x = aux; WP( prog1 ; prog2, post ) = WP(prog1, WP(prog2, post)) x=x+1 {x > 0} WP(x = aux; x = x+1, (x > 0)) = { definición de WP para la composición secuencial } WP(x = aux, WP(x = x+1, (x > 0))) = { definición de WP para la asignación } WP(x = aux, (x > 0)[x+1/x]) = { sustitución x por x+1} WP(x = aux, (x+1 > 0)) = { definición de WP para la asignación } (x+1 > 0)[aux/x] = { sustitución x por aux } (aux+1 > 0) = { aritmética } aux > -1 VERFICACIÓN FORMAL: Todo entero aux aux > -1 => aux >= 0 mayor a -1 es mayor o igual a 0 23  MÉTODOS FORMALES VERIFICACIÓN ESTRUCTURAS CONDICIONAL Y REPETITIVA 24  MÉTODOS FORMALES COMPOSICIÓN ALTERNATIVA Podemos realizar también la verificación formal de programas mas complejos, como aquellos que tienen una composición alternativa, es decir, con el if-then-else. El WP es: WP( if (cond) { B1 } else { B2 }, post) = (cond => WP(B1, post)) & (!cond => WP(B2, post)) => : Indica implicación lógica Símbolo ‘&’ : Indica conjunción Símbolo ‘!’: Indica negación 25  MÉTODOS FORMALES COMPOSICIÓN ALTERNATIVA Esta terna de Hoare asevera que el programa calcula correctamente, en la variable result, el valor absoluto (módulo) del valor almacenado en la variable x {true} if (x < 0) { result = -x; } else { result = x; } {(x >= 0 => result == x) & (x < 0 => result == -x)} 26  MÉTODOS FORMALES COMPOSICIÓN ALTERNATIVA Para verificar este programa respecto a su especificación, primero calculamos WP del programa y la postcondición: WP( if (cond) { B1 } else { B2 }, post) = (cond => WP(B1, post)) & (!cond => WP(B2, post)) WP(if (x=0=>result==x)&(xresult==-x)) = { definición de WP para if-then-else } (x WP(result=-x, (x>=0=>result==x)&(xresult==-x)) & (!(x WP(result=x, (x>=0=>result==x)&(xresult==-x)) = { aritmética } (x WP(result=-x, (x>=0=>result==x)&(xresult==-x)) & (x>=0 => WP(result=x, (x>=0=>result==x)&(xresult==-x)) = { definición WP para asig. } 27  MÉTODOS FORMALES COMPOSICIÓN ALTERNATIVA (x (x>=0=>-x==x)&(x-x==-x)) & (x>=0 => (x>=0=>x==x)&(xx==-x)) = { lógica } (x (x>=0=>-x==x)) & (x (x-x==-x)) & (x>=0 => (x>=0=>x==x)) & (x>=0 => (xx==-x)) = { lógica } (x-x==-x) & (x>=0 => x==x) = {sustitución } (xtrue) & (x>=0 => true) = { lógica } true Al ser la precondición más débil true, este programa es correcto respecto de su especificación. 28  MÉTODOS FORMALES PROGRAMAS CON CICLOS Con la incorporación de ciclos en los programas a analizar, perdemos esta sistematicidad y aparece el concepto de invariante. La regla de WP para ciclos es la siguiente: WP(while (cond) {B}, post) = Inv & (Inv & cond => WP(B, Inv)) & (Inv & !cond => post) La parte derecha de la igualdad hace referencia a un predicado Inv que no forma parte del programa ni la postcondición (no aparece en la parte izquierda de la igualdad). Ese predicado debe ser propuesto por el desarrollador. 29  MÉTODOS FORMALES PROGRAMAS CON CICLOS (Inv & !cond => post) Cuando se hace falsa la condición de continuación del ciclo, se sale del ciclo y el invariante implica la postcondición. Es decir, el invariante es suficiente, junto con la condición de terminación del ciclo, para establecer la postcondición del programa. (Inv & cond => WP(B, Inv)) Si es válido el invariante antes de ejecutar el cuerpo del ciclo, y es válida la condición de continuación, entonces debe ser válido el WP del cuerpo del ciclo y el invariante. Luego de ejecutar el cuerpo del ciclo se debe restablecer el invariante (debe volver a valer). Inv Indica que el invariante debe valer antes de comenzar a ejecutar el ciclo. 30  MÉTODOS FORMALES PROGRAMAS CON CICLOS Consideremos el siguiente ejemplo, en el cual suponemos que a es un arreglo de enteros: { a != null } int sum = 0; int i = 0; while (i < a.length) { sum = sum + a[i]; i = i+1; } 𝑎.𝑙𝑒𝑛𝑔𝑡ℎ−1 { sum = σ𝑗=0 𝑎[𝑗] } Esta especificación indica que, si a no es null, entonces luego de ejecutar el programa la variable sum tendrá la suma de todos los valores del arreglo 31 MÉTODOS FORMALES MODELOS 32 MÉTODOS FORMALES SATISFACCIÓN DE RESTRICCIONES Imaginen que les encargaron definir la ubicación de lo invitados a un asado. ¿Fácil? En la propuesta a realizar existen varias limitaciones: la abuela y el abuelo deben sentarse cerca del baño. La tía Juana y la tía Sonia deben sentarse lo más separadas posible. Los hijos del tío Roberto deben estar sentados cerca de él. Los anfitriones deben sentarse en las cabeceras de la mesa… etc. Dadas esta situación, ¿qué instancias satisfacen las restricciones? 33  MÉTODOS FORMALES SATISFACCIÓN DE RESTRICCIONES Simplificar las restricciones 1. El abuelo y la abuela, deben sentarse cerca del baño. 2. La tía Juana y la tía Sonia deben sentarse lo más separadas posible. 3. Los hijos del tío Roberto deben estar sentados cerca de él. 4. Los anfitriones deben sentarse en las cabeceras de la mesa. 5. ….. ¿Suficiente? ¿Qué es una silla?, ¿Cómo se relaciona una silla con una persona?, ¿Qué es una persona?, ¿Qué es un baño?, …. Necesitamos un modelo 34 MÉTODOS FORMALES A TRABAJAR Imaginen que tienen que organizar los puestos de una feria gastronómica, con las siguientes restricciones: Los puestos de comida deben estar agrupados por tipo de cocina Los puestos que venden bebidas alcohólicas deben estar ubicados lejos de los puestos familiares. Los puestos que venden postres y dulces deben estar cerca de la entrada principal para atraer a los visitantes. Debe haber espacio suficiente entre los puestos para que la gente pueda caminar cómodamente. Los puestos de los organizadores del evento deben estar en un lugar visible y de fácil acceso. 35 MÉTODOS FORMALES A TRABAJAR Piensen en cómo podrían representar la distribución de los puestos. Recuerden también considerar el flujo de personas y la accesibilidad. 36 MÉTODOS FORMALES ¿PARA QUE USAMOS MODELOS? Comprender el sistema: la estructura, el comportamiento y cualquier otra característica relevante. Nos permite tener una especificación del sistema. Abstraer el problema: Resaltando los aspectos importantes para su propósito y ocultar los irrelevantes para el observador. 37 MÉTODOS FORMALES ¿PARA QUE USAMOS MODELOS? Facilitar la comunicación: Con los distintos tipos de stakeholder del sistema (desarrolladores, usuarios finales, etc.) Validar el sistema y su diseño: Detectar errores, omisiones y anomalías en el diseño tan pronto como sea posible. Poder realizar análisis formales sobre el sistema 38  MÉTODOS FORMALES MODEL DRIVEN DEVELOPMENT (MDD) Es un paradigma de desarrollo de software que utiliza modelos para diseñar los sistemas a distintos niveles de abstracción, y secuencias de transformaciones de modelos para generar unos modelos a partir de otros hasta OMG: Object Management Group generar el código final de las MDE: Model-driven engineering MDA: Model-driven architecture aplicaciones en las plataformas MDD: model-driven development destino. 39 MÉTODOS FORMALES GENERACIÓN DE CÓDIGO Especificación Especificación Especificación 1. Carga inicial Transformación 2. Inferencia Modelo 3. Especificación Generación Código Código Código 40 MÉTODOS FORMALES ALLOY 41 MÉTODOS FORMALES LENGUAJE DE MODELADO Informal Semi-formal: Se basan principalmente en el uso de lenguajes diagramáticos, tales como UML que transmiten un significado intuitivo Formal: Existen técnicas y herramientas formales que ayudan a modelar el problema y razonar sobre la solución de una manera precisa y rigurosa. Ejemplo Z, Alloy Actualmente casi todos los métodos de desarrollo de software utilizan modelos. 42 MÉTODOS FORMALES LENGUAJE ALLOY Es un lenguaje formal liviano de modelado para la especificación y diseño de software. Tiene una sintaxis simple, semántica intuitiva. Puede analizarse de manera automática con el Alloy Analyzer. Ayuda a verificar el modelo. Alloy = lógica de primer orden + álgebra de relaciones. Está basado en la lógica relacional de primer orden, que permite modelar formalmente sistemas de software. El lenguaje subyacente es el álgebra relacional. 43  MÉTODOS FORMALES FILOSOFÍA DE ALLOY Modelo (uso lenguaje Alloy Analyzer Alloy) SAT solver Alloy es un lenguaje de modelado y también es una herramienta. El analizador Alloy traduce el modelo a una expresión booleana que la herramienta SAT interpreta y devuelve el conjunto de instancias que satisfacen las restricciones (fact). 44  MÉTODOS FORMALES FILOSOFÍA DE ALLOY Un SAT-Solver (SATisfiability solver) es una herramienta que consiste en buscar modelos que satisfagan fórmulas proposicionales. Determina si existe al menos un valor de sus variables para la cual la función es verdadera. 45 MÉTODOS FORMALES ALLOY TOOL 46 MÉTODOS FORMALES ALLOY TOOL Modelo, expresado en lenguaje Alloy Análisis 47 MÉTODOS FORMALES SINTAXIS ALLOY 48  MÉTODOS FORMALES ÁTOMOS Y RELACIONES Átomo: es la entidad primitiva que cumple con tres condiciones Indivisible: no puede ser dividido en partes mas pequeñas. Immutable: sus propiedades no cambian en el tiempo. No interpretada: por defecto no tiene propiedad Relación: es la estructura que relaciona átomos, por ejemplo Tuplas Person = {(P0),(P1)} Relación Unaria Address = {(A0),(A1)} address = {(P0,A1),(P1,A0)} Relación Binaria Átomo Tamaño de la relación: numero de tuplas. Aridad de la relación: numero de átomos en cada relación (unaria, binaria, ternaria). 49 MÉTODOS FORMALES OPERADORES DE CONJUNTO Person = {(P0),(P1)} Address = {(A0),(A1)} none conjunto vacío univ conjunto universal none = {} iden relación identidad univ = {(P0),(P1),(A0),(A1)} iden = {(P0, P0), (P1, P1), (A0, A0), (A1, A1)} Person = {(P0),(P1)} + unión Address = {(A0),(A1)} & intersección - diferencia Person + Address = {(P0),(P1),(A0),(A1)} in subconjunto Person & Address = {} = igualdad Person - (P0) = {(P1)} (P0) in Person = true Person = Address = false 50  MÉTODOS FORMALES OPERADORES RELACIONALES -> producto Person = {(P0),(P1)} cartesiano Address = {(A0),(A1)} -> producto cartesiano Address = :> restricción de rango {(P0,A0),(P0,A1),(P1,A0),(P1,A1)} ++ sobre-escritura. composición Es una operación que resulta en otro conjunto, cuyos elementos son todos los pares ordenados [] composición ~ transpuesta [ ] Composición ^ cláusura transitiva e1[e2] = e2.e1 * cláusura reflexivo-transitiva a.b.c[d] = d.(a.b.c) Se trata de una función o aplicación que toma dos elementos de dos conjuntos dados y los asigna a otro elemento, perteneciente a uno de los dos conjuntos. 51 MÉTODOS FORMALES OPERADORES RELACIONALES Person = {(P0),(P1)} s s restricción de rango Address = {(A0),(A1)} Donde s: un conjunto r: una relación (P0) A0 = {(P1,A0)} Composición. (P0). address = (A1) Persona = {(P0),(P1)} P0 (P0,A1) A1 address = {(P0,A1),(P1,A0)} (P1,A0) Es un join relacional 52  MÉTODOS FORMALES OPERADORES RELACIONALES ~ transpuesta ^ cláusura transitiva Se aplican sólo a relaciones binarias * cláusura reflexo transitiva Person = {(P0), (P1), (P2)} father = {(P0,P2),(P1,P0),(P2,P2)} ~father = {(P2,P0),(P0,P1),(P2,P2)} ^father = {(P0,P2),(P1,P0),(P2,P2),(P1,P2)} *father = {(P0,P2),(P1,P0),(P2,P2),(P1,P2),(P0,P0),(P1,P1)} Dado el conjunto A y una relación R, esta relación es Fuente: Wikipedia transitiva si: a > b y b > c se cumple a > c. 53 MÉTODOS FORMALES CUANTIFICADORES Y OTROS OPERADORES all para todo Person = {(P0), (P1), (P2)} some al menos uno no ninguno some p: Person | p in Person = true lone a lo sumo uno one Person = false one exactamente uno ! NOT negación # cardinalidad && AND conjunción = igual || OR disjunción < menor => implicación > mayor iff Bi-implicación =< menor o igual >= mayor o igual 54 MÉTODOS FORMALES SINTAXIS ALLOY 55  MÉTODOS FORMALES SINTAXIS ALLOY La sintaxis de Alloy es muy simple, convirtiéndose en un lenguaje fácil de aprender a manipular. Solo cuenta con 5 construcciones: Signaturas (Sig): permite describir dominios de datos Predicados (Pre): describen operaciones asociadas con las signaturas. Restricciones (fact): describen propiedades que se consideran verdaderas en el modelo. Aserciones (Assert): propiedades cuya validez sobre el modelo se desea controlar. Comandos: (run, check) instrucciones que el Alloy Analyzer ejecuta. 56  MÉTODOS FORMALES ANALISIS DE PREDICADOS La ejecución de un predicado se corresponde al intento de construir una instancia (escenario) que tenga la estructura dictada por la especificación, satisfaga todos los hechos (facts), y las restricciones del predicado. 57  MÉTODOS FORMALES BÚSQUEDA DE INSTANCIAS Consideremos el predicado sistemaVacio, cuya intención fue la de especificar a un sistema sin productos. Ejecutamos el predicado predicado: run sistemaVacio Alloy Analyzer busca una instancia de la especificación que satisfaga las restricciones del predicado Fact ExisteCantidad indica que todo producto registrado en el sistema debe tener una cantidad, no dice nada al revés 58  MÉTODOS FORMALES BÚSQUEDA DE INSTANCIAS Podemos corregir el modelo indicando que si de un producto existe una cantidad, entonces debe estar registrado en el sistema. 59 MÉTODOS FORMALES ASERCIONES 60  MÉTODOS FORMALES ASERCIONES Una especificación está compuesta por: Aplicación de una estructura (signaturas y campos) Definición de suposiciones a través de hechos (facts) Utilización de predicados para capturar estados y modelar de operaciones Los predicados se pueden evaluar automáticamente pidiendo a Alloy Analyzer la construcción de escenarios que satisfagan las restricciones. Podemos complementarlo con las aserciones 61  MÉTODOS FORMALES ASERCIONES Una aserción captura una propiedad esperada del modelo, es decir, una consecuencia de la especificación. Una propiedad que esperamos que fuese válida es que, en todo sistema, luego de agregar un producto (con la operación agregarProducto), necesariamente el sistema es no vacío. No podría ser una fact, porque forzaríamos a que se cumpla. Tampoco parte de un predicado porque consultaríamos los escenarios para los cuales se cumple. Para esto existe un assert, que indica que siempre que se satisfagan los hechos la propiedad también se cumple. 62 MÉTODOS FORMALES ASERCIONES Las aserciones, a diferencia de los predicados, no tienen parámetros: encierran una fórmula que el desarrollador quisiera validar. 63