Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1 Cicli ed asserzioni Corso di Informatica 2 a.a....

Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1

Cicli ed asserzioni

Corso di Informatica 2

a.a. 2003/04

Lezione 1


Il “che cosa” ed il “come”

Problema: 1. dati x, y, z, … così e così

istanza



Problema: 1. dati x, y, z, … così e così2. trovare u, v, w .. tali che …

criterio per riconoscere la risposta



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



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



Quindi un problema è una relazione (binaria) R, ossia una collezione di coppie

Le cui istanze sono in

Rrisposta istanza,

R è sempre univoca?

yRyxxRdom qualcheper ,: )(


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.



• Algoritmo: è un metodo automatico di calcolo, che indica passo passo come ottenere un risultato (output) date certe informazioni di partenza (input).



• 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 )(



• 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


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


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.


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.


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


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


Asserzioni per le iterazioni

while y > 0 do

{ ??????? }

z z + x2

y y 1

Cosa mettere in un punto

attraversato tante volte?



{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!



{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


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?



• Un ciclo ha molti (infiniti) invarianti, per lo più triviali:

{0 = 0} è invariante di ogni ciclo

Qual è allora quello che mi serve?



• 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!


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!


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


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]



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



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:



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



i+1

Passo

V [1..n]

Inoltre la lunghezza della porzione ordinata è aumentata, mentre la lunghezza di quella da ordinare è diminuita



i

Guardia (test di controllo)

V [1..n]

L’iterazione deve proseguire fintanto che i < n.



i = 1

Inizializzazione

V [1..n]

La parte già ordinata è vuota: V[1.. 0]



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



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



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


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



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



xxxxx z x y

xxxxx z + x x (y –

1 )



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)


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



dispari se 12

pari se 2

ak

aka

)(22 bbkbkbaka

bbbkbkbaka )()12(12

dispari )()2 div ()(

pari )(2) div (

abbabz

abbazbaz



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


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


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)


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


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


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 Cicli ed asserzioni Corso di Informatica 2 a.a....

Documents

Transcript of Ugo de'Liguoro - Informatica 2 a.a. 03/04 Lez. 1 Cicli ed asserzioni Corso di Informatica 2 a.a....