Trudny dowód poprawności prostego algorytmu

Mam problem z udowodnieniem poprawności algorytmu do zadania:

Mamy dwie tablice T i S liczb całkowitych nieujemnych. Trzeba zbadać, czy istnieją takie indeksy w T (niech będzie to t) i S (ten indeks to s), żeby suma wszystkich elementów w T od 1 to t była
równa sumie elementów S od 1 do s.

Napisałem program, który wydaje się działać. Teraz jak mam udownodnić jego poprawność, czy poniższe rozumowanie będzie tu wystarczającym dowodem?

W pętli I (oznaczono komentarzem) niezmiennikiem jest to, że w T[lt] (lt- licznik tablicy t) przechowywana jest suma elementów tablicy T od 1 do lt (niezmiennik inicjuje się trywialnie, bo T[1] jest równe sumie wszyskich el. tablicy T od 1 do 1) Analogicznie w S. Drugim niezmiennikiem
jest to, że suma w tablicy T od 1 do k (k nalezy do zbioru{1,2..lt-1} jest różna od analogicznej sumy tablicy S (inicjacja trywialna bo T[0]!=S[0], po prostu nie ma elementów o indeksie 0).

Przy wyjściu z pętli mamy dwie możliwości:

• ls<10 i lt<10, wtedy znaleźliśmy już równe sumy i zadanie jest wykonane.
• ls=10 albo lt=10 wtedy przechodzimy do udowawniania poprawności Pętli II (i analogicznej Pętli III)...

Czy taki "dowód" jest ok? I czy niezmienniki są dobre?

#include <iostream>
#include <ctime>

using namespace std;
#define pauza system("pause");


														/***************************************
														**		      ZADANIE 33	    	                    **
														**								    **
														***************************************/
const int N=4;
int main(){
	srand(time(0));		//losowanie tablic
	int T[13],S[13];
	for (int l=1;l<=N;l++) {T[l]=rand()%10+1;S[l]=rand()%10+1;};
	
	for (int l=1;l<=N;l++) cout<<T[l]<<" ";	//drukowanie tablic
	cout <<endl;
	for (int l=1;l<=N;l++) cout<<S[l]<<" ";
	cout <<endl;
	
	bool rownosc=false;

	int lt=1,ls=1;
	while (lt<N && ls<N){								//---------------PĘTLA I
		if(T[lt]==S[ls]){  //T=S
			printf("Sa rowne sumy dla indeksu tablicy T= %d i S= %d",lt,ls);
			rownosc=true;
			break;
		}
		if(T[lt]>S[ls]){  //T>S
			ls++;
			S[ls]+=S[ls-1];
			continue;
		}
		if(T[lt]<S[ls]){  //T<S
			lt++;
			T[lt]+=T[lt-1];
			continue;
		}
	}

	while (lt<N && !rownosc){	 //Tablica T jest niedokończona			  //---------------PĘTLA II
		lt++;
		T[lt]+=T[lt-1];
		if (T[lt]==S[ls]){
			printf("Sa rowne sumy dla indeksu tablicy T=%d i S=%d",lt,ls);
			rownosc=true;
		}	
	}

	while (ls<N && !rownosc){	 //Tablica S jest niedokończona			//---------------PĘTLA III
		ls++;
		S[ls]+=S[ls-1];
		if (T[lt]==S[ls]) {
			printf("Sa rowne sumy dla indeksu tablicy T=%d i S=%d",lt,ls);
			rownosc=true;
		}	
	}
	
	if (!rownosc) printf("Nie ma rownych sum");
	pauza;
}

Algorytm, jak i dowód, możesz znacznie uprościć używając sum prefiksowych ( http://en.wikipedia.org/wiki/Prefix_sum ) oraz http://pl.wikipedia.org/wiki/Wartownik

Kroki algorytmu:

• przerabiasz obie tablice na sumy prefiksowe (złożoność liniowa, zero dodatkowej pamięci potrzebne),
• do obu tablic dodajesz wartownika, czyli w tym przypadku element większy od wszystkich innych (np max(ostatni element z sum prefiksowych dla S, ostatni element z sum prefiksowych dla T) + 1),
• teraz robisz pętlę bardzo podobną do twojej największej pętli, ale zamiast sprawdzać czy indeks wykracza poza zakres tablicy, sprawdzasz czy masz wartownika pod indeksem,
• dzięki trikowi z wartownikiem nie musisz robić pozostałych dwóch pętli,

Edit:
Nawet nie trzeba wartownika. I tak da się pominąć te dwie mniejsze pętle bez niego:

#include <iostream>

int main() {
    // wczytaj ilość
    uint32_t N;
    std::cin >> N;
    // wczytaj dane
    uint32_t *A = new uint32_t[N];
    for (uint32_t i = 0; i < N; i++) {
        std::cin >> A[i];
    }
    uint32_t *B = new uint32_t[N];
    for (uint32_t i = 0; i < N; i++) {
        std::cin >> B[i];
    }
    // oblicz sumy prefiksowe
    for (uint32_t i = 1; i < N; i++) {
        A[i] += A[i - 1];
    }
    for (uint32_t i = 1; i < N; i++) {
        B[i] += B[i - 1];
    }
    // skan
    uint32_t ia = 0;
    uint32_t ib = 0;
    while (true) {
        if (ia == N || ib == N) {
            std::cout << "Nie znaleziono" << std::endl;
            break;
        }
        if (A[ia] == B[ib]) {
            std::cout << "Znaleziono: " << ia + 1 << ", " << ib + 1 << std::endl;
            break;
        }
        if (A[ia] < B[ib]) {
            ia++;
        } else {
            ib++;
        }
    }

    delete [] A;
    delete [] B;
    return EXIT_SUCCESS;
}

Dzięki.

W ogóle uświadomiłeś mi, że pętle II i III są całkowicie zbędne po prostej przeróbce dozoru pętli I (zamiast lt<N && ls<N) napisałem teraz (lt<=N && ls<=N).

A w poprzedniej wersji, czy te moje niezmienniki udowadniały pętlę I ?

Jeśli zmieniłeś while (lt<N && ls<N){ na while (lt<=N && ls<=N){ to masz błąd bo wychodzisz poza ostatni element tablicy w ostatnich ifach z pętli pierwszej (oznaczonej I).

Spróbuj wstawić niezmienniki bezpośrednio do kodu, we właściwe miejsca. Będzie łatwiej je komentować.

Wibowit napisał(a):

Jeśli zmieniłeś while (lt<N && ls<N){ na while (lt<=N && ls<=N){ to masz błąd bo wychodzisz poza ostatni element tablicy w ostatnich ifach z pętli pierwszej (oznaczonej I).

Masz rację, jednak czy to coś zmienia? Nie będzie Acces Valiation, bo tablice T i S są dłuższe niż N. Czy to w jakiś sposób wpływa na poprawność? Bo w/g jest jedynie trochę "nieeleganckie".

 
while (lt<=N && ls<=N){                                //---------------PĘTLA I
        if(T[lt]==S[ls]){  //T=S
            printf("Sa rowne sumy dla indeksu tablicy T= %d i S= %d",lt,ls);
            rownosc=true;
            break;
        }
        if(T[lt]>S[ls]){  //T>S
            ls++;
            S[ls]+=S[ls-1];
            continue;
        }
        if(T[lt]<S[ls]){  //T<S
            lt++;
            T[lt]+=T[lt-1];
            continue;
        }
    }

Niezmienniki tak czy siak zwykle obowiązują tylko w określonych miejscach w kodzie, więc możesz je wstawić w kod jako np asercje.

Niezmienniki wydają się być ok, ale potrzeba ich więcej MSZ. Np taki że aktualny element z T jest większy niż poprzedni element z S (o ile taki jest, tzn o ile nie jesteśmy na początku tablicy S) i vice versa. Dodając do tego fakt iż zawsze zwiększamy jeden indeks tylko o 1 to wychodzi na to że nie pominiemy żadnej ewentualnej równości sum prefiksowych.