23 wrz 2025·8 min
Tony Hoare’s Correctness Ideas: From Logic to Safe Code
Dowiedz się, jak idee Tony’ego Hoare’a — logika Hoare’a, Quicksort i podejście bezpieczeństwa — wpłynęły na praktyczne techniki pisania i przeglądu poprawnego oprogramowania.
Dowiedz się, jak idee Tony’ego Hoare’a — logika Hoare’a, Quicksort i podejście bezpieczeństwa — wpłynęły na praktyczne techniki pisania i przeglądu poprawnego oprogramowania.
Kiedy ludzie mówią, że program jest „poprawny”, często mają na myśli: „uruchomiłem go kilka razy i wynik wyglądał dobrze.” To użyteczny sygnał — ale to nie jest poprawność. Mówiąc prosto: poprawność oznacza, że program spełnia swoją specyfikację: dla każdego dopuszczalnego wejścia daje wymagany wynik i przestrzega zasad dotyczących zmian stanu, czasu i obsługi błędów.
Problem w tym, że „spełnia specyfikację” jest trudniejsze, niż się wydaje.
Po pierwsze, specyfikacje są często niejednoznaczne. Wymaganie produktu może brzmieć „posortuj listę”, ale czy to ma być sortowanie stabilne? Co z wartościami zduplikowanymi, pustymi listami lub elementami niebędącymi liczbami? Jeśli spec nie precyzuje, różni ludzie przyjmą różne założenia.
Po drugie, przypadki brzegowe nie są rzadkie — po prostu testuje się je rzadziej. Wartości null, przepełnienie, granice off-by-one, nietypowe sekwencje użytkownika i niespodziewane zewnętrzne awarie mogą zmienić „wydaje się działać” w „zepsuło się w produkcji”.
Po trzecie, wymagania się zmieniają. Program może być poprawny względem wczorajszej specyfikacji, a niepoprawny względem dzisiejszej.
Największy wkład Tony’ego Hoare’a nie polegał na twierdzeniu, że powinniśmy wszystko dowodzić cały czas. Chodziło o pomysł, że możemy być bardziej precyzyjni co do tego, co kod ma robić — i rozumować o tym w zdyscyplinowany sposób.
W tym wpisie prześledzimy trzy powiązane wątki:
Większość zespołów nie będzie pisać pełnych formalnych dowodów. Ale nawet częściowe, „w stylu dowodu” podejście może ułatwić wykrywanie błędów, ostrzejsze przeglądy i jaśniejsze zachowanie przed wypuszczeniem kodu.
Tony Hoare to jeden z tych rzadkich informatyków, których praca nie pozostała tylko w artykułach czy salach wykładowych. Poruszał się między akademią a przemysłem i zależało mu na praktycznym pytaniu, z którym każdy zespół się mierzy: jak wiemy, że program robi to, co myślimy — szczególnie gdy stawka jest wysoka?
Ten tekst skupia się na kilku pomysłach Hoare’a, które ciągle pojawiają się w rzeczywistych repozytoriach:
{P} C {Q}.Nie znajdziesz tu głębokiej formalnej matematyki ani pełnego dowodu Quicksort weryfikowanego maszynowo. Celem jest uczynić koncepcje przystępnymi: wystarczająco strukturalnymi, by uporządkować rozumowanie, bez zamieniania przeglądu kodu w seminarium magisterskie.
Pomysły Hoare’a przekładają się na zwykłe decyzje: od jakich założeń zależy funkcja, co gwarantuje wywołującemu, co musi pozostać prawdą w trakcie pętli i jak dostrzec „prawie poprawne” zmiany podczas przeglądu. Nawet jeśli nigdy nie zapiszesz wyraźnie {P} C {Q}, myślenie w tym kształcie poprawia API, testy i jakość dyskusji o trudnym kodzie.
Pogląd Hoare’a jest surowszy niż „przeszło kilka przykładów”: poprawność to dotrzymanie uzgodnionej obietnicy, a nie tylko wyglądanie poprawnie na małej próbce.
Błędy często pojawiają się, gdy zespoły pomijają krok środkowy: skaczą od wymagań prosto do kodu, zostawiając „obietnicę” nieostro sformułowaną.
Dwa różne twierdzenia często są ze sobą mieszane:
W systemach rzeczywistych „niedokończenie” może być tak samo szkodliwe jak „zakończenie z błędnym wynikiem”.
Twierdzenia o poprawności nigdy nie są uniwersalne; opierają się na założeniach dotyczących:
Wyrażenie założeń jawnie zamienia „działa u mnie” w coś, nad czym inni mogą się racjonalnie pochylić.
Rozważ funkcję sortedCopy(xs).
Przydatna specyfikacja może brzmieć: „Zwraca nową listę ys taką, że (1) ys jest posortowana rosnąco, oraz (2) ys zawiera dokładnie te same elementy co xs (te same liczebności), oraz (3) xs nie jest zmienione.”
Teraz „poprawny” oznacza, że kod spełnia te trzy punkty przy zadanych założeniach — nie tylko że wynik wygląda posortowany przy szybkim teście.
Logika Hoare’a to sposób mówienia o kodzie z taką samą jasnością, jak o kontrakcie: jeśli zaczynasz w stanie spełniającym pewne założenia i uruchomisz fragment kodu, skończysz w stanie spełniającym pewne gwarancje.
Główna notacja to potrójka Hoare'a:
{precondition} program {postcondition}
Precondition określa, co musi być prawdziwe przed wykonaniem fragmentu programu. To nie jest to, co miejmy nadzieję jest prawdą; to to, czego kod potrzebuje.
Przykład: załóżmy funkcję obliczającą średnią dwóch liczb bez sprawdzania przepełnienia.
a + b mieści się w typie całkowitymavg = (a + b) / 2avg równa się matematycznej średniej a i bGdy precondition nie jest spełnione (możliwe przepełnienie), obietnica postcondition przestaje obowiązywać. Potrójka zmusza do wyartykułowania tego na głos.
Postcondition mówi, co będzie prawdą po wykonaniu kodu — zakładając, że precondition była spełniona. Dobre postconditions są konkretne i sprawdzalne. Zamiast „wynik jest poprawny”, powiedz, co znaczy „poprawny”: posortowany, nieujemny, w zakresie, niezmieniony poza konkretnymi polami itp.
Logika Hoare’a skaluje się od małych instrukcji do wielostopniowego kodu:
x = x + 1 jakie fakty o x są teraz prawdziwe?Sens nie polega na dosłownym rozrzucaniu nawiasów klamrowych w kodzie. Chodzi o czytelny zamiar: jasne założenia, jasne skutki i mniej „wydaje się działać” w przeglądach.
Inwariant pętli to zdanie prawdziwe przed startem pętli, pozostające prawdziwym po każdej iteracji i nadal prawdziwym, gdy pętla się kończy. To prosta idea o dużym zwrocie: zastępuje „wydaje się działać” twierdzeniem, które można sprawdzić na każdym kroku.
Bez inwariantu przegląd często wygląda tak: „Iterujemy po liście i stopniowo coś naprawiamy.” Inwariant wymusza precyzję: co dokładnie jest już poprawne teraz, chociaż pętla nie jest zakończona? Gdy potrafisz to jasno powiedzieć, błędy off-by-one i brakujące przypadki stają się łatwiejsze do zauważenia, bo pokazują się jako momenty, w których inwariant zostałby złamany.
Większość codziennego kodu może korzystać z kilku niezawodnych szablonów.
Trzymaj indeksy w bezpiecznym zakresie.
0 \u003c= i \u003c= nlow \u003c= left \u003c= right \u003c= highTen typ inwariantu świetnie zapobiega dostępowi poza zakres i czyni rozumowanie o tablicach konkretne.
Podziel dane na region „zrobione” i „jeszcze nie”.
a[0..i) zostały zbadane.”result spełnia predykat filtra.”To zamienia niejasny postęp w jasny kontrakt o tym, co znaczy „przetworzone”.
Częste w sortowaniu, scalaniu i partycjonowaniu.
a[0..i) jest posortowane.”a[0..i) są \u003c= pivot, a wszystkie w a[j..n) są \u003e= pivot.”Nawet jeśli cała tablica nie jest jeszcze uporządkowana, wyznaczasz, co jest.
Poprawność to nie tylko bycie poprawnym; pętla musi też się zakończyć. Prosty sposób, by to uzasadnić, to nazwać miarę (wariant), która zmniejsza się przy każdej iteracji i nie może zmaleć w nieskończoność.
Przykłady:
n - i kurczy się o 1 przy każdej iteracji.”Jeśli nie możesz znaleźć kurczącej się miary, możesz odkryć realne ryzyko: nieskończoną pętlę dla niektórych wejść.
Quicksort ma prostą obietnicę: dla danego fragmentu tablicy przestaw elementy tak, by były w porządku nierosnącym, bez utraty lub wynajdywania wartości. Ogólny kształt algorytmu jest łatwy do podsumowania:
To świetny przykład dla poprawności, ponieważ jest na tyle mały, że mieści się w głowie, ale na tyle bogaty, że pokazuje, gdzie nieformalne rozumowanie zawodzi. Quicksort, który „wydaje się działać” na kilku losowych testach, może być nadal błędny w sytuacjach specyficznych wejść lub warunków brzegowych.
Kilka problemów powoduje większość błędów:
W rozumowaniu w stylu Hoare’a zwykle oddzielasz dowód na dwie części:
To rozdzielenie utrzymuje rozumowanie w ryzach: napraw partycjonowanie, a potem zbuduj poprawność sortowania na jego podstawie.
Szybkość Quicksorta zależy od jednego zwodniczo małego fragmentu: partition. Jeżeli partition jest choć trochę niepoprawne, Quicksort może źle posortować, zapętlić się, albo zawiesić się na przypadkach brzegowych.
Użyjemy klasycznego schematu Hoare partition (dwa wskaźniki poruszające się do środka).
Wejście: fragment tablicy A[lo..hi] i wybrana wartość pivot (często A[lo]).
Wyjście: indeks p taki, że:
A[lo..p] jest \u003c= pivotA[p+1..hi] jest \u003e= pivotZauważ, czego nie obiecujemy: pivot nie musi kończyć na pozycji p, a elementy równe pivot mogą pojawić się po obu stronach. To w porządku — Quicksort potrzebuje jedynie poprawnego podziału.
Gdy algorytm przesuwa dwa indeksy — i od lewej, j od prawej — dobre rozumowanie skupia się na tym, co już „zamknięte”. Praktyczny zestaw inwariantów to:
A[lo..i-1] są \u003c= pivot (lewa strona jest czysta)A[j+1..hi] są \u003e= pivot (prawa strona jest czysta)A[i..j] jest sklasyfikowane (jeszcze do sprawdzenia)Gdy znajdziemy A[i] \u003e= pivot i A[j] \u003c= pivot, zamiana ich zachowuje inwarianty i zmniejsza nieklasyfikowany środek.
i przesunie się w prawo; partycjonowanie nadal powinno się zakończyć i zwrócić sensowny p.j przesunie się w lewo; ta sama troska o zakończenie.\u003c vs \u003c=), wskaźniki mogą zastać się w miejscu. Schemat Hoare’a opiera się na konsekwentnej regule, by postęp trwał.Istnieją różne schematy partycjonowania (Lomuto, Hoare, partycjonowanie trzystronne). Kluczowe jest wybranie jednego, sformułowanie jego kontraktu i konsekwentne przeglądanie kodu względem tego kontraktu.
Rekurencję najłatwiej zaufać, gdy potrafisz jasno odpowiedzieć na dwa pytania: kiedy się zatrzymuje? i dlaczego każdy krok jest poprawny? Myślenie w stylu Hoare’a pomaga, bo zmusza do stwierdzenia, co musi być prawdą przed wywołaniem, i co będzie prawdą po jego powrocie.
Funkcja rekurencyjna potrzebuje przynajmniej jednego przypadku bazowego, w którym nie wykonuje dalszych wywołań rekurencyjnych i nadal spełnia obiecaną specyfikację.
Dla sortowania typowy przypadek bazowy to „tablice długości 0 lub 1 są już posortowane.” Tutaj „posortowane” powinno być jawne: dla relacji ≤ wynik jest posortowany, jeśli dla każdego i \u003c j mamy a[i] ≤ a[j]. (To, czy równe elementy zachowują kolejność, to odrębne własności zwane stabilnością; Quicksort zwykle nie jest stabilny, chyba że tak go skonstruujesz.)
Każdy krok rekurencyjny powinien wywołać się na ściśle mniejszym wejściu. To „kurczenie się” jest argumentem zakończenia: jeśli rozmiar maleje i nie może spaść poniżej zera, nie można rekurencyjnie wywoływać się w nieskończoność.
Kurczenie ma też znaczenie dla bezpieczeństwa stosu. Nawet poprawny kod może się zawiesić, jeśli głębokość rekurencji będzie zbyt duża. W Quicksorcie niezrównoważone partycje mogą dać głęboką rekurencję. To dowód zakończenia i praktyczne przypomnienie, by rozważyć najgorszą głębokość.
Zła złożoność Quicksorta w najgorszym przypadku może spaść do O(n²) przy bardzo niezrównoważonych partycjach, ale to kwestia wydajności — nie poprawności. Cel rozumowania tutaj to: zakładając, że partycjonowanie zachowuje elementy i dzieli je zgodnie z pivotem, rekurencyjne posortowanie podzakresów implikuje, że cała tablica jest posortowana.
Testy i rozumowanie w stylu dowodu dążą do tego samego celu — pewności — ale osiągają to różnymi drogami.
Testy świetnie wykrywają konkretne błędy: off-by-one, brakujący przypadek, regresję. Ale zestaw testów może jedynie próbować przestrzeń wejść. Nawet „100% pokrycia” nie oznacza „wszystkie zachowania sprawdzone”; zazwyczaj znaczy „wszystkie linie uruchomione”.
Rozumowanie w stylu dowodu (szczególnie Hoare’a) zaczyna od specyfikacji i pyta: jeśli te preconditions są spełnione, czy kod zawsze osiągnie postconditions? Gdy robisz to dobrze, nie tylko znajdziesz błąd — często wyeliminujesz całą kategorię błędów (np. „dostęp do tablicy mieści się w zakresie” lub „pętla nie łamie warunku partycjonowania”).
Jasna specyfikacja to generator testów.
Jeśli twoja postcondition mówi „wynik jest posortowany i jest permutacją wejścia”, dostajesz automatycznie pomysły na testy:
Specyfikacja mówi, co znaczy „poprawne”, a testy sprawdzają, czy rzeczywistość z tym się zgadza.
Testy property-based stoją między dowodami a przykładami. Zamiast wybierać ręcznie kilka przypadków, opisujesz własności, a narzędzie generuje wiele wejść.
Dla sortowania dwie proste własności wystarczają daleko:
Te własności to w zasadzie postconditions zapisane jako wykonywalne sprawdzenia.
Lekki rytuał, który skaluje:
Jeśli chcesz to sformalizować, dodaj „spec + notatki o rozumowaniu + testy” do szablonu PR lub checklisty przeglądu kodu (zobacz też /blog/code-review-checklist).
Jeśli używasz workflow generowania kodu z interfejsu konwersacyjnego, ta sama dyscyplina ma jeszcze większe znaczenie. W Koder.ai możesz np. zacząć w Planning Mode, by ustalić preconditions/postconditions zanim wygenerujesz kod, potem iterować ze snapshotami i rollbackem i dodać testy property-based. Narzędzie przyspiesza implementację, ale to spec trzyma „szybko” z dala od „kruchy”.
Poprawność to nie tylko „program zwraca właściwą wartość”. Myślenie o bezpieczeństwie zadaje inne pytanie: które wyniki są nieakceptowalne i jak im zapobiec — nawet gdy kod jest obciążony, źle używany lub częściowo zawodzi? W praktyce bezpieczeństwo to poprawność z priorytetami: niektóre awarie są tylko uciążliwe, inne mogą powodować straty finansowe, naruszenia prywatności lub fizyczną szkodę.
Błąd to wada w kodzie lub projekcie. Zagrożenie to sytuacja mogąca doprowadzić do nieakceptowalnego wyniku. Ten sam błąd może być nieszkodliwy w jednym kontekście i niebezpieczny w innym.
Przykład: off-by-one w galerii zdjęć może źle opisać obraz; ten sam błąd w kalkulatorze dawek leku może zaszkodzić pacjentowi. Myślenie o bezpieczeństwie zmusza do łączenia zachowania kodu z konsekwencjami, a nie tylko z „zgodnością ze specyfikacją”.
Nie potrzebujesz ciężkich formalnych metod, by uzyskać natychmiastowe korzyści bezpieczeństwa. Zespoły mogą przyjąć małe, powtarzalne praktyki:
Te techniki ładnie łączą się z rozumowaniem Hoare’a: jawnie określasz preconditions (jakie wejścia są akceptowalne) i upewniasz się, że postconditions zawierają własności bezpieczeństwa (czego nigdy nie może się zdarzyć).
Kontrole związane z bezpieczeństwem kosztują — czas CPU, złożoność lub okazjonalne odrzucenia.
Myślenie o bezpieczeństwie to mniej próba udowodnienia elegancji, a bardziej zapobieganie trybom awarii, których nie możemy sobie pozwolić.
Przeglądy kodu to miejsce, gdzie myślenie o poprawności daje najszybszy zwrot, bo możesz dostrzec brakujące założenia zanim błędy trafią do produkcji. Główny ruch Hoare’a — stwierdzenie co musi być prawdą przed i co będzie prawdą po — łatwo przekłada się na pytania przeglądowe.
Gdy czytasz zmianę, spróbuj sformułować każdą kluczową funkcję jako małą obietnicę:
Prosty nawyk recenzenta: jeśli nie potrafisz powiedzieć pre/post w jednym zdaniu, kod prawdopodobnie potrzebuje klarowniejszej struktury.
Dla ryzykownych lub centralnych funkcji dodaj krótki komentarz-kontrakt nad sygnaturą. Niech będzie konkretny: wejścia, wyjścia, skutki uboczne i błędy.
def withdraw(account, amount):
"""Contract:
Pre: amount is an integer \u003e 0; account is active.
Post (success): returns new_balance; account.balance decreased by amount.
Post (failure): raises InsufficientFunds; account.balance unchanged.
"""
...
Te komentarze to nie dowody formalne, ale dają recenzentom coś konkretnego do porównania z implementacją.
Bądź szczególnie eksplicytyczny, gdy przeglądasz kod obsługujący:
Jeśli zmiana dotyczy któregokolwiek z tych obszarów, zapytaj: „Jakie są preconditions i gdzie są egzekwowane?” oraz „Jakie gwarancje dajemy nawet, gdy coś zawiedzie?”
Formalne rozumowanie nie musi oznaczać przerobienia całej bazy kodu na pracę naukową. Cel to poświęcić większą pewność tam, gdzie się opłaca: w miejscach, gdzie „wygląda dobrze w testach” to za mało.
Dobrze sprawdzają się, gdy masz mały, krytyczny moduł, od którego zależy reszta (auth, reguły płatności, uprawnienia, blokady bezpieczeństwa), albo trudny algorytm, w którym błędy off-by-one ukrywają się miesiącami (parsery, schedulery, mechanizmy cache/eviction, partycjonowanie, transformacje z wieloma granicami).
Przydatna zasada: jeśli błąd może spowodować realną szkodę, duże straty finansowe lub ciche uszkodzenie danych, potrzebujesz więcej niż zwykły przegląd + testy.
Możesz wybierać od „lekkich” do „ciężkich”, a najlepsze wyniki często wynikają z ich kombinacji:
Zdecyduj zakres formalności, ważąc:
W praktyce „formalność” to coś, co możesz dodawać inkrementalnie: zacznij od jawnych kontraktów i inwariantów, a potem niech automatyzacja pilnuje zgodności.
Dla zespołów rozwijających szybko na Koder.ai — gdzie generacja frontu React, backendu Go i schematu Postgres może być szybka — snapshoty/rollback i eksport źródła ułatwiają iterację, zachowując jednocześnie kontrakty przez testy i analizę statyczną w CI.
Użyj tego jako szybkiego bramki „czy powinniśmy więcej sformalizować?” podczas planowania lub przeglądu:
Dalsze lektury: design-by-contract, property-based testing, model checking dla maszyn stanów, analizatory statyczne dla twojego języka oraz wprowadzenie do asystentów dowodu i specyfikacji formalnej.
Poprawność oznacza, że program spełnia uzgodnioną specyfikację: dla każdego dopuszczalnego wejścia i istotnego stanu systemu zwraca wymagane wyjścia i skutki uboczne (oraz obsługuje błędy zgodnie z obietnicą). „Wygląda, że działa” zwykle oznacza, że sprawdzono tylko kilka przykładów, a nie całą przestrzeń danych ani krytyczne warunki brzegowe.
Wymagania to cel biznesowy wyrażony prostym językiem (np. „posortuj listę do wyświetlenia”). Specyfikacja to precyzyjna, sprawdzalna obietnica (np. „zwraca nową listę posortowaną rosnąco, zawierającą ten sam multizbiór elementów, bez modyfikowania wejścia”). Implementacja to kod. Błędy często pojawiają się, gdy zespół pomija krok pośredni i przechodzi od wymagań prosto do kodu, nie zapisując sprawdzalnej obietnicy.
Częściowa poprawność: jeśli kod zwraca, wynik jest poprawny. Całkowita poprawność: kod zwraca i wynik jest poprawny — więc zakończenie działania jest częścią założenia.
W praktyce całkowita poprawność ma znaczenie, gdy „zawieszenie się” jest widoczne dla użytkownika, prowadzi do wycieku zasobów lub stanowi ryzyko bezpieczeństwa.
Potrójka Hoare’a {P} C {Q} czyta się jak kontrakt:
P (precondition): co musi być prawdą przed uruchomieniem CC: fragment koduPreconditions to to, czego kod potrzebuje (np. „indeksy mieszczą się w zakresie”, „elementy są porównywalne”, „zablokowano zasób”). Jeśli precondition może zostać złamane przez wywołujących, trzeba albo:
W przeciwnym razie twoje postconditions to życzeniowe myślenie.
Inwariant pętli to stwierdzenie prawdziwe przed jej rozpoczęciem, pozostające prawdziwym po każdej iteracji i nadal prawdziwe po zakończeniu pętli. Przydatne szablony:
0 \u003c= i \u003c= n)Jeśli nie potrafisz sformułować inwariantu, to znak, że pętla robi za dużo albo granice są niejasne.
Zwykle nazywasz miarę (wariant), która maleje przy każdej iteracji i nie może maleć w nieskończoność, np.:
n - i zmniejsza się o 1Jeśli nie potrafisz znaleźć malejącej miary, być może odkryłeś realne ryzyko nieskończonej pętli (zwłaszcza przy duplikatach lub zacinających się wskaźnikach).
W Quicksort partycjonowanie to mała funkcja, od której zależy wszystko. Jeśli partycjonowanie jest choć trochę błędne, możesz dostać:
Dlatego warto jasno określić kontrakt partycjonowania: co jest po lewej stronie, co po prawej i że elementy są jedynie przestawiane (permutacja).
Duplikaty i obsługa „równe pivotowi” to częste źródła błędów. Praktyczne zasady:
i/j)Jeśli duplikaty występują często, rozważ partycjonowanie trzystronne, by zmniejszyć zarówno błędy, jak i głębokość rekurencji.
Testy znajdują konkretne błędy; rozumowanie może wykluczyć całe klasy błędów (np. naruszenia zakresów, naruszenie inwariantów, brak zakończenia). Praktyczny hybrydowy workflow:
Dla sortowania dwa wysokowartościowe właściwości to:
Q (postcondition): co będzie prawdą po zakończeniu C, zakładając że P była spełnionaNie musisz pisać tej notacji w kodzie — używanie tej struktury w przeglądach kodu („wejście spełnia założenia, wyjście daje gwarancje”) to praktyczny zysk.