Jak radzić sobie z tablicami podczas sprawdzania poprawności w stylu Hoare'a

11

W dyskusji wokół tego pytania Gilles poprawnie wspomina, że każdy dowód poprawności algorytmu wykorzystującego tablice musi udowodnić, że nie ma dostępu do tablicy poza granicami; w zależności od modelu środowiska wykonawczego spowoduje to błąd środowiska wykonawczego lub dostęp do elementów innych niż macierzowe.

Jedną z powszechnych technik przeprowadzania takich dowodów poprawności (przynajmniej w badaniach licencjackich i prawdopodobnie w automatycznej weryfikacji) jest użycie logiki Hoare'a . Nie wiem, czy standardowy zestaw reguł zawiera wszystko, co dotyczy tablic; wydają się być ograniczone do zmiennych monadycznych.

Mogę sobie wyobrazić dodanie aksjomatów formy

$\qquad \displaystyle \frac{}{\{0 \leq i \lt A.\mathrm{length} \land {P[A[i]/E]} \}\ A[i] := E;\ \{P\}}$

Jednak to nie jest dla mnie jasne, w jaki sposób radzić sobie z dostępem do tablicy po prawej stronie, to znaczy, jeśli jest częścią złożonego ekspresji $E$ w pewnym rachunku $x := E$ .

W jaki sposób można modelować dostęp do macierzy w logice Hoare, aby brak nieprawidłowych dostępów mógł zostać udowodniony pod kątem poprawności programu?

W odpowiedziach można założyć, że nie zezwalamy na stosowanie elementów tablicowych w instrukcjach innych niż $A[i] := E$ lub jako część niektórych $E$ w $x := E$ ponieważ nie ogranicza to ekspresji; zawsze możemy przypisać zmiennej tymczasowej żądaną wartość, tj. zapisać $t := A[i];\ \mathtt{if} ( t > 0 ) \dots$ zamiast $\mathtt{if} ( A[i] > 0 )\dots$ .

— Raphael
źródło

8

Wasz aksjomat nie jest tak naprawdę aksjomatem, brakuje w nim hipotez. Proste prezentacje logiki Hoare manipulować formuły postaci w którym i są wyrażeniami logiczne i jest polecenie. Musisz upewnić się, że jest dobrze uformowany . W prostych językach, takich jak te często używane w pierwszym wprowadzeniu do logiki Hoare'a, dobrze uformowana jest składniowa: zazwyczaj chodzi o sprawdzenie, czy $\{P\} C \{P'\}$ $P$ $P'$ $C$ $C$ $C$ jest zgodny z gramatyką bezkontekstową i możliwe, że wolne zmienne mieszczą się w dozwolonym zestawie. Jeśli język zawiera konstrukty o semantycznej poprawności, takie jak dostęp do elementów tablicy, musisz dodać hipotezy, aby wyrazić tę poprawność semantyczną.

Formalnie możesz dodawać osądy w celu wyrażenia korekty wyrażeń i poleceń. Jeśli wyrażenia nie wywołują skutków ubocznych, nie potrzebują warunków dodatkowych, a jedynie warunki wstępne. Na przykład możesz pisać dobrze sformułowane reguły, takie jak i zezwalaj tylko na poprawnie sformułowane wyrażenia w poleceniach:

\frac{{P} E wf}{{P \land 0 \leq E < l e n g t h (A)} A [E] wf} \frac{{P} E_{1} wf {P} E_{2} wf}{{P} E_{1} + E_{2} wf}

$\dfrac{\{P\} \;\; E \text{ wf}} {\{P \wedge 0 \le E < \mathrm{length}(A)\} \;\; A[E] \text{ wf}} \qquad \dfrac{\{P\} \;\; E_1 \text{ wf} \qquad \{P\} \;\; E_2 \text{ wf}} {\{P\} \;\; E_1 + E_2 \text{ wf}}$

\frac{{P [x \leftarrow E]} E wf}{{P [x \leftarrow E]} x := E {P}}

$\dfrac{\{P[x\leftarrow E]\} \;\; E \text{ wf}} {\{P[x\leftarrow E]\} \;\; x := E \{P\}}$

Inne podejście do leczenia wszystkie wyrażenia także uformowane, ale aby każdy ekspresję obejmujące źle ukształtowany obliczenia mają szczególną wartość . Języków z granice wykonywania kontroli czasu, oznacza „program podniesione” fatalny wyjątek. Będziesz wtedy sprawdzać, czy program pomyłkowo przeszedł przez logiczny predykat ; program jest ważny tylko wtedy, gdy możesz udowodnić, że jego uwarunkowanie implikuje . $\mathbf{error}$ $\mathbf{error}$ $\mathbf{Error}$ $\neg\mathbf{Error}$

\frac{}{{P [x \leftarrow E]} x := E {P \lor E r r o r}} \frac{P [x \leftarrow E] ⟹ E ↛ e r r o r}{{P [x \leftarrow E]} x := E {P}}

$\dfrac{} {\{P[x\leftarrow E]\} \;\; x := E \;\; \{P \vee \mathbf{Error}\}} \qquad \dfrac{P[x\leftarrow E] \implies E \not\rightarrow \mathbf{error}} {\{P[x\leftarrow E]\} \;\; x := E \;\; \{P\}}$

Jeszcze innym podejściem jest rozważenie potrójnego zatrzymania Hoare'a tylko wtedy, gdy program zakończy się poprawnie. Jest to zwykle podejście stosowane w przypadku programów niekończących się: warunek ten obowiązuje po zakończeniu działania polecenia, co nie zawsze może się zdarzyć. Jeśli traktujesz błędy czasu wykonania jako brak zakończenia, omiatasz wszystkie problemy z poprawnością pod maską. Nadal będziesz musiał jakoś udowodnić poprawność programu, ale nie musi to być logika Hoare, jeśli wolisz inny formalizm do tego zadania.

Przy okazji, zauważ, że wyrażanie tego, co dzieje się, gdy zmienna złożona, taka jak tablica, jest modyfikowana, jest bardziej zaangażowane niż to, co napisałeś. Załóżmy, był, na przykład, : substytucja nie zmienia , a przydział może unieważnić . Nawet jeśli ograniczysz składnię predykatów tylko do mówienia o atomach, rozważ przypisanie pod warunkiem : nie można dokonać prostej zamiany w celu uzyskania prawidłowego warunku , należy ocenić $P$ $\mathrm{IsSorted}(A)$ $A[i]\leftarrow E$ $P$ $A[i] \leftarrow P$ $P$ $A[A[0]-1] := A[0]$ $A[0] = 2 \wedge A[1] = 3$ $A[0] = 1 \wedge A[1] = 1$ $A[0]$ (co może być ogólnie trudne, ponieważ warunek wstępny może nie określać pojedynczej możliwej wartości dla ). Musisz wykonać podstawienie na samej tablicy: . Notatki z wykładu Mike'a Gordona mają dobrą prezentację Logika Hoare'a z tablicami (ale bez sprawdzania błędów). $A[0]$ $A \leftarrow A[i\leftarrow E]$

— Gilles „SO- przestań być zły”
źródło

0

Jak wspomniał Gilles, istnieje aksjomat przypisania tablic (patrz uwagi Gordona, pkt 2.1.10 ): słowami, jeśli zadanie tablicy, a następnie zastąpienia oryginalnej tablicy w tablicy , który posiada w pozycji wartość . Pamiętaj, że jeśli masz już post i przypisujesz , powinieneś dostać się jako pre (tak, w tej kolejności - najnowsza aktualizacja jest wykonywana jako pierwsza!).

\frac{}{{Q [A \mapsto A . s t o r e (i, e x p r)]} A [i] = e x p r {Q}}

$\dfrac{} {\{Q[A \mapsto A.store(i,expr) ] \} \;\; A[i] = expr \;\;\{ Q \}}$ A.store(i,expr)iexprA.store(i,vi)A[j]=vjA.store(j,vj).store(i,vi)

Dodatkowo musimy aksjomat dostępu do tablicy: A.store(i,v)[i]może być zastąpione przez v( „jeśli masz dostęp do th element, który po prostu zaktualizowaną, a następnie powrócić przypisaną wartość”). $i$

Myślę, że aby udowodnić, że program z tablicami jest poprawny („brak dostępu poza granicami”), powyższe aksjomaty są wystarczające. Rozważmy program:

...
A[i] = 12
...

Opiszemy ten program:

...
@ {0<i<A_length}
A[i] = 12
...

gdzie A_lengthjest zmienną określającą długość tablicy. Teraz spróbuj udowodnić adnotację - mianowicie przećwicz ją wstecz (od dołu do góry, „jak zwykle” w dowodach Hoare'a). Jeśli na górze dostaniesz {false}, może się zdarzyć, że dostęp poza granicami może się zdarzyć, w przeciwnym razie wyrażenie, które otrzymasz, jest warunkiem wstępnym, pod którym nie ma możliwości uzyskania dostępu poza granicami. (musimy także upewnić się, że gdy tablica jest tworzona tak jak int A=int[10];wtedy, gdy mamy taki stan {A_length==10}).

— Ayrat
źródło

Twoje aksjomaty nie modelują dostępu poza granicami: nawet nie wspominają o długości! W przykładzie programu, w jaki sposób odnoszą się lengthdo A?

— Gilles 'SO - przestań być zły'

Racja, aksjomaty nie modelują poza dostępami dostępowymi. Po pierwsze, aby udowodnić, że program jest poprawny, dodaję adnotacje, które wymagają, aby dostęp był w granicach. ( lengthzostał przemianowany A_length.) Po drugie, potrzebujemy aksjomatów „tworzenia” tablicy, takich jak int[] a = int[length] {a_length==length}. Myślę, że to powinno wystarczyć.

— Ayrat