DOMANDA Invariante di ciclo?

FiloRp

Utente Attivo
393
24
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
HDD
SSD 256GB + HDD 2TB
RAM
16GB
GPU
NVidea Geforce GTX 980
Monitor
DELL U2515H
PSU
Corsair CX750M Bronze
Case
Cooler Master N300
OS
Windows 10
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
 

pabloski

Utente Èlite
2,868
916
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
 
  • Mi piace
Reazioni: FiloRp

FiloRp

Utente Attivo
393
24
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
HDD
SSD 256GB + HDD 2TB
RAM
16GB
GPU
NVidea Geforce GTX 980
Monitor
DELL U2515H
PSU
Corsair CX750M Bronze
Case
Cooler Master N300
OS
Windows 10
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
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?
 

pabloski

Utente Èlite
2,868
916
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.
 
  • Mi piace
Reazioni: FiloRp

FiloRp

Utente Attivo
393
24
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
HDD
SSD 256GB + HDD 2TB
RAM
16GB
GPU
NVidea Geforce GTX 980
Monitor
DELL U2515H
PSU
Corsair CX750M Bronze
Case
Cooler Master N300
OS
Windows 10
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.

Chiaro, era una domanda poco pensata.

Potresti fare un altro esempio magari più complesso?
 

pabloski

Utente Èlite
2,868
916
Chiaro, era una domanda poco pensata.

Potresti fare un altro esempio magari più complesso?

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
 
  • Mi piace
Reazioni: FiloRp

FiloRp

Utente Attivo
393
24
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
HDD
SSD 256GB + HDD 2TB
RAM
16GB
GPU
NVidea Geforce GTX 980
Monitor
DELL U2515H
PSU
Corsair CX750M Bronze
Case
Cooler Master N300
OS
Windows 10
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
E l'hai valutato sul ciclo for o sul ciclo while? In base a cosa hai scelto uno e non l'altro?
 

pabloski

Utente Èlite
2,868
916
E l'hai valutato sul ciclo for o sul ciclo while? In base a cosa hai scelto uno e non l'altro?

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.
 
  • Mi piace
Reazioni: Andretti60

FiloRp

Utente Attivo
393
24
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
HDD
SSD 256GB + HDD 2TB
RAM
16GB
GPU
NVidea Geforce GTX 980
Monitor
DELL U2515H
PSU
Corsair CX750M Bronze
Case
Cooler Master N300
OS
Windows 10
Si parte dal più esterno, anche perchè per essere corretto, devono prima esseri corretti i cicli interni.
Controllando il ciclo esterno si valuta la correzione di quelli interni?
 

FiloRp

Utente Attivo
393
24
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
HDD
SSD 256GB + HDD 2TB
RAM
16GB
GPU
NVidea Geforce GTX 980
Monitor
DELL U2515H
PSU
Corsair CX750M Bronze
Case
Cooler Master N300
OS
Windows 10
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.
Guarda sono super intuitivo su moltissime cose ma con quest'ultima spiegazione è sparito il barlume di comprensione che avevo
 

pabloski

Utente Èlite
2,868
916
Guarda sono super intuitivo su moltissime cose ma con quest'ultima spiegazione è sparito il barlume di comprensione che avevo

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.
 
  • Mi piace
Reazioni: FiloRp

FiloRp

Utente Attivo
393
24
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
HDD
SSD 256GB + HDD 2TB
RAM
16GB
GPU
NVidea Geforce GTX 980
Monitor
DELL U2515H
PSU
Corsair CX750M Bronze
Case
Cooler Master N300
OS
Windows 10
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.
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.
 

pabloski

Utente Èlite
2,868
916
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.

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.
 
  • Mi piace
Reazioni: FiloRp

Entra

oppure Accedi utilizzando
Discord Ufficiale Entra ora!

Discussioni Simili