Post on 02-May-2015
transcript
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
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 nullin 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.
istanzacriterio 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
di n elementi di un insieme A linearmente ordinato, trovare una permutazione di ordine n tale che:
Aaa n ,...,1
)()2()1( naaa 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
Le cui istanze sono in
Rrisposta istanza,
R è sempre univoca?
yRyxxRdom qualcheper ,: )(
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:
14,43,22,31 e 24,43,12,31
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:
outputinputF )(
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:
F sceglie una risposta per ogni istanza (ma le risposte possono essere più d’una se R non è univoca).
)( ogniper )(, RdomxRxFx
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à
Posso farlo purché i dati soddisfino
Pre-condizione
Post-condizione
Sig. Utente 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
sodd. sodd. , yxPyx
Una pre-condizione ed una post-condizione definiscono una relazione:
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 < mr n
q 0
while r m do
r r mq q + 1
return q, r
{ n = m q + r, 0 r }
{ n = m (q+1) + r m, 0 r m}
{ n = m q + r, 0 r < m}
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
{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}
invariante
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?
inizializzazione
while condizione do
corpo dell’iterazione
1
2
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
L’ordine giusto è l’opposto!
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
parte ordinata tutti gli el. di questa parte sono maggiori di quelli nella parte ordinata
i
indice del primo elemento della parte da ordinare
Idea
V [1..n]
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
i
Invariante
V [1..n]
• 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
i
Passo
V [1..n] V [k] sia il minimo valore in V [i .. n]
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
i
Passo
V [1..n] V [k] sia il minimo valore in V [i .. n]
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
i+1
Passo
V [1..n]
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
i
Guardia (test di controllo)
V [1..n]
L’iterazione deve proseguire fintanto che i < n.
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Ordinamento per selezione
i = 1
Inizializzazione
V [1..n]
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++)
// 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]);
}
}
C++: dichiarazioni nei blocchi
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++)
if (v[j] < v[indmin]) indmin = j;
return indmin;
}
void Scambia(int& a, int& b)
// post: scambia distruttivamente i valori dei par.
{ int temp = a; a = b; b = temp; }
C++: passaggio parametri per riferimento
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 xn{ int z = 0, y = n;
while (y > 0)
{ z = z + x;
y = y 1; }
return z;
}
2 X 3 =
2 + 2 + 2
A scuola: moltiplicandi e moltiplicatori
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Accumulatori ed invarianti
xxxxx z x y
xxxxx 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 xn{ int z = 0, y = n;
while (y > 0)
{ z = z + x;
y = y 1; }
return z;
}
accumulatorecontatore
{inv. x n = z + x y}
z + x y = (z + x) + x (y – 1)
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Moltiplicazione alla russa
13 56 56
6 112 0
3 224 224
1 448 448
0 - 728
13 56
div 2
raddoppio
+
+
+
=
Risultato = somma val. della seconda colonna quando quelli sulla prima sono dispari
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Moltiplicazione alla russa
dispari se 12
pari se 2
ak
aka
)(22 bbkbkbaka
bbbkbkbaka )()12(12
dispari )()2 div ()(
pari )(2) div (
abbabz
abbazbaz
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;
while (a > 0)
{ if (a % 2 == 1) z = z + b;
a = a / 2;
b = b + b;
}
return z;
}
{inv. n m = z + a b}
contatore
accumulatore
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Dimostrare proprietà di cicli (1)
Divisione (n, m)
Pre. n 0, m > 0
Post. ritorna q, r t.c. n = m q + r, 0 r < mr n
q 0while r m do
r r nq q + 1
return q, r{ n = m q + r, 0 r < m}
{inv. n = m q + r, 0 r }
Come dimostrare che
l’invarinte vale?
Per induzione sul numero
delle iterazioni
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Lo schema dell’induzione
)(.
)]1()(.[ )0(
nPn
nPnPnP
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 nk.P(n))
2. Il passo induttivo: P(n) P(n+1). L’ipotesi P(n) si chiama ipotesi induttiva.
P(m) P(m-1) … P(0)
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Una dimostrazione per induzione
2
)1(
1
nni
n
i
Tesi:
Base: P(0). 2
)10(00
0
1
i
i
Passo: P(n) P(n+1).
Per ipotesi induttiva 2
)1(
1
nni
n
iquindi:
2
)2)(1()1(
2
)1()1(
1
1
1
nnn
nnnii
n
i
n
i
Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1
Dimostrare proprietà di cicli (2)
iterazioni dopo , di valorii siano , irqrq ii
Base: nrq 00 ,0
Tesi:
Passo:
iii rrmqni 0 , , ogniper
nrmqmrmmq iiii
ipotesi induttiva
mrqmrmq iiii )1(11
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