Principios de demostraciones de validez

Esta es mi tarea 5 correspondiente a la clase de validación y verificación de Software. La tarea consistió en elegir un ejercicio del pdf logicination y resolverlo, el mio es el 4.18 sobre Fórmulas, situaciones e imágenes donde con una imagen podemos representar diferentes semánticas. 

Exercise 4.18 Consider the following picture:

Use G for the property of being a girl, H for the property of being a hat, and W for the relation of wearing (so that W xy expresses that x is wearing y). Now do the following:

(1) Give a predicate logical formula that is true for the situation in the picture.
(2) Give a predicate logical form

Ejercicio 4.18 considere la siguiente imagen, utilice:

• G para la propiedad de ser una chica, 
• H para la propiedad de ser un sombrero 
• W para la relación de usando (para W(xy) expresa que x está usando y).

Ahora lo siguiente:

(1) Dar una fórmula de lógica predicada que es cierto para la situación en la imagen.

Para esta parte también utilizaremos nuevamente los cuantificadores, en este caso solo utilice uno de la siguiente manera:

• ∀: Todos, para todos

• En la imagen se muestran diferentes enunciados que podrían representarse por lógica predictiva, esta es una de ellas: 

• Todas las chicas están usando sombrero 
    ∀x∀(Gx ^Hy ^Wxy)

(2) Dar una fórmula lógica predicada que es falsa por la situación en la imagen

• Algunas chicas no usan sombrero.  

 ∃Gx(¬Wxy->Hy )

 

 

Lógica predictiva

En esta semana la tarea a entregar es sobre lógica predictiva(predicados) o lógica de primer orden, dentro del libro "Symbolic Logic" debíamos escoger proposiciones compuestas y obtener de ahí lo que son las proposiciones de lógica predictiva.

Esté es mi par de proposiciones:

• Some pictures are not first attempts;(Algunas imágenes no son los primeros intentos)
• No first attempts are really good.(Ninguno de los primeros intentos son  buenos)

Las expresiones que utilice son las siguientes:

• F(x)= imágenes 
• G(x)= primeros intentos
• H(x)= son buenos

Expresiones:
Se  utilizan los cuantificadores para expresar el conjunto de proposiciones.

• ∀: Todos, para todos 
• ∃: Por lo menos uno, algunos, algunas
  

Ahora las proposiciones de lógica predictiva son las que se muestran enseguida:

• ∃F(x) -> ¬G(x)
• ¬∃G(x) -> H(x)

Como ninguno fue un intento bueno, algunas imágenes no son buenas. 

• Conclusión:  ∃F(x)-> ¬H(x).
  

Tarea 4.Diagramas Binarios de Decisión

Para esta tarea el problema a resolver es:

• Inventen una expresión Booleana(Usando por mínimo 3 variables y 4 conectivos básicos)
• Construyan y dibujen su BDD.
• Reduzcan el BDD resultante a un ROBDD.
• Dibujen el ROBDD resultante.

BDD (Diagrama de Decisión Binario)
Un diagrama de decisión binario (DDB) es un grafo acíclico dirigido con
Uno o dos nodos terminales etiquetados con 0 o 1

Expresión Booleana
Mi expresión a representar es la siguiente:

(x2 ^ x3) v (x1 ^ x3)

Tabla lógica:

Árbol Binario de Decisión: 

BDD: 
Este es mi Diagrama de Decisión Binario que dio como resultado.  

Reducción a ROBDD y ROBDD resultante 
En el PDF: "An Introduction to Binary Decision Diagrams" por Henrik Reif Andersen, se mencionan tres condiciones para el orden y reducción:

• Las variables deben estar ordenadas
• Los nodos deben ser únicos
• Solo tests no redundantes deben estar presentes

Referencias: 
"An Introduction to Binary Decision Diagrams"

Aplicaciones de logica propocional

Una de las formas de definir la lógica proposicional es como lo vimos en clase anteriormente es el estudio de las formas de razonamiento donde su validación depende solamente de las propiedades verdadero o falso.

De manera informal, una proposición se define como una frase que puede ser considerada

Verdadera y que no se puede descomponer en otras frases Verdaderas o Falsas, y estas a su ves pueden ser simples o compuestas.

Ejemplo: 
Luis es inteligente y estudioso = Proposición Compuesta
Llueve si y solo si esta nublado = Proposición Compuesta
Luis es inteligente = Proposición simple

Para poder relacionar distintas proposiciones se utilizan los conectivas como las siguientes:

Existe un lenguaje para la logica proposicional representado por el siguiente conjunto de simbolos: 

Existe un orden de precedencia entre los operadores: ¬, ∧, ∨, ⇒y⇔ 

  

Cada uno de los conectores o constantes lógicas se define semánticamente mediante
una tabla de verdad que muestra sus posibles valores veritativos según los casos. 

Aplicaciones:
Se necesita tener un lenguaje con una sintaxis y semántica bien definida.
Se puede utilizar dentro de las matematicas como:

• Definición de objetos matemá́ticos: conjunto, números naturales, nú́meros reales.
• Definición de teorías matematicas: teoria de conjuntos, teoria de los numeros naturales. 

En Circuitos logicos:
La aplicación de la logica proposicional es dentro de circuitos electricos  digitales y es posible en virtud del isomorfismo a la relación de igualdad que existe entre dos objetos.

Teoria de la computación: complejidad descriptiva, y algoritmos de aproximación.

    
En Inteligencia Artificial:
Representación de conocimiento, razonamiento con sentido comú́n.

Referencias: 
Aplicaciones de la logica proposicional 
Conceptos principales
Logica-Proposicional-para-Informitica
Clases lógica
circuitos-lgicos-presentation

Lógica proposicional; formas normales

Tautología
Una expresión lógica es una tautología si es verdadera para todas las asignaciones posibles.

Nota: 
Si P → Q es una tautología se le llama implicación y se escribe P ⇒Q

Si P ↔ Q es una tautología se dice que es una doble implicación, se escribe P ⇔ Q

La validez es parte de una tautología ya que se da en el razonamiento y puede realizarse mediante las tablas de verdad.

Tarea 2. Ejemplo de Tautología
Aquí esta mi tautología esta esta dada por 3 variables de entrada p,q y r, para realizarla primeramente declare las proposiciones estas son compuestas ya que contienen conectivos lógicos. 

Premisas

P1= p ->q
P2=r -> q
P3 = p V r -> q
PT= q

 Tabla de verdad

 

Referencias:
www.fdi.ucm.es/profesor/rmartine/.../logica_tema1_4.pd

Introducción a la verificación formal

La prueba de software se conoce también como verificación y validación (V&V).

Es asegurar que el sistema de software cumpla las necesidades del usuario

 
Diferencias: 

• Verificación: 

Se conoce como un conjunto de actividades que aseguran que el software implementa correctamente una función especifica, esto nos lleva a cuestionar, ¿Estamos construyendo el producto correctamente?. El software debe estar conforme a las especificaciones.

• Validación:  

¿Se esta construyendo el producto adecuado?"El software debe hacer lo que el usuario requiere. 

Verificación estática y dinámica

•  Verificación dinámica: Se refiere al ejercicio y observación del comportamiento del producto (prueba). 
• Verificación estática: Se refiere al análisis de la representación estática del sistema para descubrir problemas. 

Los procesos de validación y verificación se inician con revisiones de requerimientos, luego se realizan revisiones del diseño e inspecciones de código hasta llegar a la prueba del producto.

El objetivo del proceso de V&V es garantizar la seguridad de que el sistema software esta “hecho para un propósito “, lo cual significa que el sistema debe ser suficientemente bueno para su uso establecido.

  

Pruebas de programas 

Las técnicas dinámicas también conocidas como testing(prueba) se basa en ejercitar una implementación. 

• Puede revelar la presencia de errores no su ausencia
• Una prueba exitosa consiste en descubrir uno o mas errores
• Solo se considera la técnica de validación para requerimientos no-funcionales
• De se usada en conjunto con la verificación estática 

•  Pruebas estadística: Pruebas diseñadas para reflejar la frecuencia de las entradas del usuario.Usadas para estimación de la confiabilidad. 

• Prueba de defectos: Pruebas diseñadas para descubrir defectos en el sistema. Una prueba de defectos exitosa es aquella que revela la presencia de defectos en el sistema.  

Depuración 

• La prueba de defectos y la depuración son distintos procesos
• La prueba de defectos se refiere a la confirmación de la presencia de errores
• La depuración se refiere a la localización y reparación de estos errores.
• La depuración involucra la formulación de una hipótesis acerca del comportamiento del programa y la prueba de la hipótesis para encontrar los errores en el sistema.  

Fases de pruebas

• Pruebas de unidades: prueba de componentes individuales. 
• Pruebas de módulos: prueba de conjuntos de componentes dependientes.
• Pruebas de sub-sistemas: prueba de colecciones de módulos integrados en sub-sistemas.
• Prueba del sistema: prueba del sistema completo ante de su entrega
• Prueba de aceptación: pruebas de los usuarios para verificar que el sistema cumple con los requerimientos. Llamado en ocasiones prueba alfa.  

Ejemplos de mala validación.

1. Marinero sin rumbo (1962)
 
Coste: 18,5 millones de dólares.

Desastre: El cohete Mariner 1, en una investigación espacial destinada a Venus, se desvió de su trayectoria de vuelo poco después de su lanzamiento. El control de la misión destruyó el cohete pasados 293 segundos desde el despegue.

Causa: Un programador codificó incorrectamente en el software una fórmula manuscrita, saltándose un simple guión sobre una expresión. Sin la función de suavizado indicada por este símbolo, el software interpretó como serias las variaciones normales de velocidad y causó correcciones erróneas en el rumbo que hicieron que el cohete saliera de su trayectoria.  El fallo del Pentium en las divisiones largas (1993)
 

Coste: 475 millones de dólares, credibilidad de Intel.

Desastre: el promocionadísimo chip de Intel, Pentium, producía errores al dividir números en coma flotante que se encontraban en un rango determinado. Por ejemplo, dividiendo 4195835,0/3145727,0 se obtenía 1,33374 en lugar de 1,33382, un error del 0,006%. Aunque el error afectaba a pocos usuarios, se convirtió en una pesadilla en cuanto a sus relaciones públicas; con unos 5 millones de chips en circulación, Intel ofreció reemplazar los Pentium sólo de aquellos clientes que demostraran que necesitaban alta precisión en sus cálculos. Finalmente, reemplazó los chips de todos los que lo solicitaron.

Causa: El divisor en la unidad de coma flotante contaba con una tabla de división incorrecta, donde faltaban cinco entradas sobre mil, y que provocaba estos errores en los redondeos. 
Referencias:  
Validación y Verificación  
Pruebas