Newsgroup: it.scienza.informatica
Titolo: Dimostrazione di finitezza e completezza

Salve a tutti
Per la mia tesi sto implementando un  algoritmo in java. Sono ancora
alla fase teorica e di analisi comunque. Siccome mi sto laureando in
matematica e di informatica teorica nn so poi molto dovrei dimostrare
che questo algoritmo e' finito e corretto nel senso che dato l'input
produce l'output previsto.
Per la finittezza non c'e problema poiche' l'algoritmo ha come
condizione di uscita il fatto che una di due variabili superi un certo
limite n finito.  Ma per per la correttezza come faccio ? Qualcuno
puo' darmi qualche consiglio? l'algoritmo descritto in breve e' il
seguente:
input:
tre array di stringhe A,B,C
scorro entrambi gli A e B array finche' uno dei due indici non ne
supera i limiti
se succede una condizione copio una stringa del primo array su di un
terzo
altrimenti copio una stringa del secondo array su di un terzo
OUTPUT C
Se qualcuno fosse cosi' gentite da darmi qualche suggerimento...
Grazie anticipatamente
Piero


Bhe, non ha detto cosa deve fare l'algoritmo. Converrai che per dimostrare che 
un algoritmo sia corretto bisogna specificare per bene (logica del primo 
ordine per esempio) cosa l'algoritmo faccia. Altrimenti tutti gli algoritmi e 
i programmi sono corretti perche` fanno esattamente quello che fanno. :-)
si procede cosi`
Ti ci vuole una condizione che dica qualcosa sull'input, che deve essere vera 
*prima* dell'algoritmo,
ti ci vuole una condizione che dica qualcosa sull'output, che quindi deve 
essere vera *dopo* l'esecuzione e la terminazione (nota terminazione) 
dell'algoritmo.
poi partendo cosi` si puo` dimostrare (o provare a farlo) che ogni qualvolta 
e` vera la condizione di input, l'algoritmo parte e termina, e` vera la 
condizione di output.
Giorgio

 Se qualcuno fosse cosi' gentite da darmi qualche suggerimento...
Io provo a scrivertelo in linguaggio naturale, vale a dire
dichiaro la mia funzione si chiama finita_e_corretta come un array, che
accetta in ingresso tre array chiamati A, B e C
    memorizzo la lunghezza dell'array A in una variabile come tipo dati long
    memorizzo la lunghezza dell'array B in una variabile  come tipo dati
long
    Se A e' maggiore di B allora e B e' maggiore di zero
        conta da lunghezza dell'array B-1 a lunghezza dell'array A-1
            prendi l'elemento dell'array A il cui indice è uguale al valore
della conta
            aggiungi questo elemento all'array C
        ripeti queste istruzioni fino al termine della conta
    altrimenti se B e' uguale a zero
        copia l'array A dentro C
    fine della condizione
    Se A e' minore di B allora e A maggiore di zero
        conta da lunghezza dell'array A-1 a lunghezza dell'array B-1
            prendi l'elemento dell'array A il cui indice è uguale al valore
della conta
            aggiungi questo elemento all'array C
        ripeti queste istruzioni fino al termine della conta
    altrimenti se A e' uguale a zero
        copia l'array B dentro C
    fine della condizione
    restituisci C
fine della funzione
E così se i due array hanno lo stesso numero di elementi C esce cosi' come
e' entrato.
PERO', ora che mi ci fai pensare potresti fare una cosa un po' più elegante
estendendo la classe Array con un metodo che restituisca gli ultimi n
elementi, allora il numero di righe si ridurrebbe considerevolmente poichè
sparirebbero tutti i cicli.
Ciau
Andrea