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