La tripla {Q}S{R} es una expresión lógica que es válida cuando el programa S es correcto con respecto a su especificación Q y R. El programa S es correcto si y solo si al ser ejecutado sobre cualquier estado inicial que satisface la precondición, produce un estado final que satisface la poscondición.

propiedades de las triplas de hoare

Una Tripla de Hoare es una expresión boleana escrita en la forma , {Q}S{R} donde S es un programa, {Q} es una aserción que describe la precondición del programa, y{R} es una aserción que describe la poscondición del programa. La expresión{Q}S{R} se lee textualmente el programa S es correcto con respecto a la precondición Q y a la poscondición R , o simplemente S es correcto con respecto a su especificación. Operacionalmente hablando, {Q}S{R} es verdadero si y sólo si para todo estado que satisface la precondiciónQ , al ejecutar el programa S , se termina, llegando a un estado que satisface la poscondición R .

para una asignación simple: wp(x:=E,Q)= Q[X=E] EJEMPLOS: wp(a:=7,a=7) =(7-7)=true wp(a:=7,a=6)=(7=6)=false wp(a:7,b=c)= (b=c) wp(a:=a-b,a>b)=(a-b>b)=(a>2b) precondición mas debil.

Cota de ciclo

EJEMPLO Ejemplo 1c. Cálculo de la suma de los números naturales entre 1 y n, completamente anotado. {Pre Q: n ≥ 1} program sumatoria input: n:ℤ var: suma:ℤ, i:ℤ suma := 0 i := 1 {Inv P: suma = ⋀ 1≤i≤n+1} {t = (n+1)-i, Tmin = 0} while i ≤ n do suma := suma + i i := i + 1 return suma {Pos R: suma = }