DIMOSTRAZIONE DI
PROPRIETA’ DEI
PROGRAMMI
INVARIANTI DEI CICLI
O
ASSERZIONE INDUTTIVA
ITERAZIONE
• Una tecnica in cui si esegue la ripetizione
di uno stesso compito.
ORDINAMENTO PER
SELEZIONE
(3,1,4,1,5,9,2,6,5) ---> (1,1,2,3,4,5,5,6,9)
ordinato
non ordinato
i
(a1,a2,....,an) e’ ordinata <---> (b1,b2,....,bn) ordinata ed e’ una
permutazione della lista iniziale
ORDINAMENTO PER SELEZIONE: ALGORITMO
void SelectionSort (float A[ ], const int n);
int i,j, piccolo,temp;
{
for (i= 0; i<n-1; i++)
{
/* piccolo e’ l’indice della prima occorrenza dell’elemento piu’ piccolo */
piccolo=i;
for (j=i+1; j<=n; j++)
if A[j]<A[piccolo]
piccolo:=j;
(* a questo punto piccolo e’ l’indice del primo elemento
piu’ piccolo in A[i.....n] si scambia A[piccolo] con A[i] *)
temp:=A[piccolo];
A[piccolo]:=A[i];
A[i]:=temp;
}
}
void stampa (float [ ], const int );
void SelectionSort (float [ ], const int );
int main ( )
{
float A[8] = {55.5, 22.5, 99.9, 66.6, 44.4, 88.8, 33.3, 77.7};
print (A, 8);
SelectionSort (A, 8);
print (A, 8);
}
void stampa (float [ ], const int );
{
for (i= 0; i<n-1; i++) {
cout << a[i] << “, “;
if ((i+1)%16 ==0) cout << endl;
}
cout << a[n-1] << endl;
}
void SelectionSort (float A[ ], const int n);
…..{
………… // il corpo della funzione
}
• Le prove INDUTTIVE sono di ausilio alla
comprensione del funzionamento dei
programmi
• In particolare, la comprensione del
funzionamento di una struttura ripetitiva o
iterativa risulta fondamentale per la
comprensione del programma stesso
INDUZIONE
• L’idea è quella di provare un asserto per un
caso particolare, e poi mostrare che
allorquando l’asserto è vero per un caso
particolare esso è vero anche per un caso
più grande ( o più piccolo)
INDUZIONE
• In una prova per induzione l’asserto da provare è
detto IPOTESI INDUTTIVA (o ASSERTO
INDUTTIVO)
• Il punto di partenza, cioè un caso particolare
dell’asserto che risulta essere vero, è detto BASE
• Il processo che consente di andare avanti dalla
base verso casi progressivamente maggiori è detto
PASSO INDUTTIVO (o INDUZIONE)
INDUZIONE SEMPLICE
• spesso la base e’ s(0) qualche volta e’ s(k). L’asserto da
dimostrare e’ S(n) con n>=k.
• si assume la verita’ dell’ipotesi induttiva (S(n)) per
mostrare la verita’ di S(n+1) S(n)--> S(n+1)
• “La dimostrazione e’ per induzione su n”
S(n)
.............
S(2)
S(1)
S(0)
INDUZIONE: ESEMPIO
int esponenziale (int x)
{
int SUM =1;
for(int i=1; i <=x; i++)
SUM +=SUM;
/* +++ */
Cout << SUM;
}
La prova di correttezza può essere
effettuata come segue:
• ASSERTO INDUTTIVO: La n-ma volta che si raggiunge +++
, SUM=2n
• BASE Quando n=1, SUM è uguale a 1+1=2 e cioè 21
• PASSO INDUTTIVO: Supponiamo che l’asserto induttivo sia
vero per un particolare valore di n. La n+1-ma volta che +++ è
raggiunto, SUM è posta al valore precedente addizionato a se
stessa. Per l’asserto induttivo, il valore precedente è 2n.
Quindi il nuovo valore è 2n+ 2n= 2n+1. Quindi l’asserto
induttivo è valido anche per n+1. Considerando quindi la
BASE ne segue che l’asserto induttivo vale per n>=1
INDUZIONE: ESEMPIO
• ASSERTO
S(n) 
n i
 2
i0
 2

n 1
S(0) 
 1
BASE
0 i
2
i0
 21  1
INDUZIONE
n 1
S (n  1)   2i 
i 0
n
i
n 1
2

2

i 0
 2n  1  1  2n  1  2 * 2n  1  1  2n  2  1
ASSERZIONI
• Se bisogna verificare la correttezza di un
algoritmo non banale molte volte non è
applicabile il processo di induzione a tutto
l’algoritmo.
• Bisogna, dunque, dividere il programma in
MODULI
ASSERZIONI
• I moduli dovrebbero essere individuati in
modo tale da essere indipendenti.
• La prova di correttezza deve certificare che
il modulo è conforme alle specifiche, che
descrivono gli input forniti al modulo e
l’output che ci si aspetta
ASSERZIONI
• Bisogna, inoltre, provare a realizzare i
moduli in maniera indipendente dai moduli
che esso chiama (moduli di basso livello)
• Si cerca, quindi, di effettuare una prova di
correttezza indipendentemente dai moduli
di basso livello (ci interessa sapere cosa fa
un modulo a basso livello e non come lo fa)
ASSERZIONI
•
Le specifiche dei moduli consistono di due
parti
1. Una specifica sull’intervallo dei valori di
input sui quali ci si aspetta che lavori il
modulo (pre-condizioni)
2. Le specifiche sui comportamenti desiderati
del modulo (post-condizioni)
ASSERZIONI
• Le pre-condizioni descrivono lo stato della
computazione prima che il modulo sia
eseguito
• Le post-condizioni descrivono lo stato dopo
che il modulo è stato eseguito
• Pre e Post condizioni vengono indicate
come ASSERZIONI
ASSERZIONI
• Alcune volte pezzi di un algoritmo sono troppo
correlati per ottenere una buona modularità. In
questi casi, le asserzioni vengono messe nel mezzo
di “pezzi” di algoritmo.
• Un algoritmo dovrebbe contenere le asserzioni nei
punti chiave. Una scelta raccomandata è quella di
metterle una prima ed una dopo una serie di
istruzioni che realizzano un compito ben definito
ASSERZIONI
• Nelle strutture iterative o ripetitive
tipicamente si pone almeno una asserzione
all’interno del ciclo
• Tale asserto viene anche riferito come
INVARIANTE di ciclo, in quanto esso deve
risultare vero durante la permanenza del
programma nel ciclo
(2)
(3)
(4)
(5)
piccolo = i;
for (j=i+1; j<=n; j++)
if A[j] < A[piccolo]
piccolo = j;
piccolo=i
J ha il valore
i+1
j=i+1
S(K)
Asserto induttivo
J>n
(4), (5)
Incremento di j e
controllo alla
guardia del ciclo
j=j+1
/* piccolo è l’indice della prima occorrenza
dell’elemento più piccolo rimasto */
(2) piccolo = i;
(3) for (j=i+1; j<=n; j++)
(4) if A[j] < A[piccolo]
(5)
piccolo = j;
/* piccolo è l’indice del primo
elemento più piccolo in A[i,…,n]
per cui si scambia A[piccolo]
con A[i]
Asserto S(K):
Se raggiungiamo la guardia del ciclo j>n
con k=j allora piccolo è l’indice minimo
in A[i,…., k-1]
Base: k=i+1, j=i+1
Induzione S(k)
S(i+1) vera
S(k+1) per un generico
k >= i+1
DIMOSTRAZIONE
Se k>n
Se k<=n
S(k+1) è vero
S(k+1) piccolo è l’indice del minimo fra
A[i,…,k]
1. Se A[k] NON è più piccolo del
minimo in A[i,…,k-1] allora
S(k+1) è vera
2. Se A[k] E’ più piccolo del minimo
A[i,…,k-1] allora S(k+1) è vera
S(k)
S(k+1)
S(k) è vera per ogni
k:k>=i+1
(1) for (i=0; i<n-1; i++)
{
(2) piccolo = i;
(3) for (j=i+1; j<=n; j++)
(4) if A[j] < A[piccolo]
(5)
piccolo = j;
(6) temp=A[piccolo];
(7) A[piccolo]=A[i];
(8) A[i]=temp
}
i=0
Asserto induttivo
T(m)
i>=n-1
(2), (8)
Incremento di i e
controllo alla
guardia del ciclo
i=i+1
INVARIANTI DELLE STRUTTURE
WHILE E REPEAT
While (espressione)
istruzione
do
istruzione
while (espressione)
(1)
(2)
(3)
(4)
(5)
(6)
(7)
cin >> n;
i=2;
fattoriale = 1;
while (i<=n)
{
fattoriale = fattoriale*i;
i++;
}
cout << fattoriale;
i=2
Fattoriale ha
valore 1
fattoriale=1
S(j)
Asserto induttivo
i<=n
J>n
fattoriale=fattoriale*i
Incremento di i e
controllo alla
guardia del ciclo
i=i+1
Quale e’ l’invariante opportuna
per il seguente frammento
di programma che assegna a somma il
valore della somma degli interi fra 1 ed n ?
cin >> n;
somma=0;
for (i=1; i<=n; i++)
somma=somma+i;
cin >> n;
x=2;
for(i=1; i<=n; i++)
x=x*x;
Una invariante opportuna dice che se
raggiungiamo la guardia del ciclo quando i
ha valore k allora x vale …….
Dimostrare per induzione su k
che questa invariante vale.
Quale è il valore di x al termine del ciclo ?
I numeri del tipo tn=n(n+1)/2 vengono chiamati
numeri triangolari. Poiché il numero di biglie
disposte in un triangolo equilatero, di lato n, è
paria a

n
i 1
i
I birilli del bouling vengono disposti in un triangolo 4 per
lato e ci sono t4=(4*5)/2= 10 birilli.
Dimostrare per induzione su n che:

1
tj

n
(
n

1
)
*
(
n

2
)
/
6
j 1