[DOMANDA] Invariante di ciclo?

Discussione in 'Programmazione' iniziata da FiloRp, 13 Gennaio 2018.

  1. FiloRp

    • Utente Binario

    Dal:
    8 Settembre 2015
    Messaggi:
    337
    Mi Piace Ricevuti:
    23
    Specifiche Hardware
    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. pabloski

    • Utente Binario

    Dal:
    30 Marzo 2007
    Messaggi:
    1.427
    Mi Piace Ricevuti:
    184
    Specifiche Hardware
    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
     
    A FiloRp piace questo elemento.
  3. FiloRp

    • Utente Binario

    Dal:
    8 Settembre 2015
    Messaggi:
    337
    Mi Piace Ricevuti:
    23
    Specifiche Hardware
    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. pabloski

    • Utente Binario

    Dal:
    30 Marzo 2007
    Messaggi:
    1.427
    Mi Piace Ricevuti:
    184
    Specifiche Hardware
    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.
     
    A FiloRp piace questo elemento.
  5. FiloRp

    • Utente Binario

    Dal:
    8 Settembre 2015
    Messaggi:
    337
    Mi Piace Ricevuti:
    23
    Specifiche Hardware
    Chiaro, era una domanda poco pensata.

    Potresti fare un altro esempio magari più complesso?
     
  6. pabloski

    • Utente Binario

    Dal:
    30 Marzo 2007
    Messaggi:
    1.427
    Mi Piace Ricevuti:
    184
    Specifiche Hardware
    Questo per esempio

    Codice (Text):
     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
     
    A FiloRp piace questo elemento.
  7. FiloRp

    • Utente Binario

    Dal:
    8 Settembre 2015
    Messaggi:
    337
    Mi Piace Ricevuti:
    23
    Specifiche Hardware
    E l'hai valutato sul ciclo for o sul ciclo while? In base a cosa hai scelto uno e non l'altro?
     
  8. pabloski

    • Utente Binario

    Dal:
    30 Marzo 2007
    Messaggi:
    1.427
    Mi Piace Ricevuti:
    184
    Specifiche Hardware
    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.
     
    A Andretti60 piace questo elemento.
  9. FiloRp

    • Utente Binario

    Dal:
    8 Settembre 2015
    Messaggi:
    337
    Mi Piace Ricevuti:
    23
    Specifiche Hardware
    Controllando il ciclo esterno si valuta la correzione di quelli interni?
     
  10. pabloski

    • Utente Binario

    Dal:
    30 Marzo 2007
    Messaggi:
    1.427
    Mi Piace Ricevuti:
    184
    Specifiche Hardware
    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.
     
    A FiloRp piace questo elemento.
  11. FiloRp

    • Utente Binario

    Dal:
    8 Settembre 2015
    Messaggi:
    337
    Mi Piace Ricevuti:
    23
    Specifiche Hardware
    Guarda sono super intuitivo su moltissime cose ma con quest'ultima spiegazione è sparito il barlume di comprensione che avevo
     
  12. pabloski

    • Utente Binario

    Dal:
    30 Marzo 2007
    Messaggi:
    1.427
    Mi Piace Ricevuti:
    184
    Specifiche Hardware
    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.
     
    A FiloRp piace questo elemento.
  13. FiloRp

    • Utente Binario

    Dal:
    8 Settembre 2015
    Messaggi:
    337
    Mi Piace Ricevuti:
    23
    Specifiche Hardware
    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. pabloski

    • Utente Binario

    Dal:
    30 Marzo 2007
    Messaggi:
    1.427
    Mi Piace Ricevuti:
    184
    Specifiche Hardware
    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.
     
    A FiloRp piace questo elemento.

Condividi questa Pagina