Programma MCD; Flowchart, correttezza e codifica in Pascal

Esercitazione seconda Esercitazione seconda Questa esercitazione è presentata in due parti: Nella prima parte è presentato il flowchart di una funzione che effettui il MCD tra due numeri Nella seconda parte, di tale flowchart è dimostrata la correttezza e ne viene presentata la codifica in Pascal.Flowchart del Programma MCD ?(n,m)?n> 0?m> 0 T P1:MCD(n,m)= =k*MCD(x,y)?(odd(x)?odd(y)) F F T T F F T odd(x)?odd(y)?MCD(n,m)=k*MCD(x,y) T F ?(z,n,m)?Z=MCD(n,m) Dimostrazione della correttezza parziale del flowchart: ?(n,m)?n> 0?m> 0 T P0?MCD(n,m)=k*MCD(x,y) P1:MCD(n,m)=k*MCD(x,y)?(odd(x)?odd(y)) Si può dimostrare che i valori iniziali di ? (n, m ) implicano p0. Tramite la retropropagazione di p0 devo quindi provare che: ? ( n, m ) ? ( p0 ? ( X = n ) ? ( Y = m ) ? ( K = 1 ) ) ( n > 0 ? m > 0 ) ? MCD ( n, m ) =1*MCD ( n, m ) Ovviamente vero; Si dimostra ora che p0 è una invariante del ciclo in figura : si “ porti indietro “ quindi p0 lungo il ciclo e contemporaneamente la si “ faccia scendere “ lungo il ramo che verifica la condizione: ( MCD ( n, m ) = K * MCD ( X, Y )?even ( X )?even ( Y ) ) ? MCD ( n, m ) = 2 * K * MCD ( X div 2, Y div 2 ) L'implicazione risulta verificata perché se X e Y sono entrambi pari certamente 2 è un loro fattore comune e quindi si può portarlo fuori e calcolare il MCD di X div 2 e Ydiv2. F T p2?MCD(n,m)= k*MCD(x,-t)?odd(x) p3? even(t)? ?odd(y)? ?MCD(n,m)= k*MCD(t,y) p4?(MCD(n,m)=k*MCD(x,-t)?odd(x)? (MCD(n,m)=k*MCD(t,y)?odd(y)) Si “ porti giù “ p1 attraverso i due rami della cella condizionale per ricavare p2 e p3 : - per ricavare p2 si sostituisca in p1 Y con -t e si aggiunga la condizione odd ( x ), avendo così : MCD ( n, m ) = K *MCD ( x, -t ) ? ( odd ( X ) ? odd ( -t ) ) ? odd ( x ) che utilizzando la legge della sussunzione si semplifica in: MCD ( n, m ) = K *MCD ( x, -t ) ? odd ( x ) . - per ricavare p3 si sostituisca in p1 X con t e si aggiunga la condizione not odd(X) ovvero even(X) ottenendo: MCD ( n, m ) = K *MCD ( X, Y ) ? ( odd ( X ) ? odd ( Y ) ) ? even ( X ) che diventa: MCD ( n, m ) = K *MCD ( X, Y ) ? odd ( Y ) ? even ( X ) in cui sostituendo x con t si ottiene: MCD ( n, m )= K *MCD ( t, Y ) ? odd ( Y ) ? even ( t ) Unendo logicamente p2 e p3 e tenendo conto che per p3 vale t t div 2 si ottiene p4: p4 non presenta l'even ( t ) della p3 in quanto dividendo t per 2 non si sa più se t è pari o dispari. p3 odd(y)?MCD(n,m)=k*MCD(t,y) T F p3 risulta evidentemente invariante del ciclo in figura. p4 F p5?(MCD(n,m)=k*MCD(x,-t)?odd(x)? odd(t))?(MCD(n,m)=k*MCD(x,y)? F T odd(y)?odd(t)) p6?odd(x)?odd(y)?MCD(n,m)=k*MCD(x,y) Da p4 ci si può ricavare p5 aggiungendo la clausola odd ( t ) : ( ( MCD ( n, m ) = K *MCD ( X, -t ) ? odd ( X )) ? ( MCD ( n, m ) = K *MCD ( t, Y ) ? ? odd ( Y ))) ? odd ( t ) da cui applicando la distributività della congiunzione ricavo p5: ( MCD( n, m )= K *MCD ( x, -t ) ? odd ( X ) ?odd ( t )? ( MCD ( n, m ) = K*MCD ( t, Y)? odd ( Y ) ? odd( t )) Ora, facendo scendere p5 l Continua »