Verifiche formali di programmi [era: Ripristino GRUB2 e conversione GPT...]
Saluton Marco,
Il 2021-03-01 19:37 Marco Ciampa ha scritto:
ecco, diciamo che lo hai detto meglio ma il "succo" è lo stesso...
perdonami
Non proprio lo stesso...
È un po' come la differenza tra "in Italia ci sono dei mafiosi" e "gli
italiani sono tutti mafiosi". Il non distinguere tra le due di solito
porta a gravi conseguenze :-P
...e non solo parlando di Italia e di mafia.
Per fare un esempio che potrebbe non interessare molte persone, ma che
affascina enormemente me, c'è un'intera libreria di calcolo matematico
in
precisione arbitraria che è formalmente verificata:
https://gitlab.inria.fr/why3/whymp
Interessante. Domanda da profano: verifica formale equivale ad assenza
di
bachi o semplicemente indica che quello che viene descritto
nell'algoritmo (che potrebbe avere dei problemi) viene correttamente
Per fare un esempio interno alla libreria citata, la verifica formale
fatta dagli autori (pubblicata e riproducibile) di una funzione come
"radice quadrata intera di un intero" garantisce che la funzione non
legga/scriva in aree di memoria diverse da quelle in cui può
leggere/scrivere. Garantisce anche che per qualunque intero
"arbitrariamente" lungo x fornito come argomento, venga fornito nel
formato atteso un risultato r tale che r^2 <= x < (r+1)^2.
Certo, se qualcuno usa la funzione powm per l'esponenziazione modulare
da quella libreria e ci costruisce sopra della crittografia RSA; la
libreria garantirà che le potenze-modulo diano il risultato
matematicamente corretto partendo da quel che le verrà dato in pasto. Se
pero il programma che usa la libreria è sbagliato o la crittografia RSA
non è sicura, non sarà l'uso di una libreria formalmente verificata ad
eliminare questi problemi.
Perché questa chiacchierata non scivoli troppo nel fuori luogo (Off
Topic), l'infrastruttura di programmi che serve per verificare queste
dimostrazioni è presente in Debian, nel pacchetto why3
https://packages.debian.org/source/sid/why3
Un primo germe della libreria che ho indicato è presente nel pacchetto
why3-examples ed una volta installatolo si trova in
/usr/share/doc/why3-examples/examples/multiprecision
Per un matematico
0,99999999999999999999999999999999999999999999999999999999999999\
9999999999999999999999999999999999999999999999999999999999999999\
9999999999999999999999999999999999999999999999999999999999999999
è completamente diverso da 1. Dillo ad una cassiera del supermercato e
sta pronto ad abbassare la testa... ;-)
Prova a dirlo tu alla stessa persona che invece di digitare 1 sulla
cassa può tranquillamente scrivere 0 seguito dalla sfilza di 9 che hai
proposto, oppure prova a dirlo ad una tipografa che quelle tre righe di
9 sono la stessa cosa di un singolo "1" e vedrai che le opinioni in
proposito sono più variegate di quelle che ti aspettavi :-)
Poi suvvia, sono sicuro che esistano anche cassiere del supermercato
acculturate, capaci di cogliere le sottigliezze, come chessò... la
differenza tra software libero e software gratuito! E se per caso la
capacità di discernere non è sufficientemente diffusa, bene adoperiamoci
perché lo sia!
vedi che anche tu guardi le probabilità e non le certezze matematiche?
L'importante è non confonderle!
Ĝis,
m
Reply to: