YouTube

Got a YouTube account?

New: enable viewer-created translations and captions on your YouTube channel!

Italian subtitles

← 02-46 Soluzione di Deduzione Automatica

Get Embed Code
4 Languages

Showing Revision 2 created 06/24/2014 by Fran Ontanaya.

  1. Grazie mille, ed ora le risposte.
  2. Le risposta e' che se vogliamo avere delle variabili in input entro intervalli giusti
  3. cosi' come per le variabili di output,
  4. abbiam bisogno di inserire questi intervalli per le chiamate a square-root.
  5. Nel nostro caso, l'intervallo giusto per x e' tra 0 e MAXINT.
  6. Se chiamiamo square-root(0) e square-root con l'intero maggiore,
  7. cio' che otterremo sara' x >=0
  8. e x <= MAXINT,
  9. che e' effettivamente l'intervallo giusto.
  10. Allo stesso modo, abbiamo imparato che il valore di rientro e' sempre >= 0
  11. ed e' sempre <= della radice quadrata di MAXINT.
  12. Se chiamassimo square-root con valore 1, non cambierebbe molto le cose,
  13. allargheremo leggermente l'intervallo ma non avremmo lo 0 qui.
  14. Questo non e' veramente necessario:
  15. se chiamiamo square-root con -1 violeremo in effetti la precondizione implicita,
  16. sperando che square-root in effetti si blocchi
  17. di modo che Daikon riesca a dedurre che se chiamiamo square-root
  18. con valori negativi questa si blocca. Questi due sono i valori esatti.