Tema 8

Tema 8:Verificacion de

programas.Introduccion

Joaquın BorregoDıaz

Outline

Motivacion

Definiendo lacorreccion

Formalismos yproblemas

Semantica yprogramacion

Ejemplos

Programas noverificables

Tema 8: Verificacion de programas.Introduccion

Ciencias de la Computacion 2012-13

Joaquın Borrego Dıaz

Depto. de Ciencias de la Computacion




Outline

Motivacion




Ejemplos


Motivacion

Definiendo la correccion

Formalismos y problemas

Semantica y programacion

Ejemplos

Programas no verificables




Outline

Motivacion




Ejemplos


Motivacion

I Objetivo: Matematizar, el problema de la correccion,para poder obtener una solucion mecanizada

I Primera formalizacion: Descripcion del problema X (E :entradas, S : salidas):

I Descripcion funcional: fX : E → SI Descripcion relacional RX ⊆ E × S

I Programa en un modelo de computacion, mododeterminista: Produce funciones

p→ fp

I Programa en un modelo de computacion, modo nodeterminista: Produce relaciones entre estados,

fp ⊆ E × P(S)




Outline

Motivacion




Ejemplos


Dos cuestiones

I Correccion parcial:I En la descripcion funcional (modo determinista)

∀x ∈ E [fp(x) ↓=⇒ fp(x) = fX (x)]

I En la descripcion relacional (modo no determinista)

∀x ∈ E [fp(x) ↓=⇒ ∀y ∈ fp(x) [xRX y ]]

I Parada:I Modo determinista, ∀x ∈ E [ fp(x) ↓]I Modo no determinista, condicion fuerte:

∀x ∈ E [{↑} /∈ fp(x)]

I Modo no determinista, condicion debil:

∀x ∈ E [{↓} ∈ fp(x)]




Outline

Motivacion




Ejemplos


Limitaciones computacionales: Irresolubilidadalgorıtmica

I Correccion parcial: dada f computable,

{p ∈ Programas : fp ⊆ f }

no es recursivo (ni siquiera recursivamente enumerable)

I Parada:

{p ∈ Programas : ∀x ∈ N fp(x) ↓}

no es recursivo (ni recursivamente enumerable)

I Consecuencia: solo podemos esperar obtenerprocedimientos de semidecision y parciales




Outline

Motivacion




Ejemplos


Especificacion de un problema

I Especificacion: coleccion de criterios que, si losatisface el programa, lo calificamos de correcto

I Se necesita un lenguaje de especificacion

I Calidad de la especificacion:

Mayor abstraccion posible (evitamos manejarpropiedades de la maquina donde se ejecuta)

Grado de detalle de la especificacion:

+ detalle =⇒ − manejable; − detalle =⇒ + manejable

(inconveniente: perdida de informacion, especificacion incorrecta)

I Cuestiones acerca de las especificaciones: ¿Completa?¿Aplicable? ¿Consistente?

I Calidad de la implementacion: correccion conrespecto a requerimientos, etc.




Outline

Motivacion




Ejemplos


Representacion

I Formalismos internos (p.e. la logica de Hoare)

Analizan el comportamiento de instrucciones

I Formalismos externos (p.e. la logica temporal)

Analizan el efecto de la ejecucion de modulos delsistema sobre el estado actual

I Problemas de la representacion:I ¿Podemos asegurar que la especificacion expresa

correctamente la intencion intuitiva?I ¿Cual es el grado de especificacion aceptable?I ¿Se pueden especificar cualquier tipo de sistemas?




Outline

Motivacion




Ejemplos


Tres enfoques

I Teorıa: Prueba = correccion

Desarrollo matematico

I Cientıfico correccion experimental

Estudio matematizado de la relacion entrada/salida

I Ingenierıa: Diseno de sistemas correctos

Programar a partir de la especificacion




Outline

Motivacion




Ejemplos


Enfoque teorico

I Idea: seguir en la verificacion de programas el metododeductivo matematico,

Programar = Demostrar

I Aproximacion debida a R. Floyd y C.A.R. Hoare:

Programacion Matematicas

Leng. de programacion Leng. MatematicoPropiedades de instr. basicas Axiomas

Especificacion Teorema

I Formalizacion (sintaxis):I Lenguaje preciso de programacionI Especificacion de las propiedades (Logica)

I Semantica:I Semantica de los formalismos matematicosI Expresion de la correccion




Outline

Motivacion




Ejemplos


Enfoque cientıfico-empırico

I Descubrir errores mediante un gran numero deejemplos-tests, una vez que se ha disenado elsistema

I Desventajas:I No garantiza la ausencia de errores (errores no

descubiertos mediante tests)I No es eficiente: es necesario generar muchos testsI Una vez construido el sistema, se hacen adaptaciones

para resolver los nuevos errores, lo que lo hace mascomplejo

I Conclusion:

El testeo puede ser un metodo muy efectivo paramostrar la presencia de errores, pero es completamenteinadecuado para justificar la ausencia de estos

(E. Dijkstra)

Siempre existe un error mas




Outline

Motivacion




Ejemplos


Enfoque Cientıfico/Ingenierıa

I Revisar junto a disenarI Producir software integrando los procesos de

salvaguardia y calidadI Coste economico mas reducidoI Software mas seguroI Inconveniente: complejidad formal

I Solucion: Mecanizar la verificacion

I Consecuencia: Es necesario disenar sistemas deverificacion automatica




Outline

Motivacion




Ejemplos


Programacion verificable




Outline

Motivacion




Ejemplos


Semantica

I Lenguaje de programacion: Lenguaje para ladescripcion de procesos dinamicos (variables en eltiempo), relacionados con la nocion de ejecucion poruna maquina

I Semantica de los lenguajes:I Semantica operacional: asociada a la descripcion

funcionalI Semantica relacional: asociada a la descripcion

relacionalI Otros...

I Necesitamos Reglas que describen la correspondenciaentre programas y especificaciones




Outline

Motivacion




Ejemplos


Problemas relacionados

I Sıntesis: Dada ϕ especificacion, construir un programap correcto segun ϕ (satisface ϕ)

I Analisis: Dado p, construir la especificaciondemostrable mas adecuada para describir sucomportamiento

I Verificacion de propiedades: Dados p y ϕ, ¿psatisface ϕ?

I Equivalencia: Dados p y p′ y una especificacion ϕ,

¿Son p y p′ equivalentes segun ϕ?

I Optimizacion: Dado p, disenar un programaequivalente mejor, segun cierta medida de complejidad

I Depuracion: Dado p que no satisface ϕ, modificar ppara satisfacer ϕ




Outline

Motivacion




Ejemplos


Observaciones

I Son problemas indecidibles, en general

I No estudiaremos eficienciaI Herramientas fundamentales:

I

I Induccion computacional (sobre la ejecucion)I Induccion estructural (sobre la sintaxis de

programas/especificaciones)

I Dos situaciones de partida:I Caso a posterioriI Caso constructivo: construir el programa junto con la

especificacion.




Outline

Motivacion




Ejemplos


Correccion constructiva versus a posteriori

Algoritmo clasico A1 de la multiplicacion

Funcion mult1(x , y)si y = 0 entonces devolver 0si no

i ← xj ← ymientras j > 1 hacer

i ← i + xj ← j − 1

devolver i

Viene de que la aplicacion f caracterizada por

1. f (x , 0) = 0, ∀x ∈ N.

2. f (x , y + 1) = f (x , y) + x , ∀x , y ∈ N.

define el producto de dos numeros naturales. A1 escorrecto, ya que ha sido disenado mediante una definicion“constructiva” de f .




Outline

Motivacion




Ejemplos


Multiplicacion rusa

Funcion mult2(x , y)Vector A, Bsi x = 0 entonces devolver 0si x = 1 entonces devolver ysi no

A[1]← x ; B[1]← yi ← 1

mientras A[i ] > 1 hacerA[i + 1]← A[i ]div2B[i + 1]← B[i ] + B[i ]i ← i + 1

prod ← 0i ← i − 1

mientras i > 0 hacersi A[i ] 6= A[i ]div2 + A[i ]div2 entonces

prod ← prod + B[i ]i ← i − 1

devolver prod

Para x = 52 e y = 27

52 2726 54

→ 13 1086 216

→ 3 432

→ 1 864

52 · 27 = 108 + 432 + 864 =

= 1404




Outline

Motivacion




Ejemplos


Correccion parcial

Teorema: Si A2 para sobre (x , y) ∈ N× N, entoncesdevuelve x · y . Es decir, fA2(x , y) = x · y .

I Demostracion:

Si x = 0, trivial

I Si x > 0, entoncesx = ak2k + ak−12k−1 + · · ·+ a222 + a12 + a0 ai ∈{1, 0} ak = 1

Observese que 2k ≤ x < 2k+1. Por tanto k = blog2xc,que notaremos por log2(x).

I Las columnas A y B

A[1] = 2k + ak−12k−1 + · · ·+ a222 + a12 + a0 B[1] = yA[2] = 2k−1 + ak−12k−2 + · · ·+ a22 + a1 B[2] = 2 · yA[3] = 2k−2 + ak−12k−3 + · · ·+ a2 B[3] = 2 · B[2] = 22 · y. . . . . .A[k] = 2 + ak−1 B[k] = 2k−1yA[k + 1] = 1 B[k + 1] = 2ky




Outline

Motivacion




Ejemplos


Correccion total: Parada

Para cada j = 1, . . . , k + 1 se verifica:

A[j ] es impar⇐⇒ aj−1 6= 0⇐⇒ aj−1 = 1

Por tanto,fA2(x , y) =

∑A[j] impar

1 ≤ j ≤ k + 1

B[j ] =∑

aj−1 = 11 ≤ j ≤ k + 1

2j−1 · y =

=∑

1 ≤ j ≤ k + 1

aj−1 · 2j−1y

= y ·∑

1 ≤ j ≤ k + 1

aj−1 · 2j−1 = y · x

Teorema (Prueba de parada): El algoritmo A2 para sobretodo (x , y) ∈ N× N.Demostracion: Los dos bucles considerados constan, a losumo, de k + 1 = 1 + log2(x) pasos.




Outline

Motivacion




Ejemplos


Ejemplo: Error del procesador Pentium

I Ano 1994, 67.000 millones de pesetas)

I Algoritmo de division del procesador (Calculo de pd ):

Division SRT4(p, d)p0 ← pPara cada k = 1, ... hacerdeterminar qk ∈ {−2,−1, 0, 1, 2} tal quesi pk+1 = 4(pk − qkd), entonces |pk+1| ≤ 8

3 d

I Se verifica quep

d=

∑i∈N

qi

4i

I Propiedad: |pk | ≤ 83 d =⇒ |pk − qkd | ≤ 2

3Para algun qk ∈ {−2,−1, 0, 1, 2}




Outline

Motivacion




Ejemplos


Ejemplo (cont.)I Si pk+1 = 4(pk − qkd) y |pk+1| ≤ 8

3d , entonces

pk

d4−k =

qk

4k+

pk + 1

d4−(k+1)

Aplicando induccion pd

= (q0 + · · ·+ qk−1) + pkd

4−k y por lımite setiene la igualdad

I Eleccion del qk (unidad: d/3):

I El algoritmo elegıa 0 en vez de 2 para ciertos numeros en [5/3, 8/3],debido a errores de precision




Outline

Motivacion




Ejemplos


Otros ejemplos

I 1985-87, Canada: Fallo en el software de un emisor derayos para el tratamiento del cancer: cuatro muertos

I Banco de Nueva York: En el contador de mensajes decompra/venta:

32767 + 1 = 0

I Perdida de la nave Phobos (U. Sovietica, 1988)

I Un sımbolo: Explosion de la lanzadera espacial

Verificacion de propiedades para sistemas con numerofinito de estados, pero existen 1010 estados o mas

I Ariane 5: mal envıo de la altitud correcta

I Los errores tienen su causa en una deficiente verificacion

I Costes en EEUU: 300.000 millones de pesetas en 2002

I Costes en UK: 900 millones de pesetas (2002)




Outline

Motivacion




Ejemplos


Verificacion en la NASA




Outline

Motivacion




Ejemplos


Programas no verificables

I (Fijamos x > 1) Procedimiento 1: Dado n > 0,aplıquese recursivamente la siguiente regla:

Escribir n en base x, aumentar en 1 la base, y restarle 1al nuevo numero

I Ejemplo: si n = 20098, y x = 3, entonces

n = 39 + 35 + 34 + 32 + 30

y el resultado es 49 + 45 + 44 + 42 + 40 − 1

I (Goodstein) Procedimiento 2: similar al 1, pero seaplica la regla al numero escrito en base x pura:

I En el caso anterior, n = 332+ 331+2 + 33+1 + 32 + 30

y el resultado es n = 442+ 441+2 + 44+1 + 42 + 40 − 1

I

Teorema: Despues de un numero finito de pasos los pro-cedimientos anteriores paran, llegando a 0




Outline

Motivacion




Ejemplos


Programas no verificables (II)

I Consecuencia del teorema de la forma normal:Cualquier programa aritmetico se puede traducir a unaformula Σ1, esto es, formulas del tipo

∃~xϕ(~y ,~x)

donde ϕ solo posee cuantificadores acotadosI Existe traduccion p ∈ Programas 7→ ϕp tal que:

I Es automatica (mecanizable)I Se tiene que para cualesquiera ~x , y ∈ N

[[p]](~x) = y⇐⇒ N |= ψp(~x, y)




Outline

Motivacion




Ejemplos


Imposibilidad de verificacion

I Teorema: Supongamos que la teorıa deespecificaciones solo admite induccion sobre formulasΣ1. Entonces el sistema no puede demostrar que elprocedimiento 1 para

I Potencia de ese sistema: Programas LOOP, funcionesprimitivas recursivas

I Teorema: Supongamos que la teorıa deespecificaciones admite induccion sobre cualquierformula aritmetica. Entonces el sistema no puededemostrar que el procedimiento 2 para

I El sistema es la Aritmetica de Peano.I Para demostrar la parada se necesita usar tecnicas de

teorıa de conjuntos

Tema 8

Education

Transcript of Tema 8