1 Extracción dinámica de Invariantes Edgar Miranda Rafael Corchuelo Departamento de lenguajes y sistemas informáticos

2 Índice de contenidos Introducción Algoritmo Daikon Aplicación Conclusiones

3 Índice de contenidos Introducción Algoritmo Daikon Aplicación Conclusiones

4 Introducción  Invariante – RAE: Magnitud o expresión matemática que no cambia de valor al sufrir determinadas transformaciones. – En el documento, tomamos las precondiciones y poscondiciones como invariantes – Podemos definir invariantes en otros puntos del programa -> invariantes de bucle

5 Introducción Un ejemplo: Precondiciones: N>=0 Poscondiciones: S= (∑j: 0

6 Introducción ¡Invariantes declaradas implícitamente!

7 Índice de contenidos Introducción Algoritmo Daikon Detalles concretos Aplicación Conclusiones

8 Algoritmo Daikon Estructura del algoritmo

9 Algoritmo Daikon Posible solución al programa void sumaBucle(int B[], int N){ int S; for(int I=0; I

10 Algoritmo Daikon Tipos de invariantes Tipo de InvarianteEjemplo Una variable numéricaX=a Dos variables numéricasX=a*Y Tres variables numéricasX=a*Y+b*Z+c Una variable cualquieraX Є {a,b,c} Una secuenciaSeq in [a..b] Dos secuenciasSeq1 reverse Seq2

11 Algoritmo Daikon ¿Cómo funicona Daikon? Instrumentación del programa original void sumaBucle(int B[], int N){ int S; for(int I=0; I

12 Algoritmo Daikon ¿Cómo funciona Daikon? Extracción de las invariantes – Conjunto de entrenamiento Orig(N)Orig(B)Orig(S)NBS 4{1,2,3,1}04 7 4{1,2,3,4}04 10 3{2,4,5}03 11

13 Algoritmo Daikon ¿Cómo funciona Daikon? Extracción de las invariantes Orig(N)Orig(B)Orig(S)NBS 4{1,2,3,1}04 7 4{1,2,3,4}04 10 3{2,4,5}03 11 Conjunto de Invariantes Orig(N)=N Orig(B)=B N=4 B in [1..3] ….

14 Algoritmo Daikon ¿Cómo funciona Daikon? Extracción de las invariantes Conjunto de Invariantes Orig(N)=N -> correcta Orig(B)=B -> correcta N=4 -> correcta B in [1..3] -> fallo …. Orig(N)Orig(B)Orig(S)NBS 4{1,2,3,1}04 7 4{1,2,3,4}04 10 3{2,4,5}03 11

15 Algoritmo Daikon ¿Cómo funciona Daikon? Extracción de las invariantes Conjunto de Invariantes Orig(N)=N -> correcta Orig(B)=B -> correcta N=4 -> fallo …. Orig(N)Orig(B)Orig(S)NBS 4{1,2,3,1}04 7 4{1,2,3,4}04 10 3{2,4,5}03 11

16 Algoritmo Daikon ¿Cómo funciona Daikon? Conjunto de invariantes obtenidas Conjunto de Invariantes Orig(N)=N -> correcta Orig(B)=B -> correcta ….

17 Algoritmo Daikon ¿Cómo de fiable es Daikon? Fiabilidad de las invariantes Orig(N)Orig(B)Orig(S)NBS 4{1,2,3,1}04 7 4{1,2,3,4}04 10 4{2,4,5,1}04 12 Problema!! Con este conjunto de entrenamiento obtenemos la invariante N=4

18 Algoritmo Daikon ¿Cómo de fiable es Daikon? Solución propuesta – Para cada una de las invariantes, calculamos la probabilidad de que sea errónea y la comparamos con una variable de fiabilidad Invariantes: N in [a..b] -> correcta N!=0 -> ¿es correcta? Calculamos probabilidad N!=0 probabilidad N=0 -> 1/(b-a+1) probabilidad N!=0 -> 1- 1/(b-a+1) probabilidad N!=0 en k casos -> P=(1-1/(b-a+1))^k Tenemos que si P

19 Algoritmo Daikon Eficiencia de Daikon Elementos positivos – El coste computaciones es proporcional al número de invariantes y este va decreciendo – En cada punto de controlo sólo tenemos en cuenta las variables visibles Elementos negativos – Se derivan invariantes innecesarias. Por ejemplo N!=B[0]

20 Índice de contenidos Introducción Algoritmo Daikon Aplicación Conclusiones

21 Aplicación ¡¿Cómo encaja todo esto en el problema de la extracción de información?!

22 Aplicación Introducción No es necesario realizar el proceso de instrumentación

23 Aplicación Funcionamiento aplicado CONJUNTO DE ENTRENAMIENTO Detección de datos incorrectos

24 Aplicación Problema en la web Daikon supone que los datos son correctos – En la web los datos pueden contener ruido

25 Aplicación Problema en la web Dos tipos de invariantes – Intrínsecas – Accidentales Conjunto de entrenamiento Dividimos el conjunto de entrenamiento en suconjuntos

26 Índice de contenidos Introducción Algoritmo Daikon Aplicación Conclusiones

27 Daikon proporciona método efectivo para extracción de invariantes – Podemos aplicarlo en el proceso de verificación de información Problemas con la eficiencia – Se proponen mejoras Problemas con la fiabilidad – Se proponen mejoras

28 ¿Preguntas?