[DOMANDA] Invariante di ciclo?

  • Nuovo server! Potrebbero esserci ancora piccoli problemi legati alle disponibilità dei servizi del Forum. Scopri di più

FiloRp

Utente Attivo
376
24
Hardware Utente
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
Hard Disk
SSD 256GB + HDD 2TB
RAM
16GB
Scheda Video
NVidea Geforce GTX 980
Monitor
DELL U2515H
Alimentatore
Corsair CX750M Bronze
Case
Cooler Master N300
Sistema Operativo
Windows 10
#1
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
 
#2
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: FiloRp

FiloRp

Utente Attivo
376
24
Hardware Utente
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
Hard Disk
SSD 256GB + HDD 2TB
RAM
16GB
Scheda Video
NVidea Geforce GTX 980
Monitor
DELL U2515H
Alimentatore
Corsair CX750M Bronze
Case
Cooler Master N300
Sistema Operativo
Windows 10
#3
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?
 
#4
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: FiloRp

FiloRp

Utente Attivo
376
24
Hardware Utente
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
Hard Disk
SSD 256GB + HDD 2TB
RAM
16GB
Scheda Video
NVidea Geforce GTX 980
Monitor
DELL U2515H
Alimentatore
Corsair CX750M Bronze
Case
Cooler Master N300
Sistema Operativo
Windows 10
#5
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?
 
#6
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: FiloRp

FiloRp

Utente Attivo
376
24
Hardware Utente
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
Hard Disk
SSD 256GB + HDD 2TB
RAM
16GB
Scheda Video
NVidea Geforce GTX 980
Monitor
DELL U2515H
Alimentatore
Corsair CX750M Bronze
Case
Cooler Master N300
Sistema Operativo
Windows 10
#7
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?
 
#8
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: Andretti60

FiloRp

Utente Attivo
376
24
Hardware Utente
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
Hard Disk
SSD 256GB + HDD 2TB
RAM
16GB
Scheda Video
NVidea Geforce GTX 980
Monitor
DELL U2515H
Alimentatore
Corsair CX750M Bronze
Case
Cooler Master N300
Sistema Operativo
Windows 10
#9
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
376
24
Hardware Utente
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
Hard Disk
SSD 256GB + HDD 2TB
RAM
16GB
Scheda Video
NVidea Geforce GTX 980
Monitor
DELL U2515H
Alimentatore
Corsair CX750M Bronze
Case
Cooler Master N300
Sistema Operativo
Windows 10
#11
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
 
#12
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: FiloRp

FiloRp

Utente Attivo
376
24
Hardware Utente
CPU
Intel Core i5 4690
Scheda Madre
Asus Z97 Deluxe
Hard Disk
SSD 256GB + HDD 2TB
RAM
16GB
Scheda Video
NVidea Geforce GTX 980
Monitor
DELL U2515H
Alimentatore
Corsair CX750M Bronze
Case
Cooler Master N300
Sistema Operativo
Windows 10
#13
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.
 
#14
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: FiloRp

Discussioni Simili