En ingeniería de software un método formal es un camino a la construcción y análisis de modelos matemáticos que permitan una automatización del desarrollo de sistemas informáticos. Los métodos formales se caracterizan por emplear técnicas y herramientas matemáticas para lograr una facilitación a la hora de encarar la construcción o el análisis de un modelo matemático de un sistema.
En 1967, Robert Floyd propuso utilizar lo que se denominó método de aserciones intermedias como una manera de estudiar las propiedades de los programas. Destacó la posibilidad de definir la semántica de las operaciones mediante reglas lógicas afirmando que estas aserciones son válidas después de ejecutarse las operaciones basándose en la información de las aserciones que son válidas antes de ejecutarse dichas operaciones.
Estas ideas fueron perfeccionadas por Hoare dando lugar al método axiomático (precondiciones E/S) donde introdujo la idea de "invariante".
En 1976, Edsger Dijkstra, presentó un método formal llamado precondición más débil, basado en la transformación de predicados wp (weakest precondition). De esta manera rompía con las ideas de verificación a posteriori de Floyd y Dijkstra. La idea principal era invertir los métodos de ambos de tal manera que se pudiera derivar la precondición a partir de la postcondición.
Entre los métodos de verificación más utilizados, se encuentran:
Basado en la lógica de Hoare. El programa, en lógica de Hoare, se específica mediante aserciones que relacionan las entradas y salidas del programa. Se garantiza que si la entrada actual satisface las restricciones de entrada (precondiciones) la salida satisface las restricciones de salida (poscondiciones).
Se utiliza una expresión del tipo P{programa}Q, siendo P y Q aserciones de la lógica, para indicar que si P es cierto antes de la ejecución del programa y dicho programa termina, entonces Q es cierto tras la ejecución de dicho programa. Este método permite tanto la corrección parcial como total de los programas.
Un caso especial son los bucles, donde los predicados deben mostrar una relación invariante, es decir, deben ser ciertos independientemente del número de vueltas del bucle, por lo tanto el predicado debe cumplir lo siguiente:
Básicamente, consiste en dada una poscondición POST, encontrar, operando hacia atrás, un programa S tal que wp(S, POST) (la precondición) se satisfaga en un amplio conjunto de situaciones
Dada una proposición (P) S (Q) donde S es un conjunto de sentencias de un módulo de un programa, y donde P y Q son los predicados que se cumplen antes y después de S respectivamente, se dice que P es la precondición más débil (wp) de S, si es la condición mínima que garantiza que Q es cierto tras la ejecución de S.
La inducción estructural es una técnica de verificación formal que se basa en el principio de inducción matemática.
Dado un conjunto S con una serie de propiedades y una proposición P que se desea probar, la inducción matemática:
La clasificación más común se realiza en base al modelo matemático subyacente en cada método, de esta manera podrían clasificarse en:
Escribe un comentario o lo que quieras sobre Métodos formales (directo, no tienes que registrarte)
Comentarios
(de más nuevos a más antiguos)