Loop invariante di selezione Ordina

Question

Loop invariante di selezione Ordina

#1 da (1 voti)
#2 da (0 voti)

1

 Selection Sort(A[1,2..n]:array of integers)
 1.for i=1  to n-1
 2.for j=i+1 to n
 3.if A[j]<A[i]
 4     swap(A[i],A[j])

Sto cercando di dimostrare la correttezza di questo algoritmo, ho letto dal mio libro e qui è ciò che è scritto: dobbiamo avere 2 invarianti per il ciclo interno ed esterno

Gli stati interni: ogni volta che raggiungiamo la linea 2, la corrente A [i] mantiene il valore di un elemento minimo da A [i, ..., j-1]

Gli stati esterni: ogni volta che siamo alla linea 1, il sottoarray attuale A [1, .., i-1] è costituito da i-1 in numero di elementi più piccoli dall'array originale A '[1, ...., n] nell'ordine ordinato

Ora per dimostrare che si tratta veramente di un ordinamento usiamo il ciclo esterno con l'affermazione che la parte da A [1, .., i-1] è ordinata e dal ciclo interno invariante A [i] è il minimo da A [1, ... n] ed è risolto, tuttavia ciò che mi sembra poco chiaro è come progettiamo l'invariante interno, perché diciamo che A [i] è il minimo da A [i, .., j-1 ] Ho provato con alcuni valori e gira sempre solo 1 elemento e credo che nella nostra prova finale diciamo che non è [I] il minimo in A [i, ... j-1] ma A [i, .. n ]. Non dovremmo dire che A [i] è il minimo in A [i, .., j-1] poiché lo abbiamo dimostrato?

algorithms algorithm-analysis

posta Joel Separ 25.04.2017 - 04:06

fonte

2 risposte

Leggi altre domande sui tag algorithms algorithm-analysis

Pattern per sovraccarico di sottoclasse con argomenti diversi Aggiorna una casella combinata da un presentatore (MVP)

score 1 · Answer 1

L'analisi del programma diventerebbe più facile se hai riscritto i loop per come i cicli while equivalenti, perché allora diventa ovvio qual è il valore del "controllato" variabile 'dopo che il ciclo è terminato. In questo stile, il tuo ciclo interno è

j = i+1
(* Inv: i+1 <= j <= n+1 and A[i] = min A[i..j-1] *)
while j <= n:
    if a[j] < a[i]:
        swap(A[i], A[j])
    j = j+1

L'invariante è vero quando j = i +1, ed è gestito dal corpo del ciclo. Quando termina il ciclo, abbiamo j = n +1, e l'invariante ci dice che A [ i ] = min A [ i .. j -1] = min A [ i .. n ]. Questo è ciò che è necessario per giustificare un reclamo che A [1 .. i ] contiene i più piccoli elementi i di A in ordine.

Il ciclo esterno diventa

i = 1
(* Inv: 1 <= i <= n and A[1..i-1] contains the smallest i-1
        elements of A[1..n] in sorted order *)
while i <= n-1:
    [Inner loop]
    i = i+1

Quindi se il ciclo interno termina con A [1 .. i ] come descritto, diventa A [1 .. < em> i -1] dopo aver preso in considerazione l'incremento di i . Il ciclo esterno può terminare con i = n , perché a quel punto abbiamo selezionato e ordinato n -1 elementi di A e l'ultimo elemento rimanente deve essere il più grande.

Non fa male e aiuta la chiarezza a rendere espliciti gli intervalli di variabili come i e j negli invarianti.

In generale: questo tipo di analisi diventa più semplice se si adotta l'indicizzazione basata su 0, perché in tal caso la nebbia di + 1 e -1 diminuisce; ma se il tuo libro utilizza l'indicizzazione basata su 1, credo che tu sia bloccato con esso. Mi piace anche usare la notazione A [ i .. j ) per A [ i .. j -1].

Alcune lingue (che risalgono ad Algol 60) dicono che il valore della variabile controllata non è definito dopo un ciclo per , e altri ci incoraggiano a rendere la variabile locale al ciclo. Ad ogni modo, siamo scoraggiati dal dire che il suo valore dopo il ciclo è n +1, ma tale affermazione è necessaria per dare un senso a ciò che l'invariante ci dice sullo stato dopo che il ciclo è finito. Ecco perché insegno ai miei studenti a riscrivere mentalmente il ciclo come while prima dell'analisi.

score 0 · Answer 2

La dimostrazione riguarda l'ordinamento. Per dimostrare che un array è ordinato, devi solo dimostrare che c'è lo stesso ordine tra tutti i numeri successivi. O altrimenti dichiarato, che ogni numero nell'array è almeno tanto quanto il suo predecessore.

Iniziamo! L'invariante dell'istruzione 3 (insieme alla clausola then in 4) è che:

(I3): whatever the selected i and j, a[i] < a[j]

Da questo, possiamo dedurre l'invariante dell'istruzione 2: il ciclo inizia da i + 1 e continuerà fino a n, quindi assicurerà (I3) per tutti i numeri che seguono i nell'array.

(I2): whatever i, and whatever j between i+1 and n, a[i]< a[j]

Da lì, passiamo all'invariant dell'istruzione 1: il ciclo parte da i = 1 e garantisce che (I2) sia vero, quindi in particolare che 1 induzione matematica:

(I3): every number in the array is smaller than its successor

O al contrario, questo:

every number in the array is greater or equal than the number before.

E questo corrisponde alla definizione di una matrice ordinata.

L'uso dei minimi può certamente essere anche un modo per andare. Ma lo prenderei solo se avessi una definizione di array ordinato che si baserebbe sui minimi.