Errori comuni che portano a invarianti corrotti

Question

Errori comuni che portano a invarianti corrotti

#1 da (3 voti)
#2 da (3 voti)
#3 da (1 voti)

2

La mia principale fonte di reddito è lo sviluppo web e attraverso questo sono giunto a godermi le meraviglie della programmazione poiché la mia conoscenza di lingue diverse è aumentata nel corso degli anni attraverso il lavoro e il gioco personale. Ad un certo punto ho raggiunto la decisione che la mia istruzione universitaria non era sufficiente e che volevo tornare a scuola per ottenere una laurea in informatica o ingegneria del software. Ho provato un sacco di cose nella mia vita e mi ci è voluto un po 'prima di trovare qualcosa che sento sia una passione e questo è tutto.

C'è un aspetto di quest'area di studio che trovo mi butta fuori però. Trovo che i metodi formali per dimostrare la correttezza del programma siano una sfida. Non è che ho problemi a scrivere codice in modo corretto, posso guardare un algoritmo e vedere come è corretto o imperfetto, ma a volte faccio fatica a tradurre questo in definizioni formali. Ho ottenuto voti perfetti o quasi perfetti su tutti gli incarichi di programmazione che ho svolto a livello universitario, ma di recente ho ricevuto un elenco di libri di testo di un ragazzo dall'università di Waterloo e ho scoperto che ho avuto problemi quando si tratta di alcuni dei formalismi .

Bene, a questo punto è davvero una sola cosa in particolare, mi sarebbe di grande aiuto se qualcuno di voi potesse fornirmi alcuni buoni esempi di errori comuni che portano ad invarianti corrotti, specialmente nei loop. Ho alcuni manuali di ingegneria del software e di informatica, ma mostrano solo come dovrebbero essere le cose. Mi piacerebbe sapere come vanno le cose, così è più facile riconoscere quando succede. È quasi imbarazzante affrontare questo argomento perché i formalismi sono fondamenta davvero basilari su cui vengono costruite le questioni di sostanza.

Voglio superarlo ora in modo che non mi ostacoli più tardi.

invariants

posta Dave B. 10.01.2011 - 00:59

fonte

3 risposte

Leggi altre domande sui tag invariants

Gestione dei timeout della sessione in relazione all'attività dell'utente nella pagina Chi dovrebbe scrivere la documentazione tecnica?

score 3 · Answer 1

Problemi numerici comuni

Overflow, underflow.

Cosa c'è di sbagliato con

int newArrayLength = arr.length * 2;
T[] newArray = new T[newArrayLength];

Virgola mobile

Mancato account per NaN quando si confronta usando & lt ;, & gt ;, < =, = >.

Cosa c'è di sbagliato con questo

double max(double a, double b) { return a < b ? b : a; }

Filtri

Mancanza di account per i duplicati.

Cosa c'è di sbagliato con

int numberOfInstancesIn(T[] items, T[] set) {
  int count = 0;
  for (int i = 0; i < items.length; ++i) {
    T item = items[i];
    for (int j = 0; j < set.length; ++j) {
      if (item == set[j]) { ++count; }
    }
  }
  return count;
}

Supponendo che due oggetti non siano uguali perché hanno nomi diversi

Cosa c'è di sbagliato con

class Pair {
  T* a;
  T* b;

  ~C() {
    delete a;
    delete b;
  }
}

score 3 · Answer 2

Il mio preferito: errore di inizializzazione corretto

 minIndex = 0
 minValue= someRandomValue # NOT someList[minIndex]
 for i in range( 0, len(someList) ) # NOT range( 1, len(someList) ): 
     assert min(someList) == someList[minIndex] # not true initially
     if someList[i] <= someList[minIndex]:
         minIndex= i
         minValue= someList[minIndex]

L'inizializzazione dovrebbe essere basata su dati reali.

Altro comune - incapacità di mantenere l'invariante in presenza di istruzioni if.

oddSum= 0
evenSum= 0 
for i in range( 0, len(someList) ):
    if i % 2 == 0:
        evenSum += someList[i]
    else:
        # some random statement that doesn't update oddSum
    assert evenSum + oddSum == sum( someList[0:i] )
        # The above may not always be true

Il trucco è questo.

Per ogni "ma mostrano solo come dovrebbero essere le cose" puoi rovinare qualsiasi affermazione e avrai un errore.

Mentre tu - personalmente - puoi vedere l'errore, devi capire che altri programmatori casuali non vedono gli errori e scrivono codice casuale che non soddisfa l'invarianza.

È un esercizio di "Programmazione genetica" - introdurre una mutazione casuale e vedere se l'invariante è vero o no. Mentre leggi il codice di altre persone, vedrai che commettono errori completamente casuali.

score 1 · Answer 3

In generale, lo stato di muting è la causa principale (e potrebbe essere di fatto la causa solo ) degli invarianti corrotti. Non intendo iniziare il vecchio dibattito imperativo vs funzionale, ma c'è un motivo per cui linguaggi come Haskell sono così popolari tra gli accademici: è molto più facile dimostrare la correttezza del codice puramente funzionale. Ovviamente, se il codice funzionale è in generale migliore è una discussione completamente diversa.

Ad esempio, se ho un invariant che la variabile foo deve essere inferiore a 5 dopo ogni iterazione di un ciclo, allora l'unico modo in cui tale invariante fallire è di cambiare il valore di foo. Quindi se foo è inferiore a 5 prima che il codice abbia inizio e tu non modifichi il valore di foo, puoi essere sicuro che foo sarà inferiore a 5 quando il loop termina.