Métodos Formales - Parcial 2

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 de lenguaje. Verdadero. Falso.

Necesitamos verificar que el programa Prog siguiente, que no modifica el valor de la variable y: if (y>=0) (x=x+1;), garantiza la poscondición (y>=0). Como Prog no modifica y, tenemos que WP (Prog, y>=0) da como resultado: Y>=0. Y<=0. Y<0. Y=0.

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 relación. De aridad 1. De aridad 2. De aridad 3.

Al verificar formalmente, mediante WP, un programa de la forma: if (cond) {prog1} else {prog2x expr} respecto de cierta poscondición 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. Primero, se calcula el WP del if-then-else, y al resultado se le aplica el WP de la asignación y post. Primero, se calcula el WP de la especificación y pred, y al resultado se le aplica el WP del if-then-else.

En Alloy, algunos operadores relacionales binarios, es decir, que reciben dos argumentos, se aplican sólo a relaciones de una misma aridad, entre ellos la clausura transitiva (^). Falso. Verdadero.

Crear un predicado con cuerpo vacío en Alloy, ¿cómo se interpreta?. Ausencia de restricciones del predicado, es decir, true (verdadero). Presencia de restricciones del predicado, es decir, false (falso). Ausencia de restricciones del predicado, es decir, false (falso).

En la verificación formal de programas, lo que distingue a la corrección total de la corrección parcial, es que la corrección exige, además de los requisitos de la corrección parcial, la terminación del programa en todas las ejecuciones que comienzan en que satisfacen la precondición. Verdadero. Falso.

La lógica proposicional es tan expresiva como la lógica de primer orden. Falso. Verdadero.

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. Instancias que satisfacen los hechos (facts) y el predicado. Instancias que satisfagan solamente el predicado. Escenarios que satisfacen los hechos y el predicado.

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 i + 1. De aridad A. De aridad B.

Seleccione las 2 (dos) opciones correctas. En Alloy, ¿qué permite la definición de un predicado?. Describir propiedades del modelo. Modelar operaciones del modelo. Definir la estructura estática del sistema y sus relaciones. Establecer restricciones globales que se asumen verdaderas en todas las instancias del modelo.

Para un programa Prog con una precondición pre y poscondición post existe un test que comienza en un estado que satisface terminar, viola post, no hace falta calcular WP, ya que sabemos que el programa es incorrecto. Verdadero. Falso.

Pregunta: Seleccione las 4 (cuatro) opciones correctas. Tenemos una signatura sig A (links: set A), y queremos especificar el hecho relación links es simétrica (x está relacionado con y si y sólo si y está relacionado con x, en links). ¿De qué manera se puede ir 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 | a -> a in links. All a: A | a1 in a.links iff a in a1.links. All y, x: | A y-> x in links iff x->y in links.

Seleccione las 2 (dos) opciones correctas. En una especificación formal en el lenguaje Alloy, ¿cómo es posible analizar las ((propiedades?)) de un modelo formal?. Chequeo de satisfactibilidad de predicados. Verificación acotada de aserciones. Cálculo de la precondición más débil. Demostración interactiva de teoremas.

Si pre es verdadero, entonces (pre Prog (post) se cumple, cualesquiera sean Prog y post. Falso. Verdadero.

Los lenguajes formales orientados a modelos describen formalmente al software mediante modelos abstractos formales, que de...() ..dominios, propiedades y operaciones sobre estos. Verdadero. Falso.

¿Qué es la sobreescritura relacional?. 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. Operación relacional binaria que combina dos relaciones, emparejando el último elemento de las tuplas de la primera con el primer elemento de las tuplas de la segunda. Operación relacional binaria que enlaza cada tupla de la primera relación con todas las tuplas de la segunda, generando todas las combinaciones posibles. Operación relacional binaria que devuelve únicamente aquellas tuplas que son exactamente idénticas y están presentes simultáneamente en ambas relaciones.

Dadas dos fórmulas alfa y beta, si sabemos que alfa => beta entonces, ¿cuál es la afirmación correcta?. Alfa es más fuerte que beta. Beta es mas fuerte que Alfa. Todo modelo que satisface a beta, necesariamente satisface a alfa. Alfa y beta son lógicamente equivalentes.

Seleccione las 2 (dos) opciones correctas. 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 unión relacional (-). La diferencia relacional (+).

Si pre es falso, entonces (pre Prog post) se cumple, cualesquiera sean Prog y post. Verdadero. Falso.

El cálculo de WP de un programa y poscondición: Se puede realizar de manera enteramente mecánica, siempre que el programa no tenga iteración. Se puede hacer de manera mecánica si la precondición es verdadera. Nunca se puede hacer de manera mecánica, es siempre manual. Siempre se puede realizar de manera enteramente mecánica.

¿En qué consiste la técnica de análisis denominada ejecución simbólica?. Explorar sistemáticamente los caminos del programa, utilizando entradas simbólicas en lugar de concretas, y recolectando las condiciones que estas deben cumplir para cada camino específico. Ejecutar el programa bajo análisis en un conjunto de datos aleatorios. Revisar, en grupos, el código de un programa analizando posibles deficiencias, como uso inadecuado de bibliotecas, la violación de estándares, etc. Analizar los requisitos de un programa abstracto, y simular su ejecución cuando aún no se cuenta con el código del programa.

Dado una aserción de corrección {pre} Prog {post}, el programa satisface su especificación si: Pre => WP(Prog, pos). Post => WP(Prog, pre). WP(Prog, pos) => pre. WP(Prog, pre) => pos.

Consideremos el fragmento de programa siguiente, tomado del cuerpo del método mismaLinea de la clase a verificar: if (fila == otra.fila) { resultado = true; } y la poscondición (resultado == true). ¿Cuál es la precondición más débil (WP) de este programa y poscondición?. (fila == otra.fila => true == true) & (fila != otra.fila => resultado == true). fila == otra.fila & true == true. fila == otra.fila || true == true. true == true.

Consideremos el programa siguiente, tomado del cuerpo del constructor de la clase a verificar: fila = nuevaFila; columna = nuevaColumna; deJugadorA = juegaA; y la poscondición (deJugadorA == true). ¿Cuál es la precondición más débil (WP) de este programa y poscondición?. juegaA == true. fila >= 1 & fila <= 6 & columna >= 1 & columna <= 7. deJugadorA == deJugadorA. fila >= 1 & fila <= 6.

¿De qué es la implementación el método repOK()?. El invariante de clase, que debería ser verdadero luego de la ejecución de cada constructor y todo método público debe preservar. Un test unitario para comprobar si el constructor de la clase funciona correctamente. El chequeo de la precondición de un método de la clase en la que está definido.

Las aserciones de corrección capturan el comportamiento esperado de un programa a través de: Dos fórmulas, la precondición y la poscondición del programa. Comentarios en el código. Información de escenarios específicos de ejecución, es decir, tests.

Selecciona 2 (dos) opciones correctas: Si un programa es totalmente correcto respecto de su especificación, dada en términos de pre y poscondición, entonces: Se garantiza que, si se comienza la ejecución en un estado que satisface la precondición, y el programa termina, al hacerlo se cumple la poscondición. Se garantiza que si se comienza la ejecución en un estado que satisface la precondición, el programa termina. Se garantiza que, en algunos casos, pero posiblemente no todos, cuando se cumple la precondición el programa termina. Se garantiza que la poscondición y la precondición son equivalentes.

El WP de una asignación x = expr (a x se le asigna la expresión expr) y una poscondición dada pos, es: El reemplazo de x por la expresión expr en la poscondición pos. La conjunción x & expr. La disyunción x || expr. El reemplazo de la expresión expr por la variable x, en la poscondición pos.

Un invariante adecuado para un programa con iteración debe: (i) en combinación con la condición de terminación del ciclo, implicar a la poscondición; y (ii) valer justo antes de alcanzar la iteración. No importa si el cuerpo del ciclo preserva al invariante o no. Con las dos condiciones anteriores alcanza. Falso. Verdadero.

Dadas dos aserciones p y q, p es más débil que q, lo que equivale a decir que: Q => p. P => q. P es verdadero. Q es verdadero.

Dado un programa Prog y una especificación en términos de precondición pre y poscondición pos, el programa es incorrecto respecto a esta especificación si: Existe una ejecución de Prog que comienza en un estado que satisface pre, y termina en un estado que no satisface pos. Existe una ejecución de Prog que comienza en un estado que no satisface pre, y termina en un estado que no satisface pos. Existe una ejecución de Prog que no satisface la precondición pre. Existe una ejecución de Prog que comienza en un estado que no satisface pre, y termina en un estado que satisface pos.

El método conectada (ficha otra) requiere como precondición que otra sea distinto de null. La forma adecuada de representar esta poscondición es chequeando si la misma se cumple al comienzo del método, y de no ser así lanzar una excepción de tipo IllegalArgumentException. Verdadero. Falso.

Para calcular el WP de una asignación es necesaria la poscondición. En cambio, para calcular el WP de un if-then-else hace falta la precondición. Falso. Verdadero.

Si un programa es parcialmente correcto respecto de su especificación, dada en términos de pre y poscondición, entonces: Se garantiza que si se comienza la ejecución en un estado que satisface la precondición y el programa termina, lo hace en un estado que satisface la poscondición. Se garantiza que el programa cumple la especificación en algunos casos, no todos. Se garantiza que el programa termina para algunos casos que satisfacen la precondición, pero no todos. Se garantiza que el programa termina para todas las ejecuciones que cumplen con la poscondición.

Dado un programa Prog y una especificación en términos de precondición pre y poscondición pos, el programa es correcto si: Toda ejecución de Prog que comienza satisfaciendo pre termina satisfaciendo pos. Existe una ejecución de Prog que comienza satisfaciendo pos y termina satisfaciendo pre. Toda ejecución de Prog que comienza satisfaciendo pos termina satisfaciendo pre. Existe una ejecución de Prog que comienza satisfaciendo pre y termina satisfaciendo pos.

Dado un programa Prog y una especificación en términos de precondición pre y poscondición pos, para demostrar que Prog no es correcto respecto de su especificación, ¿con qué alcanza?. Dar un estado inicial de Prog que satisface pre, y cuyo correspondiente estado final no satisface pos. Dar un estado inicial de Prog que satisface pos, y cuyo correspondiente estado final no satisface pre. Mostrar que pre y pos no son equivalentes. Dar un estado inicial de Prog que satisface pre, y cuyo correspondiente estado final también satisface pos.

La corrección parcial difiere de la corrección total del programa debido a que: La corrección total exige, por sobre la corrección parcial, la terminación del programa para las ejecuciones que satisfacen la precondición. La corrección parcial exige que se satisfaga la poscondición, mientras que la corrección total exige que se satisfaga la precondición. La corrección parcial exige, por sobre la corrección total, la eficiencia del programa. La corrección parcial exige que se satisfaga la precondición, mientras que la corrección total exige que se satisfaga la poscondición.

La lógica relacional empleada por el lenguaje Alloy posee el mismo poder expresivo que la lógica de predicados (lógica de primer orden). Falso. Verdadero.

Cuando en la declaración de un campo en una signatura, no se indica un modificador de cardinalidad, el modificador de cardinalidad por defecto es: El modificador “one”, que indica que cada elemento de la signatura donde se define el campo puede estar relacionado con un átomo (elemento) del tipo declarado del campo. El modificador “lone”, que indica que cada elemento de la signatura donde se define el campo puede estar relacionado con cero o un átomo (elemento) del tipo declarado del campo. El modificador “set”, que indica que cada elemento de la signatura donde se define el campo puede estar relacionado con cero o más átomos (elementos) del tipo declarado del campo. El modificador “some”, que indica que cada elemento de la signatura donde se define el campo puede estar relacionado con uno o más átomos (elementos) del tipo declarado del campo.

Alloy Analyzer es capaz de encontrar contraejemplos de aserciones, pero no es capaz de detectar problemas de inconsistencia en una especificación. Falso. Verdadero.

En Alloy es posible dar estructura a las especificaciones a través de campos. Un campo se define…. Como parte de alguna signatura, y define una relación. Como parte de un hecho, y define una fórmula. Como parte de alguna signatura, y define una fórmula. Como parte de una aserción, y define una restricción.

En una especificación Alloy, dos signaturas distintas, como el caso de las signaturas «Direccion» y «Dato» en la especificación de memorias, definen: Dominios que no pueden solaparse, es decir, no tienen elementos en común, pero que pueden o no ser vacíos. Dominios no vacíos que pueden solaparse, es decir, tener elementos en común. Dominios no vacíos, que no pueden solaparse, dado que signaturas distintas tienen conjuntos de elementos distintos. Dominios que pueden solaparse, es decir, tener elementos en común, pero deben necesariamente ser no vacíos.

¿Qué definen las signaturas en Alloy?. Dominios de datos. Restricciones provenientes del dominio del problema modelado. Propiedades formales.

En la declaración de un campo dentro de una signatura, el modificador “set” indica: Que cada elemento de la signatura donde se define el campo puede estar relacionado con cero o más átomos (elementos) del tipo declarado del campo. Que indica que cada elemento de la signatura donde se define el campo puede estar relacionado con cero o un átomo (elemento) del tipo declarado del campo. Que cada elemento de la signatura donde se define el campo puede estar relacionado con exactamente un átomo (elemento) del tipo declarado del campo.

En un modelo Alloy, cuando se declaran varios hechos (facts) en el mismo modelo, esto se interpreta como: La conjunción de todos los hechos, es decir, se añaden todos los hechos como suposiciones simultáneas del modelo. La disyunción de todos los hechos, es decir, se puede considerar arbitrariamente la validez de al menos uno de los hechos. La validez del primer hecho; el resto de los hechos se ignora. La disyunción excluyente de los hechos, es decir, se considera arbitrariamente la validez de exactamente uno de los hechos.

Selecciona 2 (dos) respuestas correctas: Al declarar un campo dentro de una signatura, el desarrollador…. Puede declarar una restricción de cardinalidad, como el modificador “set” que indica que cada elemento de la signatura que contiene la declaración puede relacionarse con cualquier número de elementos del tipo del campo. Puede declarar como tipo del campo una relación de aridad mayor a uno. No puede declarar restricciones de cardinalidad; tales restricciones se definen exclusivamente a través de hechos. Solo puede usar como tipo de la relación una signatura.

Seleccione 2 (dos) respuestas correctas: En el lenguaje formal de especificaciones Alloy, los predicados se pueden utilizar para definir: Operaciones del modelo, mediante fórmulas con parámetros. Propiedades definidas por fórmulas, que pueden ser utilizadas como parte de hechos, otros predicados y aserciones. Signaturas, dado que las operaciones corresponden a una sintaxis alternativa para introducir nuevos dominios de datos. Comentarios no analizables del modelo: los predicados sirven para describir en lenguaje natural el propósito de un modelo; no tienen efecto en el análisis.

En el lenguaje formal de especificaciones Alloy, los hechos (facts) sirven para modelar: Suposiciones del modelo, propiedades que se asumen verdaderas en todas las instancias del modelo. La estructura de la especificación, dado que los hechos definen relaciones. Propiedades a verificar, es decir, propiedades que comprobaremos si se satisfacen o no mediante análisis. Operaciones del modelo, mediante fórmulas con parámetros.

Dado un modelo Alloy, y una aserción en el mismo, si el resultado de análisis de esta aserción (assertion check) informa que no se encuentran contraejemplos, no implica necesariamente la validez de la aserción en el contexto del modelo. Verdadero. Falso.