DOMANDA Invariante di ciclo?

Pubblicità
F

FiloRp

Utente Attivo
Messaggi
393
Reazioni
24
Punteggio
39
Ciao a tutti,
da quando ho iniziato a studiare la teoria per il corso di algoritmi non ho mai capito fino in fondo il significato di invariante e la sua utilità nello stabilire la correttezza.

Credo che un esempio molto facile con una breve spiegazione possa essere sufficiente per chiarire definitivamente il concetto.

Grazie in anticipo
 
E' una tecnica induttiva per dimostrare la correttezza dei cicli iterativi. Praticamente si determina una proprietà ( dipende dal ciclo, non c'è una regola fissa per determinarla o una forma di costanza nel tipo di proprietà ) che è valida prima che il ciclo inizi. Si va a verificare che tale proprietà sia valida anche per dopo la prima iterazione. Dopo di che si valuta, per induzione, la sua correttezza per i > 1. Invariante significa appunto che la proprietà mantiene il suo valore di verità pima, durante o dopo il ciclo.

Un esempio http://spazioinwind.libero.it/inginfotv/appunti/dati_algo1/Loop_invariants.pdf
 
pabloski ha detto:
E' una tecnica induttiva per dimostrare la correttezza dei cicli iterativi. Praticamente si determina una proprietà ( dipende dal ciclo, non c'è una regola fissa per determinarla o una forma di costanza nel tipo di proprietà ) che è valida prima che il ciclo inizi. Si va a verificare che tale proprietà sia valida anche per dopo la prima iterazione. Dopo di che si valuta, per induzione, la sua correttezza per i > 1. Invariante significa appunto che la proprietà mantiene il suo valore di verità pima, durante o dopo il ciclo.

Un esempio http://spazioinwind.libero.it/inginfotv/appunti/dati_algo1/Loop_invariants.pdf
Clicca per espandere...
Non so se ho capito: riassumendo brevemente, ipotizzando di avere un ciclo while che si verifica in determinate condizioni, l'invariante consiste nel valutare 3 casi, quello in cui la variabile non è ancora assegnata e quindi il ciclo non è ancora iniziato, quello in cui la variabile viene/non viene trovata nell'array durante uno dei cicli e l'ultimo, dove la variabile non è stata trovata cercando in tutto l'array.

Supponendo di non aver sbagliato/confuso qualcosa, questo caso è abbastanza semplice da definire. Ma quando si tratta di trovare l'invariante per una funzione hash, per degli alberi o per dei grafi?
 
L'invarianza in questo caso è una proprietà dei cicli, non delle stutture dati usati.

Se usi degli hash in un ciclo, probabilmente ad un certo punto saranno confrontati con altri valori ed è questo confronto che potrà fungere da predicato per verificare l'invarianza.
 
pabloski ha detto:
L'invarianza in questo caso è una proprietà dei cicli, non delle stutture dati usati.

Se usi degli hash in un ciclo, probabilmente ad un certo punto saranno confrontati con altri valori ed è questo confronto che potrà fungere da predicato per verificare l'invarianza.
Clicca per espandere...

Chiaro, era una domanda poco pensata.

Potresti fare un altro esempio magari più complesso?
 
FiloRp ha detto:
Chiaro, era una domanda poco pensata.

Potresti fare un altro esempio magari più complesso?
Clicca per espandere...

Questo per esempio

Codice: 
 int i, val, j;
   for (i = 1; i < N; i++)
   {
      val = arr[i];
       j = i-1;

      while (j >= 0 && arr[j] > val)
       {
           arr[j+1] = arr[j];
           j = j-1;
       }
       arr[j+1] = val;
   }

Si tratta dell'insertion sort. Le condizioni sono:

1. iniziale --> il sottoarray contiene il solo elemento iniziale, il che vuol dire che ovviamente è ordinato
2. ciclo --> ogni iterazione ingrossa il sottoarray e un elemento è aggiunto solo se è maggiore dell'elemento alla sua sinistra ( e di tutti quelli a sinistra di quest'ultimo ), cioè il sottoarray è ancora una volta ordinato
3. terminazione --> i raggiunge N e quindi il sottoarray contiene tutti gli elementi dell'array iniziale e sono ordinati per i punti 1 e 2
 
pabloski ha detto:
Questo per esempio

Codice: 
 int i, val, j;
   for (i = 1; i < N; i++)
   {
      val = arr[i];
       j = i-1;

      while (j >= 0 && arr[j] > val)
       {
           arr[j+1] = arr[j];
           j = j-1;
       }
       arr[j+1] = val;
   }

Si tratta dell'insertion sort. Le condizioni sono:

1. iniziale --> il sottoarray contiene il solo elemento iniziale, il che vuol dire che ovviamente è ordinato
2. ciclo --> ogni iterazione ingrossa il sottoarray e un elemento è aggiunto solo se è maggiore dell'elemento alla sua sinistra ( e di tutti quelli a sinistra di quest'ultimo ), cioè il sottoarray è ancora una volta ordinato
3. terminazione --> i raggiunge N e quindi il sottoarray contiene tutti gli elementi dell'array iniziale e sono ordinati per i punti 1 e 2
Clicca per espandere...
E l'hai valutato sul ciclo for o sul ciclo while? In base a cosa hai scelto uno e non l'altro?
 
FiloRp ha detto:
E l'hai valutato sul ciclo for o sul ciclo while? In base a cosa hai scelto uno e non l'altro?
Clicca per espandere...

Si parte dal più esterno, anche perchè per essere corretto, devono prima esseri corretti i cicli interni. Il punto è che la tecnica "loop invariant" è un metodo matematico per verificare la correttezza dei cicli, cioè dimostrare formalmente che fanno quello che devono fare.
 
pabloski ha detto:
Nel senso che per controllare il ciclo esterno devi valutare cosa accade passo dopo passo. E quindi devi per forza valutare per il ciclo interno.
Clicca per espandere...
Guarda sono super intuitivo su moltissime cose ma con quest'ultima spiegazione è sparito il barlume di comprensione che avevo
 
FiloRp ha detto:
Guarda sono super intuitivo su moltissime cose ma con quest'ultima spiegazione è sparito il barlume di comprensione che avevo
Clicca per espandere...

Basta tener presente che il ciclo interno è un pezzo del ciclo esterno, cioè il ciclo esterno non può completare il suo lavoro senza il contributo di quello interno. Mettiti dal punto di vista del processore, cioè mentalmente immagina il ciclo fetch-decode-execute.
 
pabloski ha detto:
Basta tener presente che il ciclo interno è un pezzo del ciclo esterno, cioè il ciclo esterno non può completare il suo lavoro senza il contributo di quello interno. Mettiti dal punto di vista del processore, cioè mentalmente immagina il ciclo fetch-decode-execute.
Clicca per espandere...
Si ok, parlando di pipeline mi è più chiaro il concetto, ma resta il fatto che quando devo valutare l'invariante su un ipotetico ciclo for/while esterno e valuto le sue 3 fasi, il ciclo interno non lo guarderei nemmeno, considererei i cicli interni come conclusi o comunque terminabili.
 
FiloRp ha detto:
Si ok, parlando di pipeline mi è più chiaro il concetto, ma resta il fatto che quando devo valutare l'invariante su un ipotetico ciclo for/while esterno e valuto le sue 3 fasi, il ciclo interno non lo guarderei nemmeno, considererei i cicli interni come conclusi o comunque terminabili.
Clicca per espandere...

Diffcile non guardare il ciclo interno se, per esempio, va a modificare delle variabili che poi userei nel ciclo esterno e proprio nella valutazione dello stato dell'invariante.

L'invariante è tale perchè resta costante prima, durante e dopo l'esecuzione di TUTTE le istruzioni nel ciclo considerato. E il ciclo interno è un pacchetto di istruzioni contenute nel ciclo esterno e che potenzialmente ne può modificare lo stato. Certo non è che vai a guardare se il predicato scelto rimane invariante durante l'esecuzione del ciclo interno, ma comunque devi considerare tutto quello che avviene nel ciclo interno e come eventualmente componenti esterne ad esso ne vengono condizionate.
 
Pubblicità
Pubblicità
Indietro
Top