Italian subtitles

← 02-45 Deduzione Automatica

Get Embed Code
4 Languages

Showing Revision 1 created 02/20/2013 by fabio.

  1. Ti mostro come funziona con un esempio.
  2. Ecco una funzione square-root (radice quadra)
  3. Prende x e ritorna la radice quadrata.
  4. Supponiamo di chiamarla con i valori 2,4 e 16.
  5. Quando chiamiamo square-root con valore 2,
  6. possiamo dedurre che x abbia un valore 2 ed eps abbia un valore di 10 alla -7.
  7. Comunque, questi pattern dovrebbero essere istanziati:
  8. x e' <= di 2 e x >= di 2,
  9. per far si' che questi pattern reggano anche per i valori che abbiamo osservato.
  10. Nella successiva iterazione, chiamiamo square-root con il numero 4,
  11. e ora, essendo l'invariante di x ancora 2, verra' eliminata.
  12. Cio' che abbiamo adesso, comunque, e' che x <= 4 regge ancora.
  13. Lo possiamo fare unendo l'invariante precedente con quella nuova,
  14. e x >= 2 regge ancora con il nuovo valore.
  15. Chiamando square-root(16), terremo ora l'invariante
  16. per cui x <= 16 e >= 2,
  17. e questo e' cio' che avremo alla fine:
  18. x sara' tra 2 e 16 ed eps sempre 10 alla -7.
  19. Come postcondizione avremo degli intervalli simili come valore di rientro.
  20. Il valore di rientro e' tra radice quadra di 2 e 4,
  21. che e' la radice quadra di 16.
  22. Comunque, otteniamo pure che il valore di rientro a radice e' uguale a x
  23. e lo otteniamo perche' Daikon ha un pattern apposito per questo,
  24. ossia un pattern in cui la moltiplica di due variabili qualsiasi corrisponda ad una terza variabile
  25. e cio' e' istanziato con un valore di rientro, di nuovo con un valore di rientro e con x
  26. e questo pattern reggera' per tutte le esecuzioni --
  27. almeno per tutte le esecuzioni con numeri interi.
  28. Se ci mettiamo dentro numeri in virgola mobile, allora entra in gioco eps,
  29. per via degli errori di arrotondamento e quindi questo pattern non verrebbe piu' considerato.
  30. Quindi, qualunque cosa possa produrre Daikon e' ristretto alla sua libreria di pattern,
  31. ma se tu ci aggiungi altri pattern sarai in grado di scoprire piu' proprieta',
  32. a causa delle quali pero', Daikon diventera' piu' lento.
  33. Eppure, anche con un set di pattern perfetto,
  34. gli approcci come questo dipendono dai numeri che effettivamente
  35. ci vengono messi dentro.
  36. Cio' che produce Daikon e' rilevante per tutte le esecuzioni osservate,
  37. ma sappiamo tutti che le precondizioni reali della radice quadrata
  38. non sono ristrette ad uno specifico intervallo di x
  39. a parte che x dev'essere >= 0.
  40. Allo stesso modo, il valore ritornato da square-root non e' necessariamente tra la radice quadra di 2
  41. e la radice quadra di 16,
  42. ma potra' essere qualsiasi cosa che sia > 0.
  43. Quindi, strumenti per la deduzione automatica delle invarianti puo' funzionare bene
  44. se hanno una buona test suite iniziale.
  45. Come possiamo ottentere gli intervalli giusti per x e i valori di rientro?
  46. Chiamando square-root con valore 0?
  47. Chiamando square-root con valore 1?
  48. Chiamando square-root con valore di MAXINT, in cui MAXINT e' il piu' grande numero intero disponibile?
  49. O chiamando square-root con un valore negativo?
  50. Aiutino: ti servono piu' chiamate.
  51. Segna quelle che ti servono ad ottenere i giusti intervalli. Tocca a te.