Verificación de programas

la información esta representada por variables

las cuales pueden ser

de entrada

de salida

Conjunto de valores
que toman las variables
en un determinado momento

(Q): Precondición

S: Programa

(R): Poscondición

Propiedades:
Precondición vacia
Ley del milagro excluido
Fortalecimiento de (Q)
Debilitamiento de (R)
Conjunción de (R)
Disyunción de (Q)

Precondición

Es un predicado que define el conjunto de estados iniciales válidos de un programa

Poscondición

Es un predicado que define el conjunto de estados finales aceptados del programa

de una varible

Es el valor que tiene una variable en un momento

Determinado de la ejecución de un algoritmo

de un algoritmo

Es el valor que tienen todas sus variables libres

en un momento determinado de su ejecución

de aserción

Son sentencias lógicas
que hacen referencia aun estado del sistema

Es un predicado que expresa la relación que tienen que cumplir los valores de ciertas variables

Precisión

Orden en la realización

Debe estar correctamente definido

Debe ser finito

Debe tener entrada o inicio

Debe tener Salida o fin

Ordenamiento

se tiene varios tipos de ordenamiento como:

Metodo burbuja

Dividir y conquistar

Teorema maestro

Explicación

Se caracteriza por

centrarse en el por qué

de sí una afirmación es

Verdadera o falsa

Convicción

se basa en

conjeturas desconocidas

demostración de enunciados

Método de Sistematización

simplifica teorias

Ordena enunciados
individuales

Verificación de modelos

se enfoca en reconocer
el modelo matemático

Sea finito

Sea infinito

aumenta o disminuye de acuerdo a las decisiones

Formas de medir la complejidad

Clase P
Clase NP
Clase NP completo
Reduccion de Karp