Scribd
Cargar
69 vistas1 página

Verificación Formal de Algoritmos

La verificación formal de algoritmos es una técnica basada en lógica de primer orden y lógica de Hoare para demostrar la corrección de un algoritmo antes de su ejecución. Utiliza la lógica de Hoare y la noción de triplete "precondición-instrucción-poscondición" para verificar que un programa cumple con ciertas propiedades formales. El análisis de algoritmos estudia la complejidad temporal y espacial de los algoritmos.

Cargado por

vlado3
Derechos de autor
© © All Rights Reserved
Nos tomamos en serio los derechos de los contenidos. Si sospechas que se trata de tu contenido, reclámalo aquí.
Formatos disponibles
Descarga como PDF, TXT o lee en línea desde Scribd
69 vistas1 página

Verificación Formal de Algoritmos

La verificación formal de algoritmos es una técnica basada en lógica de primer orden y lógica de Hoare para demostrar la corrección de un algoritmo antes de su ejecución. Utiliza la lógica de Hoare y la noción de triplete "precondición-instrucción-poscondición" para verificar que un programa cumple con ciertas propiedades formales. El análisis de algoritmos estudia la complejidad temporal y espacial de los algoritmos.

Cargado por

vlado3
Derechos de autor
© © All Rights Reserved
Nos tomamos en serio los derechos de los contenidos. Si sospechas que se trata de tu contenido, reclámalo aquí.
Formatos disponibles
Descarga como PDF, TXT o lee en línea desde Scribd

Analisis y verificacion de algoritmos

Instrucción

Verificación formal de algoritmos Analisis de algoritmos

es una técnica (basada en Lógica de Primer Orden y en la Lógica de Hoare) para


demostrar la correctitud de un algoritmo previo a su ejecución

lenguaje GCL hace uso de logica de Hoare


(lenguaje de comandos guardados)
es la terna o triplete “{Q} S {R}”

Propiedades Precondición vacia


La tripla {falso}S{R}es válida
lèxico Semantica
Sintaxis
es
Precondicion{Q} Condicon antes de ejecutar el programa
Ley del milagro excluido
La tripla {Q}S{falso} es válida si y solo si [Q ≡ falso]
sentido o interpretación de signos lingüísticos como :
Vocabulario o conjunto de palabras y simbolos validos
símbolos, palabras, expresiones o representaciones formales.
programa que se ejecuta
S,,,Sn instrucción(S)
Fortalecimiento de precondición
Si [P ⇒ Q] y {Q}S{R} es válida, entonces también es válida {P}S{R}.

poscondicion{R} Condicon despues de ejecutar el programa

Debilitamiento de poscondición
Modo de combinarse y ordenarse las palabras Si [R ⇒ P] y {Q}S{R} es válida, entonces también es válida {Q}S{P}
y las expresiones

Conjunción de poscondiciones
Corrección y verificacion
Precondicion más débil Si {Q}S{R} y {Q}S{P} son válidas, entonces también es válida {Q}S{R ∧ P}
de programas hace uso de

funcion
Disyunción de precondiciones
Si {Q}S{R} y {P}S{R}son válidas, entonces también es válida{Q ∨ P}S{R}
w(intruccion,poscondicon)

Instrucción que no tiene efecto


Instrucción vacía alguno sobre el estado o la ejecución
del programa

Asignación

Instrucción condicional

Ciclos

También podría gustarte