Metodos Formales 2Parcial
![]() |
![]() |
![]() |
Título del Test:![]() Metodos Formales 2Parcial Descripción: Metodos Formales Segundo Parcial |




Comentarios |
---|
NO HAY REGISTROS |
Para un programa Prog con una precondición pre y poscondicion post existe un test que comienza en un estado que satisface pre, y al terminar, viola post, no hace falta calcular WP, ya que sabemos que el programa es incorrecto. Verdadero. Falso. Los lenguajes formales orientados a modelos describen formalmente al software mediante modelos abstractos formales que constan de dominios, propiedades y operaciones sobre estos. Verdadero. Falso. En Alloy, el operador relacional de traspuesta ~ facilita la especificación de propiedades relacionales, pero no extiende el poder expresivo del lenguaje. El operador se puede expresar en términos de otros operadores del lenguaje. Verdadero. Falso. Si pre es falso, entonces {pre} Prog {post} se cumple, cualesquiera sean Prog y post. Verdadero. Falso. En verificación formal de programas, lo que distingue a la corrección total de la corrección parcial, es que la corrección…, además de los requisitos de la corrección parcial, la terminación del programa en todas las ejecuciones que comienzan en… satisfacen la precondición. Verdadero. Falso. En Alloy, algunos operadores relacionales binarios, es decir, que reciben dos argumentos, se aplican sólo a relaciones de una aridad, entre ellos la clausura transitiva(^). Falso. Verdadero. Si pre es verdadero, entonces {pre} Prog {post} se cumple, cualesquiera sean Prog y post. Verdadero. Falso. La logica proposicional es tan expresiva como la logica de primer orden. Falso. Verdadero. ¿Qué es la sobreescritura relacional?. Técnica de programación orientada a objetos que reemplaza métodos heredados sin modificar la relación entre clases. Operación que invierte el orden de los atributos en una relación para mantener la simetría de las tuplas. Función lógica que reemplaza todos los predicados de una relación por valores constantes. Operación relacional que elimina todas las tuplas duplicadas de una relación, sin tener en cuenta dominios compartidos. Operación relacional binaria, que calcula la unión entre dos relaciones, “sobreescribiendo” las tuplas de la primera que comparten el mismo dominio que tuplas de la segunda. ¿Dadas dos fórmulas α y β, si sabemos que α ⇒ β, cuál es la afirmación correcta?. α es más fuerte que β. β es más fuerte que α. α y β son lógicamente equivalentes. β implica a α en todos los casos posibles. α es una consecuencia lógica de β. ¿Crear un predicado de cuerpo vacío en Alloy. ¿Cómo se interpreta?. Ausencia de restricciones del predicado, es decir, “True” (verdadero). Se interpreta como “False” (falso), ya que no se definen condiciones. El predicado no se puede ejecutar al no contener expresiones válidas. Alloy lo ignora durante el análisis por no contener restricciones. Se asume que el predicado siempre falla y genera un contraejemplo. Completa el fragmento con la opción correcta. Al ejecutar un predicado en Alloy, se intenta encontrar ____________. Instancias que satisfacen simultáneamente los hechos y el predicado. Tuplas aleatorias que coincidan parcialmente con las restricciones del modelo. Errores de sintaxis en las signaturas y hechos definidos en el modelo. Todas las posibles combinaciones de valores sin aplicar restricciones. Contraejemplos que violen las aserciones definidas en el modelo. Completa el fragmento con la opción correcta. Dados dos relaciones A y B de la misma aridad i, la expresión A & B denota una ____________. De aridad i. De aridad 2i, resultado de combinar las tuplas de A y B. Binaria, independientemente de la aridad original. De aridad 1, ya que representa la intersección de conjuntos. Vacía, a menos que A y B sean idénticas. Al verificar formalmente, mediante WP, un programa de la forma: if (cond) {prog1} else {prog2} x = expr respecto de cierta poscondicion post, se procede de la siguiente manera: Primero se calcula el WP de la asignación y post, y al resultado se le aplica el WP del if-then-else. Se evalúan por separado prog1 y prog2 sin considerar la condición. Se ignora la asignación final, ya que el if domina la ejecución. Se aplica WP directamente al if, y luego se evalúa post como precondición. Se reemplaza la instrucción condicional por un bucle while para simplificar el análisis. Necesitamos verificar que el programa Prog siguiente, que no modifica el valor de la variable y:if(y >= 0) { x = x + 1}, garantiza la poscondicion (y >=0). Como Prog no modifica y, tenemos que WP(Prog, y>=0) da como resultado: y >= 0. x > 0. y > 0. True, porque la condición no depende del estado previo del programa. x = x + 1. En una especificación formal en el lenguaje Alloy. Cómo es posible analizar las..de un modelo formal?. Chequeo de satisfactibilidad de predicados. Verificación acotada de aserciones. Ejecución del código en un entorno Java para evaluar expresiones. Simulación aleatoria de relaciones hasta encontrar errores. Compilación del modelo para obtener una versión ejecutable. Aplicación directa de WP sin definir hechos ni restricciones. En Alloy, que permite la definición de un predicado? Seleccione las 2 opciones correctas. Describir propiedades del modelo. Modelar operaciones del modelo. Crear instancias automáticas sin restricciones. Definir constantes globales del sistema. Generar directamente código ejecutable. Validar automáticamente todas las aserciones sin ejecutarlas. En Alloy algunos operadores relacionales binarios, que reciben dos argumentos se aplican sólo a relaciones de una misma aridad. ¿Qué operación se puede encontrar entre ellos?. La unión relacional (+). La diferencia relacional (-). La composición relacional (.). La sobreescritura relacional (++). La transposición (~). El cierre reflexivo (^). Tenemos una signatura sig A {links : set A}, y queremos especificar el hecho…relacion link es simétrica (x esta relacionado con y si y solo esta relacionado con x, en links). De que manera se puede…esta restricción?. All x, y: A | x -> y in links iff y -> x in links. All a: A | all a1: A | a->a1 in links iff a1-> a in links. All a: A | all a1: A | a1 in a.links iff a in a1.links. all x: A | one y: A | x -> y in links. some a: A | a in a.links. |