1 2\chapter{Esempio: un Semplice Validatore di Parit�}\label{parity} 3 4Questo capitolo consiste di un esempio pratico: la specifica e 5la verifica di un semplice validatore di parit� sequenziale. L'intenzione � 6di ottenere due cose: 7 8\begin{myenumerate} 9\item Presentare un pezzo completo di lavoro con \HOL. 10\item Dare una sensazione di cosa vuol dire usare il sistema \HOL\ per 11 una\linebreak dimostrazione complicata. 12\end{myenumerate} 13 14Per quanto riguarda (ii), si noti che bench� i teoremi dimostrati siano, di fatto, 15piuttosto semplici, il modo in cui essi sono dimostrati illustra il genere intricato di 16`ingegnerizzazione della dimostrazione' che � tipico. Le dimostrazioni potrebbero essere 17fatte in modo pi� elegante, ma presentarle in quel modo farebbe fallire il 18proposito di illustrare varie caratteristiche di \HOL. Si spera che il 19semplice esempio qui illustrato dar� al lettore la sensazione di cosa significhi fare 20una dimostrazione di grandi dimensioni. 21 22I lettori che non sono interessati nella verifica dell'hardware dovrebbero essere in grado 23di imparare qualcosa circa il sistema \HOL{} anche se non desiderano 24penetrare i dettagli dell'esempio sul validatore di parit� qui usato. La 25specifica e la verifica di un validatore di parit� pi� complesso 26� lasciato come esercizio (una soluzione � fornita nella directory {\small\verb|examples/parity|}). 27 28\section{Introduzione} 29 30Le sessioni di questo esempio comprendono la specifica e 31la verifica di un dispositivo che calcolata la parit� di una sequenza di 32bit. Pi� precisamente, � data una verifica dettagliata di un dispositivo 33con un input {\small\verb|in|}, un output {\small\verb|out|} e la 34specifica che l'$n$-esimo output su {\small\verb|out|} � 35{\small\verb|T|} se e solo se c'� stato un numero pari di 36input di {\small\verb|T|} su {\small\verb|in|}. E' costruita una teoria chiamata 37{\small\verb|PARITY|}; questa contiene la specifica e 38la verifica del dispositivo. Tutti gli input \ML{} nei riquadri di sotto 39possono essere trovati nel file {\small\verb|examples/parity/PARITYScript.sml|}. Si 40suggerisce al lettore di inserire interattivamente questo per avere una 41sensazione `pratica' dell'esempio. L'obiettivo del caso di studio � di illustrare 42un dettagliato `proof hacking' su un esempio piccolo e abbastanza semplice. 43 44\section{Specifica} 45\label{example} 46Il primo passo � avviare il sistema \HOL{}. Usiamo di nuovo 47\texttt{<holdir>/bin/hol}. Il prompt \ML{} � {\small\verb|-|}, cos� 48le righe che cominciano con {\small\verb|-|} sono digitate dall'utente e le altre 49linee sono le risposte del sistema. 50 51Per specificare il dispositivo, � definita una funzione primitiva ricorsiva 52{\small\verb|PARITY|} cos� che per $n>0$, {\small\tt PARITY} 53$n f$ � vero se il numero di {\small\verb|T|} nella sequenza 54$f${\small\tt (}$1${\small\tt)}, $\ldots$ , $f${\small\tt 55 (}$n${\small\tt)} � pari. 56 57\setcounter{sessioncount}{0} 58\begin{session} 59\begin{verbatim} 60- val PARITY_def = Define` 61 (PARITY 0 f = T) /\ 62 (PARITY(SUC n) f = if f(SUC n) then ~(PARITY n f) else PARITY n f)`; 63Definition has been stored under "PARITY_def". 64> val PARITY_def = 65 |- (!f. PARITY 0 f = T) /\ 66 !n f. PARITY (SUC n) f = 67 (if f (SUC n) then ~PARITY n f else PARITY n f) 68 : thm 69\end{verbatim} 70\end{session} 71 72\noindent 73 74L'effetto della nostra chiamata a {\small\verb|Define|} � di archiviare la 75definizione 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\ 77con lo stesso nome. Si noti che vengono scritti due tipi di 78nome: i nomi delle costanti nelle teorie e i nomi 79delle variabili in \ML. L'utente in genere � libero di gestire questi nomi 80come desidera (a seconda delle varie esigenze 81lessicali), ma una convenzione comune � (come in questo caso) di dare alla 82definizione di una costante {\small\tt CON} il nome 83{\small\verb|CON_def|} nella teoria e anche in \ML. Un'altra 84convenzione usata comunemente � di usare solo {\small\verb|CON|} per la 85teoria e il nome \ML{} della definizione di una costante 86{\small\verb|CON|}. Sfortunatamente, il sistema \HOL{} non usa una 87convenzione uniforme, ma agli utenti si raccomanda di adottarne una. In questo 88caso \ml{Define} ha fatto una delle scelte per noi, ma ci sono 89altri scenari in cui dobbiamo scegliere il nome usato nel file 90della teoria. 91 92La specifica del dispositivo di controllo di parit� pu� ora essere data come: 93 94\begin{hol} 95\begin{verbatim} 96 !t. out t = PARITY t inp 97\end{verbatim} 98\end{hol} 99 100\noindent 101E' {\it intuitivamente\/} chiaro che questa specifica sar� 102soddisfatta se le funzioni di segnale\footnote{I segnali sono modellati come funzioni 103 da numeri, che rappresentano tempi, a booleani.} 104{\small\verb|inp|} e {\small\verb|out|} soddisfano\footnote{Preferiremmo 105 usare \ml{in} come uno dei nomi delle nostre variabili, ma questa � una parola 106 riservata per le espressioni-\ml{let}.}: 107 108\begin{hol} 109\begin{verbatim} 110 out(0) = T 111\end{verbatim} 112\end{hol} 113 114\noindent e 115 116\begin{hol} 117\begin{verbatim} 118 !t. out(t+1) = (if inp(t+1) then ~(out t) else out t) 119\end{verbatim} 120\end{hol} 121 122\noindent Questo pu� essere verificato in modo formale in \HOL{} fornendo il 123seguente lemma: 124 125\begin{hol} 126\begin{verbatim} 127 !inp out. 128 (out 0 = T) /\ 129 (!t. out(SUC t) = if inp(SUC t) then ~out t else out t) 130 ==> 131 (!t. out t = PARITY t inp) 132\end{verbatim} 133\end{hol} 134 135\noindent La dimostrazione di questo pu� essere fatta per Induzione Matematica e, bench� 136banale, � una buona illustrazione di come tali dimostrazioni sono fatte. Il 137lemma � dimostrato interattivamente usando il pacchetto subgoal di \HOL. La dimostrazione 138� avviata mettendo il goal da dimostrare in un goal stack usando la 139funzione {\small\verb|g|} che prende un goal come argomento. 140 141\begin{session} 142\begin{verbatim} 143- g `!inp out. 144 (out 0 = T) /\ 145 (!t. out(SUC t) = (if inp(SUC t) then ~(out t) else out t)) ==> 146 (!t. out t = PARITY t inp)`; 147> val it = 148 Proof manager status: 1 proof. 149 1. Incomplete: 150 Initial goal: 151 !inp out. 152 (out 0 = T) /\ 153 (!t. out (SUC t) = (if inp (SUC t) then ~out t else out t)) ==> 154 !t. out t = PARITY t inp 155\end{verbatim} 156\end{session} 157 158\noindent Il pacchetto subgoal stampa il goal all'inizio del goal stack. 159Il goal principale � espanso eliminando il quantificatore universale 160(con {\small\verb|GEN_TAC|}) e quindi mettendo i due congiunti 161dell'antecedente dell'implicazione nelle assunzioni del goal (con 162{\small\verb|STRIP_TAC|}). La funzione \ML{} {\small\verb|expand|} 163prende una tattica e la applica al goal principale; i subgoal risultanti 164sono immessi nel goal stack. Il messaggio `{\small\verb|OK..|}' � 165stampato appena prima dell'applicazione della tattica. Quindi � stampato 166il subgoal risultante. 167 168 169\begin{session} 170\begin{verbatim} 171- expand(REPEAT GEN_TAC THEN STRIP_TAC); 172OK.. 1731 subgoal: 174> val it = 175 !t. out t = PARITY t inp 176 ------------------------------------ 177 0. out 0 = T 178 1. !t. out (SUC t) = (if inp (SUC t) then ~out t else out t) 179\end{verbatim} 180\end{session} 181 182\noindent Poi � fatta l'induzione su {\small\verb|t|} 183usando {\small\verb|Induct|}, che fa 184l'induzione sulla variabile quantificata universalmente pi� esterna. 185 186\begin{session} 187\begin{verbatim} 188- expand Induct; 189OK.. 1902 subgoals: 191> val it = 192 out (SUC t) = PARITY (SUC t) inp 193 ------------------------------------ 194 0. out 0 = T 195 1. !t. out (SUC t) = (if inp (SUC t) then ~out t else out t) 196 2. out t = PARITY t inp 197 198 out 0 = PARITY 0 inp 199 ------------------------------------ 200 0. out 0 = T 201 1. !t. out (SUC t) = (if inp (SUC t) then ~out t else out t) 202\end{verbatim} 203\end{session} 204 205\noindent Le assunzioni dei due subgoal 206sono riportate numerate sotto le linee di trattini orizzontali. 207L'ultimo goal stampato � quello in cima allo stack, che � il 208caso base. Questo � risolto riscrivendolo con le sue assunzioni e la 209definizione di {\small\verb|PARITY|}. 210 211 212\begin{session} 213\begin{verbatim} 214- expand(ASM_REWRITE_TAC[PARITY_def]); 215OK.. 216 217Goal proved. 218 [.] |- out 0 = PARITY 0 inp 219 220Remaining subgoals: 221> val it = 222 out (SUC t) = PARITY (SUC t) inp 223 ------------------------------------ 224 0. out 0 = T 225 1. !t. out (SUC t) = (if inp (SUC t) then ~out t else out t) 226 2. out t = PARITY t inp 227\end{verbatim} 228\end{session} 229 230Il goal principale � dimostrato, cos� il sistema lo estrae dal goal stack (e 231mette il teorema dimostrato in uno stack di teoremi). Il nuovo goal principale � 232il caso di passo dell'induzione. Questo goal � anch'esso risolto per riscrittura. 233 234\begin{session} 235\begin{verbatim} 236- expand(ASM_REWRITE_TAC[PARITY_def]); 237OK.. 238 239Goal proved. 240 [..] |- out (SUC t) = PARITY (SUC t) inp 241 242Goal proved. 243 [..] |- !t. out t = PARITY t inp 244> val it = 245 Initial goal proved. 246 |- !inp out. 247 (out 0 = T) /\ 248 (!t. out (SUC t) = (if inp (SUC t) then ~out t else out t)) ==> 249 !t. out t = PARITY t inp 250\end{verbatim} 251\end{session} 252 253\noindent Il goal � dimostrato, \ie\ � prodotta la lista vuota di subgoal. 254Il sistema ora applica le funzioni di giustificazione prodotte dalle 255tattiche alla lista di teoremi ottenendo i subgoal (iniziando con 256la lista vuota). Questi teoremi sono stampati nell'ordine in cui 257sono generati (si noti che le assunzioni dei teoremi sono stampate come 258punti). 259 260La funzione \ML{} 261\begin{hol} 262\begin{verbatim} 263 top_thm : unit -> thm 264\end{verbatim} 265\end{hol} 266 267\noindent 268restituisce il teorema appena dimostrato (\ie\ quello in cima allo stack dei teoremi) 269nella teoria corrente, e noi lo leghiamo al nome \ML{} 270\ml{UNIQUENESS\_LEMMA}. 271 272 273\begin{session} 274\begin{verbatim} 275- val UNIQUENESS_LEMMA = top_thm(); 276> val UNIQUENESS_LEMMA = 277 |- !inp out. 278 (out 0 = T) /\ 279 (!t. out (SUC t) = (if inp (SUC t) then ~out t else out t)) ==> 280 !t. out t = PARITY t inp 281 : thm 282\end{verbatim} 283\end{session} 284 285\section{Implementazione} 286\label{implementation} 287 288Il lemma appena dimostrato suggerisce che il checker di parit� pu� essere 289implementato mantenendo il valore di parit� in un registro e poi 290integrando il contenuto del registro ogni volta che {\small\verb|T|} 291� inserito. Per rendere l'implementazione pi� interessante, si 292assumer� che i registri `si accendano' archiviando {\small\verb|F|}. Cos� 293l'output al tempo {\small\verb|0|} non pu� essere preso direttamente da un 294registro, perch� l'output del validatore di parit� al tempo 295{\small\verb|0|} � specificato essere {\small\verb|T|}. Un'altra cosa 296complicata da notare � che se {\small\verb|t>0|} allora l'output del 297validatore di parit� al tempo {\small\verb|t|} � una funzione dell'input al 298tempo {\small\verb|t|}. Cos� ci deve essere un percorso combinatorio 299dall'input all'output. 300 301Il diagramma schematico di sotto mostra il disegno di 302un dispositivo che � inteso implementare questa specifica. 303(L'input pi� a sinistra di \ml{MUX} � il selettore.) 304Questo funziona archiviando la parit� della sequenza immessa finora 305nella parte bassa dei due registri. Ogni volta che {\small\verb|T|} � immesso in 306{\small\verb|in|}, questo valore archiviato � integrato. Si assume che i registri 307`si accendano' in uno stato in cui stanno archiviando {\small\verb|F|}. Il secondo 308registro (connesso a {\small\verb|ONE|}) inizialmente restituisce l'output 309 {\small\verb|F|} e 310dopo restituisce sempre {\small\verb|T|}. Il suo ruolo � solo quello di assicurare che il 311dispositivo 312funzioni durante il primo ciclo collegando l'output {\small\verb|out|} al 313dispositivo {\small\verb|ONE|} attraverso il multiplexer pi� basso. Per tutti i cicli successivi 314{\small\verb|out|} � collegato a {\small\verb|l3|} e quindi o porta il 315valore di parit� archiviato (se l'input corrente � {\small\verb|F|}) oppure il 316complemento di questo valore (se l'input corrente � {\small\verb|T|}). 317 318\begin{center} 319%BEGIN IMAGE 320\setlength{\unitlength}{5mm} 321\begin{picture}(14,30)(0,0.5) 322\put(8,20){\framebox(2,2){\small{\tt NOT}}} 323\put(6,16){\framebox(6,2){\small{\tt MUX}}} 324\put(2,16){\framebox(2,2){\small{\tt ONE}}} 325\put(2,12){\framebox(2,2){\small{\tt REG}}} 326\put(6,8){\framebox(6,2){\small{\tt MUX}}} 327\put(8,4){\framebox(2,2){\small{\tt REG}}} 328 329\puthrule(9,24){4} 330\puthrule(3,15){8} 331\puthrule(3,11){4} 332\puthrule(7,7){2} 333\puthrule(9,3){4} 334 335\putvrule(3,11){1} 336\putvrule(3,14){2} 337\putvrule(7,2){5} 338\putvrule(7,10){1} 339\putvrule(7,18){8} 340\putvrule(9,3){1} 341\putvrule(9,6){2} 342\putvrule(9,10){6} 343\putvrule(9,18){2} 344\putvrule(9,22){2} 345\putvrule(11,10){5} 346\putvrule(11,18){6} 347\putvrule(13,3){21} 348 349\put(6,26){\makebox(2,2){\small{\tt in}}} 350\put(6,0){\makebox(2,2){\small{\tt out}}} 351\put(9,18){\makebox(1.8,2){\small{\tt l1}}} 352\put(13,18){\makebox(1.8,2){\small{\tt l2}}} 353\put(9,12){\makebox(1.8,2){\small{\tt l3}}} 354\put(11,12){\makebox(1.8,2){\small{\tt l4}}} 355\put(4,11){\makebox(3,1){\small{\tt l5}}} 356 357\put(10,23){\makebox(2,2){$\bullet$}} 358\put(8,6){\makebox(2,2){$\bullet$}} 359\put(2,14){\makebox(2,2){$\bullet$}} 360 361\end{picture} 362\setlength{\unitlength}{1mm} 363%END IMAGE 364%HEVEA \imageflush 365\end{center} 366 367I dispositivi che compongono questo schema saranno modellati con predicati 368\cite{Why-HOL-paper}. Per esempio, il predicato {\small\verb|ONE|} � vero 369di un segnale {\small\verb|out|} se per tutti gli istanti {\small\verb|t|} il valore di 370{\small\verb|out|} � {\small\verb|T|}. 371 372\begin{session} 373\begin{verbatim} 374- val ONE_def = Define `ONE(out:num->bool) = !t. out t = T`; 375Definition stored under "ONE_def". 376> val ONE_def = |- !out. ONE out = !t. out t = T : thm 377\end{verbatim} 378\end{session} 379 380\noindent Si noti che, come discusso di sopra, `{\small\verb|ONE_def|}' � usato sia 381come una variabile \ML{} e come il nome della definizione nella teoria. 382Si noti anche come `{\small\verb|:num->bool|}' � stato aggiunto per risolvere 383le ambiguit� di tipo; senza questa (o qualche altra informazione) il 384controllore di tipo non sarebbe in grado di dedurre che {\small\tt t} deve avere 385il tipo {\small\tt num}. 386 387Il predicato binario {\small\verb|NOT|} � vero di una coppia di segnali 388{\small\verb|(inp,out)|} se il valore di {\small\verb|out|} � sempre 389la negazione del valore di {\small\verb|inp|}. Gli invertitori sono cos� 390modellati come non aventi alcun ritardo. Questo � appropriato per un 391modello di livello registro-trasferimento, ma non per un livello inferiore. 392 393\begin{session} 394\begin{verbatim} 395- val NOT_def = Define`NOT(inp, out:num->bool) = !t. out t = ~(inp t)`; 396Definition stored under "NOT_def". 397> val NOT_def = |- !inp out. NOT (inp,out) = !t. out t = ~inp t : Thm.thm 398\end{verbatim} 399\end{session} 400 401\noindent Il dispositivo combinatorio finale necessario � un multiplexer. 402Questo � un `hardware condizionale'; l'input 403{\small\verb|sw|} seleziona quale degli altri 404due input devono essere collegati all'output {\small\verb|out|}. 405 406\begin{session} 407\begin{verbatim} 408- val MUX_def = Define` 409 MUX(sw,in1,in2,out:num->bool) = 410 !t. out t = if sw t then in1 t else in2 t`; 411Definition stored under "MUX_def". 412> val MUX_def = 413 |- !sw in1 in2 out. 414 MUX (sw,in1,in2,out) = !t. out t = (if sw t then in1 t else in2 t) 415 : thm 416\end{verbatim} 417\end{session} 418 419I dispositivi rimanenti nello schema sono i registri. Questi sono 420elementi unit� di ritardo; i valori restituiti come output al tempo {\small\verb|t+1|} sono 421i valori immessi come input al tempo precedente {\small\verb|t|}, escluso il 422tempo {\small\verb|0|} in cui il registro restituisce l'output 423{\small\verb|F|}\footnote{Il tempo {\tt {\small 0}} rappresenta quando il 424 dispositivo � acceso.}. 425 426\begin{session} 427\begin{verbatim} 428- val REG_def = 429 Define `REG(inp,out:num->bool) = 430 !t. out t = if (t=0) then F else inp(t-1)`; 431Definition stored under "REG_def". 432> val REG_def = 433 |- !inp out. REG (inp,out) = !t. out t = 434 (if t = 0 then F else inp (t - 1)) 435 : thm 436\end{verbatim} 437\end{session} 438 439Il diagramma schematico di sopra pu� essere rappresentato come un predicato 440congiungendo le relazioni che valgono tra i vari 441segnali e quindi quantificando esistenzialmente le linee interne. 442Questa tecnica � spiegata altrove 443(\eg\ si veda \cite{Camilleri-et-al,Why-HOL-paper}). 444 445\begin{session} 446\begin{verbatim} 447- val PARITY_IMP_def = Define 448 `PARITY_IMP(inp,out) = 449 ?l1 l2 l3 l4 l5. 450 NOT(l2,l1) /\ MUX(inp,l1,l2,l3) /\ REG(out,l2) /\ 451 ONE l4 /\ REG(l4,l5) /\ MUX(l5,l3,l4,out)`; 452Definition stored under "PARITY_IMP_def". 453> val PARITY_IMP_def = 454 |- !inp out. 455 PARITY_IMP (inp,out) = 456 ?l1 l2 l3 l4 l5. 457 NOT (l2,l1) /\ MUX (inp,l1,l2,l3) /\ REG (out,l2) /\ ONE l4 /\ 458 REG (l4,l5) /\ MUX (l5,l3,l4,out) 459 : thm 460\end{verbatim} 461\end{session}\label{parity-imp} 462 463\section{Verification} 464 465Alla fine sar� dimostrato il seguente teorema: 466\begin{hol} 467\begin{verbatim} 468 |- !inp out. PARITY_IMP(inp,out) ==> (!t. out t = PARITY t inp) 469\end{verbatim} 470\end{hol} 471Questo afferma che {\it se\/} {\small\verb|inp|} e {\small\verb|out|} 472sono correlati come nel diagramma 473schematico (\ie\ come nella definizione di {\small\verb|PARITY_IMP|}), 474{\it allora\/} la 475coppia di segnali {\small\verb|(inp,out)|} soddisfa la specifica. 476 477Per prima cosa, � dimostrato il seguente lemma; la correttezza del validatore 478di parit� segue da questo e da {\small\verb|UNIQUENESS_LEMMA|} per la 479transitivit� di {\small{\tt\verb+==>+}}. 480 481\begin{session} 482\begin{verbatim} 483- g `!inp out. 484 PARITY_IMP(inp,out) ==> 485 (out 0 = T) /\ 486 !t. out(SUC t) = if inp(SUC t) then ~(out t) else out t`; 487> val it = 488 Proof manager status: 2 proofs. 489 2. Completed: ... 490 1. Incomplete: 491 Initial goal: 492 !inp out. 493 PARITY_IMP (inp,out) ==> 494 (out 0 = T) /\ 495 !t. out (SUC t) = (if inp (SUC t) then ~out t else out t) 496\end{verbatim} 497\end{session} 498 499Il primo passo, per dimostrare questo goal � la riscrittura con le definizioni 500seguita da una decomposizione del goal risultante per mezzo di 501{\small\verb|STRIP_TAC|}. E' usata la tattica di riscrittura 502{\small\verb|PURE_REWRITE_TAC|}; questa non fa alcuna semplificazione 503incorporata, ma solo quelle date esplicitamente nella lista di 504teoremi fornita come argomento. Una delle semplificazioni incorporate 505usate da {\small\verb|REWRITE_TAC|} � {\small\tt |-~(x~=~T)~=~x}. 506{\small\verb|PURE_REWRITE_TAC|} � usata per evitare che venga effettuata una riscrittura 507con questa semplificazione. 508\begin{session} 509\begin{verbatim} 510- expand(PURE_REWRITE_TAC 511 [PARITY_IMP_def, ONE_def, NOT_def, MUX_def, REG_def] THEN 512 REPEAT STRIP_TAC); 513OK.. 5142 subgoals: 515> val it = 516 out (SUC t) = (if inp (SUC t) then ~out t else out t) 517 ------------------------------------ 518 0. !t. l1 t = ~l2 t 519 1. !t. l3 t = (if inp t then l1 t else l2 t) 520 2. !t. l2 t = (if t = 0 then F else out (t - 1)) 521 3. !t. l4 t = T 522 4. !t. l5 t = (if t = 0 then F else l4 (t - 1)) 523 5. !t. out t = (if l5 t then l3 t else l4 t) 524 525 out 0 = T 526 ------------------------------------ 527 0. !t. l1 t = ~l2 t 528 1. !t. l3 t = (if inp t then l1 t else l2 t) 529 2. !t. l2 t = (if t = 0 then F else out (t - 1)) 530 3. !t. l4 t = T 531 4. !t. l5 t = (if t = 0 then F else l4 (t - 1)) 532 5. !t. out t = (if l5 t then l3 t else l4 t) 533\end{verbatim} 534\end{session} 535 536Il goal principale � quello stampato per ultimo; la sua conclusione � 537{\small\verb|out 0 = T|} e le sue assunzioni sono equazioni che collegano 538i valori sulle linee nel circuito. Il prossimo passo naturale 539sarebbe espandere il goal principale per mezzo della riscrittura con le assunzioni. Tuttavia, 540se si facesse questo il sistema entrerebbe in un loop infinito perch� 541le equazioni per {\small\verb|out|}, {\small\verb|l2|} e 542{\small\verb|l3|} sono mutuamente ricorsive. Al suo posto usiamo il 543ragionatore al primo ordine {\small\verb|PROVE_TAC|} per fare il lavoro: 544 545\begin{session} 546\begin{verbatim} 547- expand(PROVE_TAC []); 548OK.. 549Meson search level: ..... 550 551Goal proved. 552 [......] |- out 0 = T 553 554Remaining subgoals: 555> val it = 556 out (SUC t) = (if inp (SUC t) then ~out t else out t) 557 ------------------------------------ 558 0. !t. l1 t = ~l2 t 559 1. !t. l3 t = (if inp t then l1 t else l2 t) 560 2. !t. l2 t = (if t = 0 then F else out (t - 1)) 561 3. !t. l4 t = T 562 4. !t. l5 t = (if t = 0 then F else l4 (t - 1)) 563 5. !t. out t = (if l5 t then l3 t else l4 t) 564\end{verbatim} 565\end{session} 566Il primo dei due subgoal � dimostrato. Ispezionando il goal 567rimanente si pu� vedere che sar� risolto se il suo lato sinistro, 568{\small\verb|out(SUC t)|}, � espanso usando l'assunzione: 569 570\begin{hol} 571\begin{verbatim} 572 !t. out t = if l5 t then l3 t else l4 t 573\end{verbatim} 574\end{hol} 575 576 577 Tuttavia, se questa assunzione � usata per riscrivere, allora anche 578 tutti i sottotermini della forma {\small\verb|out t|} saranno espansi. 579 Per evitare questo, in realt� vogliamo riscrivere con una formula che 580 riguarda specificatamente {\small\verb|out (SUC t)|}. Vogliamo estrarre 581 in qualche modo l'assunzione che desideriamo dalla lista e riscrivere con 582 una sua versione specializzata. Possiamo fare questo usando 583 {\small\verb|PAT_ASSUM|}. Questa tattica � di tipo \ml{term -> thm 584 -> tactic}. Essa seleziona un'assunzione che � della forma data 585 dal suo termine argomento, e la passa al secondo argomento, una 586 funzione che si aspetta un teorema e restituisce una tattica. Qui � 587 mostrata in azione: 588 589\begin{session} 590\begin{verbatim} 591- e (PAT_ASSUM ``!t. out t = X t`` 592 (fn th => REWRITE_TAC [SPEC ``SUC t`` th])); 593<<HOL message: inventing new type variable names: 'a, 'b.>> 594OK.. 5951 subgoal: 596> val it = 597 (if l5 (SUC t) then l3 (SUC t) else l4 (SUC t)) = 598 (if inp (SUC t) then ~out t else out t) 599 ------------------------------------ 600 0. !t. l1 t = ~l2 t 601 1. !t. l3 t = (if inp t then l1 t else l2 t) 602 2. !t. l2 t = (if t = 0 then F else out (t - 1)) 603 3. !t. l4 t = T 604 4. !t. l5 t = (if t = 0 then F else l4 (t - 1)) 605\end{verbatim} 606\end{session} 607Il pattern qui usato ha sfruttato qualcosa chiamato \emph{higher order 608 matching}. L'assunzione attuale che � stato tolta dallo stack delle 609assunzioni non ha un lato destro che appare come l'applicazione di una 610funzione (\ml{X} nel pattern) al parametro \ml{t}, ma il lato destro 611potrebbe comunque essere visto uguale all'applicazione di \emph{qualche} 612funzione al parametro \ml{t}. Di fatto, il valore che si accordava con 613\ml{X} era {\small\verb|``\x. if l5 x then l3 x else l4 x``|}. 614 615Ispezionando il goal di sopra si pu� vedere che il prossimo passo � di 616svolgere le equazioni per le linee rimanenti del circuito. Facciamo 617questo usando il simpset \ml{arith\_ss} fornito da \ml{bossLib} che 618aiuta con l'aritmetica incarnata dalle sottrazioni e dai termini 619\ml{SUC}. 620 621 622\begin{session} 623\begin{verbatim} 624- e (RW_TAC arith_ss []); 625OK.. 626 627Goal proved. 628 [.....] 629|- (if l5 (SUC t) then l3 (SUC t) else l4 (SUC t)) = 630 (if inp (SUC t) then ~out t else out t) 631 632Goal proved. 633 [......] |- out (SUC t) = (if inp (SUC t) then ~out t else out t) 634> val it = 635 Initial goal proved. 636 |- !inp out. 637 PARITY_IMP (inp,out) ==> 638 (out 0 = T) /\ 639 !t. out (SUC t) = (if inp (SUC t) then ~out t else out t) 640\end{verbatim} 641\end{session} 642 643\noindent Il teorema appena dimostrato � chiamato 644{\small\verb|PARITY_LEMMA|} e salvato nella teoria corrente. 645 646\begin{session} 647\begin{verbatim} 648- val PARITY_LEMMA = top_thm (); 649> val PARITY_LEMMA = 650 |- !inp out. 651 PARITY_IMP (inp,out) ==> 652 (out 0 = T) /\ 653 !t. out (SUC t) = (if inp (SUC t) then ~out t else out t) 654\end{verbatim} 655\end{session} 656 657{\small\verb|PARITY_LEMMA|} avrebbe potuto essere dimostrato in un unico passo con una 658singola tattica composta. Il nostro goal iniziale poteva essere espanso con una 659singola tattica corrispondente alla sequenza delle tattiche che sono state usate 660interattivamente: 661 662\begin{session} 663\begin{verbatim} 664- restart() 665> ... 666- e (PURE_REWRITE_TAC [PARITY_IMP_def, ONE_def, NOT_def, 667 MUX_def, REG_def] THEN 668 REPEAT STRIP_TAC THENL [ 669 PROVE_TAC [], 670 PAT_ASSUM ``!t. out t = X t`` 671 (fn th => REWRITE_TAC [SPEC ``SUC t`` th]) THEN 672 RW_TAC arith_ss [] 673 ]); 674<<HOL message: inventing new type variable names: 'a, 'b.>> 675OK.. 676Meson search level: ..... 677> val it = 678 Initial goal proved. 679 |- !inp out. 680 PARITY_IMP (inp,out) ==> 681 (out 0 = T) /\ 682 !t. out (SUC t) = (if inp (SUC t) then ~out t else out t) 683\end{verbatim} 684\end{session} 685 686Una volta in possesso di {\small\verb|PARITY_LEMMA|}, il teorema finale � facilmente 687dimostrato. Questo sar� fatto in un unico passo usando la funzione \ML{} 688{\small\verb|prove|}. 689 690\begin{session} 691\begin{verbatim} 692- val PARITY_CORRECT = prove( 693 ``!inp out. PARITY_IMP(inp,out) ==> (!t. out t = PARITY t inp)``, 694 REPEAT STRIP_TAC THEN MATCH_MP_TAC UNIQUENESS_LEMMA THEN 695 MATCH_MP_TAC PARITY_LEMMA THEN ASM_REWRITE_TAC []); 696> val PARITY_CORRECT = 697 |- !inp out. PARITY_IMP (inp,out) ==> !t. out t = PARITY t inp 698\end{verbatim} 699\end{session} 700 701\noindent Questo completa la dimostrazione del 702dispositivo di controllo di parit�. 703 704\section{Esercizi} 705\label{exercises} 706 707In questa sezione sono dati due esercizi: l'Esercizio~1 � 708chiaro, ma l'Esercizio~2 � piuttosto complicato e a un principiante 709potrebbe richiedere molti giorni per risolverlo. 710 711\subsection{Esercizio 1} 712 713Usando {\it solo\/} i dispositivi {\small\verb|ONE|}, {\small\verb|NOT|}, 714{\small\verb|MUX|} e {\small\verb|REG|} definiti nella 715Sezione~\ref{implementation}, progettare e verificare un registro 716{\small\verb|RESET_REG|} con un input {\small\verb|inp|}, linea di ripristino 717{\small\verb|reset|}, output {\small\verb|out|} e comportamento 718specificato come segue. 719\begin{itemize} 720\item Se {\small\verb|reset|} � {\small\verb|T|} al tempo 721 {\small\verb|t|}, allora anche il valore in {\small\verb|out|} al tempo 722 {\small\verb|t|} � {\small\verb|T|}. 723\item Se {\small\verb|reset|} � {\small\verb|T|} al tempo 724 {\small\verb|t|} o {\small\verb|t+1|}, allora il valore di output in 725 {\small\verb|out|} al tempo {\small\verb|t+1|} � {\small\verb|T|}, 726 altrimenti � uguale al valore di input al tempo {\small\verb|t|} su 727 {\small\verb|inp|}. 728\end{itemize} 729Questo � formalizzato in \HOL{} dalla definizione: 730 731 732 733\begin{hol} 734\begin{verbatim} 735 RESET_REG(reset,inp,out) = 736 (!t. reset t ==> (out t = T)) /\ 737 (!t. out(t+1) = if reset t \/ reset(t+1) then T else inp t) 738\end{verbatim} 739\end{hol} 740 741\noindent Si noti che questa specifica � solo parziale; non specifica 742l'output al tempo {\small\verb|0|} nel caso non ci sia alcun azzeramento. 743 744La soluzione all'esercizio dovrebbe essere la definizione di un predicato 745{\small\verb|RESET_REG_IMP|} come una quantificazione esistenziale di una 746congiunzione di applicazioni di {\small\verb|ONE|}, {\small\verb|NOT|}, 747{\small\verb|MUX|} e {\small\verb|REG|} a nomi di linea 748adatti\footnote{Cio� una definizione della stessa forma di 749 {\small\tt PARITY\_IMP} 750%BEGIN LATEX 751a paginae~\pageref{parity-imp}. 752%END LATEX 753%HEVEA in section~\ref{parity-imp} 754}, insieme con una dimostrazione di: 755 756\begin{hol} 757\begin{verbatim} 758 RESET_REG_IMP(reset,inp,out) ==> RESET_REG(reset,inp,out) 759\end{verbatim} 760\end{hol} 761 762 763\subsection{Esercizio 2} 764 765\begin{enumerate} 766\item Specificare formalmente un validatore di parit� azzerabile che ha due input 767 booleani {\small\tt reset} e {\small\tt inp}, e un output booleano 768 {\small\tt out} con il seguente comportamento: 769 \begin{quote} 770 Il valore in {\small\tt out} � {\small\tt T} se e solo se c'� stato 771 un numero pari di input {\small\tt T} in {\small\tt inp} 772 dall'ultima volta che {\small\tt T} � stato immesso in {\small\tt 773 reset}. 774 \end{quote} 775\item Sviluppare un'implementazione di questa specifica costruita usando {\it 776 solo\/} i dispositivi {\small\verb|ONE|}, {\small\verb|NOT|}, 777 {\small\verb|MUX|} e {\small\verb|REG|} definiti nella 778 Sezione~\ref{implementation}. 779 780\item Verificare la correttezza della tua implementazione in \HOL. 781\end{enumerate} 782 783%%% Local Variables: 784%%% mode: latex 785%%% TeX-master: "tutorial" 786%%% End: 787