Cicli ed asserzioni
Corso di Informatica 2
a.a. 2003/04
Lezione 1
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Il “che cosa” ed il “come”
Problema:
1. dati x, y, z, … così e così
istanza
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Il “che cosa” ed il “come”
Problema:
1. dati x, y, z, … così e così
2. trovare u, v, w .. tali che …
criterio per
riconoscere
la risposta
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Il “che cosa” ed il “come”
Esempio (Massimo comun divisore: MCD).
Dati due interi positivi non entrambi nulli
n ed m, determinare un intero positivo k tale
che:
1. k divide sia n che m;
2. per ogni divisore comune h di n ed m, h
divide k.
istanza
criterio per riconoscere
la risposta
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Il “che cosa” ed il “come”
Esempio (Ordinamento: Sorting)
Dato un intero positivo n ed una sequenza
a1 ,..., an  A
di n elementi di un insieme A linearmente
ordinato, trovare una permutazione  di
ordine n tale che:
a (1)  a ( 2)    a ( n )
istanza
criterio per
riconoscere
la risposta
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Il “che cosa” ed il “come”
Quindi un problema è una relazione (binaria) R,
ossia una collezione di coppie
istanza, risposta  R
Le cui istanze sono in
dom( R)   x : x, y  R per qualche y
R è sempre univoca?
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
La relazione R è:
• MCD: univoca, perché se k | h e h | k, allora h = k.
• Sorting: univoca solo se non ci sono ripetizioni. Ci
sono due risposte per l’istanza
7, 5, 22, 5:
1  3,2  1,3  4,4  2e 1  3,2  2,3  4,4  1
anche se producono lo stesso 5, 5, 7, 22.
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Il “che cosa” ed il “come”
• Algoritmo: è un metodo automatico di
calcolo, che indica passo passo come
ottenere un risultato (output) date certe
informazioni di partenza (input).
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Il “che cosa” ed il “come”
• Un algoritmo è deterministico: se eseguito
più volte sullo stesso input, fornisce sempre
lo stesso output.
Dunque ad ogni algoritmo possiamo
associare una funzione input-output:
F (input )  output
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Il “che cosa” ed il “come”
• Un algoritmo risolve un problema R se la su
funzione input-output F associa una
risposta ad ogni istanza di R:
x, F ( x)  R per ogni x  dom( R)
F sceglie una risposta per ogni istanza (ma
le risposte possono essere più d’una se R
non è univoca).
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Che cosa calcola un algoritmo?
Che cosa calcola un algoritmo?
La risposta è una specifica dell’algoritmo.
Vorrei calcolare
valori con la
proprietà 
Post-condizione
Posso farlo
purché i dati
soddisfino 
Sig. Utente
Pre-condizione
Sig. Algoritmo
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Specifica di un algoritmo
• Pre-condizioni: ipotesi sull’ingresso
• Post-condizioni: proprietà dell’uscita
Esempio:
MCD (n, m)
Pre: n, m interi positivi non entrambi nulli
Post: ritorna k che divide sia n che m e t.c. per
ogni divisore comune h di n ed m, h divide k.
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Specifica di un algoritmo
• Pre-condizioni: ipotesi sull’ingresso
• Post-condizioni: proprietà dell’uscita
Una pre-condizione  ed una post-condizione 
definiscono una relazione:
x, y  P  x sodd.   y sodd.
Se R è un problema ed R  P, allora ogni algortimo che
soddisfi la specifica Pre. , Post. , risolve R.
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ragionamenti su di un algoritmo
Ragionare sulla specifica di un algoritmo data
con pre e post-condizioni serve a:
• (a posteriori) verificare la correttezza
dell’algoritmo
• (a priori) (re)-inventare un algoritmo a
partire da un’idea circa la soluzione
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Il metodo delle asserzioni (Floyd)
Divisione (n, m)
Pre. n  0, m > 0
Post. ritorna q, r t.c. n = m q + r, 0  r < m
rn
q0
{ n = m q + r, 0  r }
while r  m do
{ n = m (q+1) + r  m, 0  r  m}
rrm
qq+1
{ n = m q + r, 0  r < m}
return q, r
Asserzioni:
descrivono relazioni
tra i valori delle
variabili, che
devono valere
quando il controllo
raggiunge un certo
punto del codice
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Asserzioni per le iterazioni
while y > 0 do
{ ??????? }
z  z + x2
yy1
Cosa mettere in
un punto
attraversato tante
volte?
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Asserzioni per le iterazioni
{x1  x2 = x2  y + z}
while y > 0 do
{x1  x2 = x2  y + z  y > 0}
z  z + x2
yy1
{x1  x2 = x2  y + z  y = 0}
{z = x1  x2 }
Qualcosa che, pur
cambiando i valori
delle variabili, resti
sempre vero!
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Asserzioni per le iterazioni
invariante
{x1  x2 = x2  y + z}
while y > 0 do
{x1  x2 = x2  y + z  y > 0}
z  z + x2
yy1
{x1  x2 = x2  y + z  y = 0}
{z = x1  x2 }
{}
while B do
{  B}
C
{}
{   B}
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Gli invarianti di ciclo
• invariante: asserzione vera prima di ogni
esecuzione del corpo dell’iterazione
• l’invariante deve essere vero anche prima di
entrare nel ciclo, dopo ogni esecuzione del
corpo, all’uscita dal ciclo
L’ invariante è unico?
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Gli invarianti di ciclo
• Un ciclo ha molti (infiniti) invarianti, per lo
più triviali:
{0 = 0} è invariante di ogni ciclo
Qual è allora quello che mi
serve?
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Gli invarianti di ciclo
• Un invariante è interessante se mi fa capire cosa
avrà fatto il ciclo dopo la terminazione
• Quindi occorre che implichi la post-condizione del
ciclo che desidero dimostrare
• Trovare un invariante senza conoscere l’idea su
cui si basa l’algoritmo è una strada in salita!
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Come si inventa un ciclo?
1
inizializzazione
2
L’ordine giusto
è l’opposto!
while condizione do
corpo dell’iterazione 3
1. Per scrivere l’inizializzazione si deve sapere
cosa deve fare il ciclo
2. Per scrivere la condizione (guardia) si deve
conoscere cosa farà il corpo
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
La generica iterazione
• Per individuare correttamente l’invariante
non ci si deve porre agli estremi (inizio o
fine del ciclo) ma in un ideale punto medio:
la generica iterazione
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
Idea
V [1..n]
parte ordinata
indice del primo
elemento della parte
da ordinare
i
tutti gli el. di questa parte
sono maggiori di quelli
nella parte ordinata
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
Invariante
V [1..n]
i
• V [1 .. i  1] ordinato
• se x in V [i .. n] ed y in V [1 .. i  1] allora x  y
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
Passo
V [k] sia il minimo valore in V [i .. n]
V [1..n]
i
k
Scambiando V[i] con V[k] l’invariante si mantiene con i  i + 1:
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
Passo
V [k] sia il minimo valore in V [i .. n]
V [1..n]
i
k
Scambiando V[i] con V[k] l’invariante si mantiene con i  i + 1:
• V [1 .. i] ordinato
• se x in V [i + 1 .. n] ed y in V [1 .. i ] allora x  y
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
Passo
V [1..n]
i+1
Inoltre la lunghezza della porzione ordinata è
aumentata, mentre la lunghezza di quella da ordinare
è diminuita
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
Guardia (test di controllo)
V [1..n]
i
L’iterazione deve proseguire fintanto che i < n.
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
Inizializzazione
V [1..n]
i=1
La parte già ordinata è vuota: V[1.. 0]
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
Pseudocodifica
SelectSort (V)
Pre. V[1..n] vettore di valori su un insieme linearmente ordinato (es. gli interi)
Post. permuta sul posto gli elementi di V in ordine non decrescente
i1
while i < n do
{inv. V[1..i 1] ordinato, gli el. in V[i..n] maggiorizzano quelli in V[1..i 1]}
k  indice del minimo in V[i..n]
scambia V[i] con V[k]
ii+1
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
Codice C++
void SelectSort (int v[], int n)
// post: ordina distruttivamente ed in
//
senso non decrescente v[0..n-1]
{
for (int i = 0; i < n; i++)
C++:
dichiarazioni
nei blocchi
// inv. v[0..i-1] ordinato, gli el.in v[i..n-1]
// maggiorizzano quelli in v[0..i-1]
{
int k = IndiceDelMin (v, i, n);
Scambia (v[i], v[k]);
}
}
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
Codice C++
int IndiceDelMin (int v[], int i, int n)
// pre: i < n, quindi v[i..n-1] non e' vuoto
// post: ritorna l'indice del minimo in v[i..n-1]
{
int indmin = i;
for(int j = i + 1; j < n; j++)
C++: passaggio
if (v[j] < v[indmin]) indmin = j; parametri per
return indmin;
riferimento
}
void Scambia(int& a, int& b)
// post: scambia distruttivamente i valori dei par.
{
int temp = a; a = b; b = temp; }
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Accumulatori ed invarianti
• Quello iterativo è un metodo di calcolo
incrementale: ci si avvicina al risultato un
passo dopo l’altro
• Un accumulatore è una variabile il cui
valore rappresenta l’approssimazione
corrente
• L’invariante deve allora spiegare in che
senso l’accumulatore approssima il risultato
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Accumulatori ed invarianti
int Molt (int x, int n)
// Pre. n intero positivo
// Post. ritorna xn
{ int z = 0, y = n;
while (y > 0)
{ z = z + x;
y = y  1;
}
return z;
}
A scuola:
moltiplicandi e
moltiplicatori
2X3=
2+2+2
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Accumulatori ed invarianti
x   x  x  x   x
z
x y
x   x  x  x   x
z+x
x (y – 1 )
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Accumulatori ed invarianti
int Molt (int x, int n)
// Pre. n intero positivo
// Post. ritorna xn
{ int z = 0, y = n;
while (y > 0) {inv. x n = z + x y}
{ z = z + x;
z + x y = (z + x) + x  (y – 1)
y = y  1;
}
accumulatore
return z;
contatore
}
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Moltiplicazione alla russa
13  56
13
56
6
112
56 +
0 +
3
224
224 +
1
448
448 =
0
-
728
Risultato =
somma val.
della seconda
colonna quando
quelli sulla
prima sono
dispari
div 2
raddoppio
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Moltiplicazione alla russa
 2k
a
2 k  1
se a pari
se a dispari
a  2k  a  b  2k  b  k  (b  b)
a  2k  1  a  b  (2k  1)  b  k  (b  b)  b
 z  (a div 2)  (b  b)
z  a b  
( z  b)  (a div 2)  (b  b)
a pari
a dispari
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Moltiplicazione alla russa
int MoltRussa (int m, int n)
// Pre. n, m interi positivi
// Post. ritorna n  m
{ int a = n, b = m, z = 0;
{inv. n  m = z + a  b}
while (a > 0)
{
if (a % 2 == 1) z = z + b;
a = a / 2;
accumulatore
b = b + b;
}
contatore
return z;
}
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Dimostrare proprietà di cicli (1)
Divisione (n, m)
Per induzione
Pre. n  0, m > 0
sul numero delle
Post. ritorna q, r t.c. n = m q + r, 0  r < m
iterazioni
rn
Come
q0
dimostrare che
while r  m do
l’invarinte vale?
{inv. n = m q + r, 0  r }
rrn
qq+1
{ n = m q + r, 0  r < m}
return q, r
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Lo schema dell’induzione
Una dimostrazione per induzione si suddivide in due parti:
1. Il caso di base: P(0) (ma potrebbe essere P(k), e allora la
conlcusione sarebbe nk.P(n))
2. Il passo induttivo: P(n)  P(n+1). L’ipotesi P(n) si
chiama ipotesi induttiva.
P(0)
P(m)
n.[ P(n)  P(n  1)]
n.P(n)
 P(m-1)  … 
P(0)
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Una dimostrazione per induzione
n
i 
Tesi:
i 1
n(n  1)
2
0
Base: P(0).
i  0 
i 1
Passo: P(n)  P(n+1).
n
Per ipotesi induttiva
n 1
n
i 1
i 1
 i   i  (n  1) 
i 
i 1
0(0  1)
2
n(n  1)
2
quindi:
n(n  1)
(n  1)( n  2)
 (n  1) 
2
2
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Dimostrare proprietà di cicli (2)
qi , ri siano i valori di q, r dopo i iterazioni
Tesi:
per ogni i, n  mqi  ri , 0  ri
Base:
q0  0, r0  n
Passo:
mqi 1  ri 1  m(qi  1)  ri  m
 mqi  m  ri  m  mqi  ri  n
ipotesi induttiva
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Riassumendo
• La specifica (pre e post condizioni) definisce cosa
fa una procedura (algoritmo)
• Le asserzioni sono un metodo per verificare la
correttezza di un algoritmo
• Per trattare i cicli occorre individuare i loro
invarianti
• Gli invarianti sono fondamentali per progettare o
capire un ciclo
• La prova che un’asserzione è un invariante è per
induzione
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1