IT/Tutorial/parity.tex

2 \chapter{Esempio: un Semplice Validatore di Parit�}\label{parity}
4 Questo capitolo consiste di un esempio pratico: la specifica e
5 la verifica di un semplice validatore di parit� sequenziale. L'intenzione �
6 di ottenere due cose:
9 \item Presentare un pezzo completo di lavoro con \HOL.
10 \item Dare una sensazione di cosa vuol dire usare il sistema \HOL\ per
14 Per quanto riguarda (ii), si noti che bench� i teoremi dimostrati siano, di fatto,
15 piuttosto semplici, il modo in cui essi sono dimostrati illustra il genere intricato di
18 proposito di illustrare varie caratteristiche di \HOL. Si spera che il
19 semplice esempio qui illustrato dar� al lettore la sensazione di cosa significhi fare
20 una dimostrazione di grandi dimensioni.
23 di imparare qualcosa circa il sistema \HOL{} anche se non desiderano
24 penetrare i dettagli dell'esempio sul validatore di parit� qui usato. La
25 specifica e la verifica di un validatore di parit� pi� complesso
30 Le sessioni di questo esempio comprendono la specifica e
31 la verifica di un dispositivo che calcolata la parit� di una sequenza di
32 bit. Pi� precisamente, � data una verifica dettagliata di un dispositivo
35 {\small\verb|T|} se e solo se c'� stato un numero pari di
36 input di {\small\verb|T|} su {\small\verb|in|}. E' costruita una teoria chiamata
38 la verifica del dispositivo. Tutti gli input \ML{} nei riquadri di sotto
40 suggerisce al lettore di inserire interattivamente questo per avere una
41 sensazione `pratica' dell'esempio. L'obiettivo del caso di studio � di illustrare
46 Il primo passo � avviare il sistema \HOL{}. Usiamo di nuovo
53 $n f$ � vero se il numero di {\small\verb|T|} nella sequenza
74 L'effetto della nostra chiamata a {\small\verb|Define|}  � di archiviare la
75 definizione di {\small\verb|PARITY|} nella teoria corrente con il nome
76 {\small\verb|PARITY_def|} e di legare il teorema di definizione alla variabile \ML\
77 con lo stesso nome. Si noti che vengono scritti due tipi di
79 delle variabili in \ML. L'utente in genere � libero di gestire questi nomi
81 lessicali), ma una convenzione comune � (come in questo caso) di dare alla
82 definizione di una costante {\small\tt CON} il nome
84 convenzione usata comunemente � di usare solo {\small\verb|CON|} per la
85 teoria e il nome \ML{} della definizione di una costante
87 convenzione uniforme, ma agli utenti si raccomanda di adottarne una. In questo
92 La specifica del dispositivo di controllo di parit� pu� ora essere data come:
102 soddisfatta se le funzioni di segnale\footnote{I segnali sono modellati come funzioni
135 \noindent La dimostrazione di questo pu� essere fatta per Induzione Matematica e, bench�
136 banale, � una buona illustrazione di come tali dimostrazioni sono fatte. Il
137 lemma � dimostrato interattivamente usando il pacchetto subgoal di \HOL. La dimostrazione
206 sono riportate numerate sotto le linee di trattini orizzontali.
209 definizione di {\small\verb|PARITY|}.
231 mette il teorema dimostrato in uno stack di teoremi). Il nuovo goal principale �
232 il caso di passo dell'induzione. Questo goal � anch'esso risolto per riscrittura.
253 \noindent Il goal � dimostrato, \ie\ � prodotta la lista vuota di subgoal.
254 Il sistema ora applica le funzioni di giustificazione prodotte dalle
255 tattiche alla lista di teoremi ottenendo i subgoal (iniziando con
288 Il lemma appena dimostrato suggerisce che il checker di parit� pu� essere
289 implementato mantenendo il valore di parit� in un registro e poi
294 registro, perch� l'output del validatore di parit� al tempo
297 validatore di parit� al tempo {\small\verb|t|} � una funzione dell'input al
301 Il diagramma schematico di sotto mostra il disegno di
303 (L'input pi� a sinistra di \ml{MUX} � il selettore.)
310 dopo restituisce sempre {\small\verb|T|}. Il suo ruolo � solo quello di assicurare che il
315 valore di parit� archiviato (se l'input corrente � {\small\verb|F|}) oppure il
316 complemento di questo valore (se l'input corrente � {\small\verb|T|}).
369 di un segnale {\small\verb|out|} se per tutti gli istanti {\small\verb|t|} il valore di
380 \noindent Si noti che, come discusso di sopra, `{\small\verb|ONE_def|}' � usato sia
383 le ambiguit� di tipo; senza questa (o qualche altra informazione) il
384 controllore di tipo non sarebbe in grado di dedurre che {\small\tt t} deve avere
387 Il predicato binario {\small\verb|NOT|} � vero di una coppia di segnali
388 {\small\verb|(inp,out)|} se il valore di {\small\verb|out|} � sempre
389 la negazione del valore di {\small\verb|inp|}. Gli invertitori sono cos�
391 modello di livello registro-trasferimento, ma non per un livello inferiore.
420 elementi unit� di ritardo; i valori restituiti come output al tempo {\small\verb|t+1|} sono
439 Il diagramma schematico di sopra pu� essere rappresentato come un predicato
473 schematico (\ie\ come nella definizione di {\small\verb|PARITY_IMP|}),
475 coppia di segnali {\small\verb|(inp,out)|} soddisfa la specifica.
478 di parit� segue da questo e da {\small\verb|UNIQUENESS_LEMMA|} per la
479 transitivit� di {\small{\tt\verb+==>+}}.
500 seguita da una decomposizione del goal risultante per mezzo di
501 {\small\verb|STRIP_TAC|}. E' usata la tattica di riscrittura
503 incorporata, ma solo quelle date esplicitamente nella lista di
583 		{\small\verb|PAT_ASSUM|}. Questa tattica � di tipo \ml{term -> thm
609 assunzioni non ha un lato destro che appare come l'applicazione di una
611 potrebbe comunque essere visto uguale all'applicazione di \emph{qualche}
615 Ispezionando il goal di sopra si pu� vedere che il prossimo passo � di
686 Una volta in possesso di {\small\verb|PARITY_LEMMA|}, il teorema finale � facilmente
702 dispositivo di controllo di parit�.
716 {\small\verb|RESET_REG|} con un input {\small\verb|inp|}, linea di ripristino
724 	{\small\verb|t|} o {\small\verb|t+1|}, allora il valore di output in
726 	altrimenti � uguale al valore di input al tempo {\small\verb|t|} su
744 La soluzione all'esercizio dovrebbe essere la definizione di un predicato
745 {\small\verb|RESET_REG_IMP|} come una quantificazione esistenziale di una
746 congiunzione di applicazioni di {\small\verb|ONE|}, {\small\verb|NOT|},
747 {\small\verb|MUX|} e {\small\verb|REG|} a nomi di linea
748 adatti\footnote{Cio�  una definizione della stessa forma di
754 }, insieme con una dimostrazione di:
766 \item Specificare formalmente un validatore di parit� azzerabile che ha due input
771 		un numero pari di input {\small\tt T} in {\small\tt inp}
775 \item Sviluppare un'implementazione di questa specifica costruita usando {\it