Poprawność programu, specyfikacja

Z Wikipedii: W informatyce teoretycznej poprawność algorytmu jest stwierdzana, gdy mówi się, że algorytm jest poprawny w odniesieniu do specyfikacji.

Problem polega jednak na tym, że uzyskanie „właściwej” specyfikacji nie jest trywialnym zadaniem i nie ma 100% poprawnej metody (o ile wiem), aby uzyskać właściwą, to tylko oszacowanie, więc jeśli mamy zamiar weź predykat jako specyfikację tylko dlatego, że „wygląda” jak „jeden”, dlaczego nie uznać programu za poprawny tylko dlatego, że „wygląda” poprawnie?

Po pierwsze, masz absolutną rację: masz poważny problem. Formalna weryfikacja przenosi problem pewności co do poprawności programu na problem pewności co do poprawności specyfikacji, więc nie jest to srebrna kula.

Istnieje jednak kilka powodów, dla których ten proces może być nadal użyteczny.

1. Specyfikacje są często prostsze niż sam kod. Rozważmy na przykład problem sortowania tablicy liczb całkowitych. Istnieją dość wyrafinowane algorytmy sortowania, które robią sprytne rzeczy w celu poprawy wydajności. Ale specyfikacja jest dość prosta do stwierdzenia: dane wyjściowe muszą być w porządku rosnącym i muszą być permutacją danych wejściowych. Zatem łatwiej jest zdobyć pewność co do poprawności specyfikacji niż poprawności samego kodu.

2. Nie ma jednego punktu awarii. Załóżmy, że jedna osoba zapisuje specyfikację, a inna pisze kod źródłowy, a następnie formalnie sprawdza, czy kod spełnia specyfikację. Wówczas każda niewykryta wada musiałaby być obecna zarówno w specyfikacji, jak i kodzie. W niektórych przypadkach, w przypadku niektórych rodzajów wad, wydaje się to mniej prawdopodobne: mniej prawdopodobne jest, że przeoczysz błąd podczas sprawdzania specyfikacji i przeoczysz błąd podczas sprawdzania kodu źródłowego. Nie wszystkie, ale niektóre.

3. Częściowe specyfikacje mogą być znacznie prostsze niż kod. Rozważmy na przykład wymóg, aby program był wolny od podatności na przepełnienie bufora. Lub wymóg, aby nie występowały błędy poza zakresem indeksu tablicy. Jest to prosta specyfikacja, która jest oczywiście dobrą i przydatną rzeczą, którą można udowodnić. Teraz możesz spróbować użyć metod formalnych, aby udowodnić, że cały program spełnia tę specyfikację. To może być dość zaangażowane zadanie, ale jeśli odniesiesz sukces, zyskasz większe zaufanie do programu.

4. Specyfikacje mogą się zmieniać rzadziej niż kod. Bez formalnych metod za każdym razem, gdy aktualizujemy kod źródłowy, musimy ręcznie sprawdzić, czy aktualizacja nie wprowadzi żadnych błędów ani wad. Metody formalne mogą potencjalnie zmniejszyć to obciążenie: załóżmy, że specyfikacja się nie zmienia, więc aktualizacje oprogramowania obejmują tylko zmiany w kodzie, a nie zmiany w specyfikacji. Następnie, przy każdej aktualizacji, jesteś zwolniony z ciężaru sprawdzania, czy specyfikacja jest nadal poprawna (nie zmieniła się, więc nie ma ryzyka, że ​​nowe specyfikacje zostały wprowadzone w specyfikacji) oraz z ciężaru, aby sprawdzić, czy kod jest nadal poprawne (weryfikator programu sprawdza to dla Ciebie). Nadal musisz sprawdzić, czy oryginalna specyfikacja jest poprawna, ale nie musisz jej sprawdzać za każdym razem, gdy programista wprowadza nową łatkę / aktualizację / zmianę.

Na koniec pamiętaj, że specyfikacje zazwyczaj są deklaratywne i niekoniecznie muszą być wykonywane ani kompilowane bezpośrednio do kodu. Na przykład zastanów się nad sortowaniem ponownie: specyfikacja mówi, że wydajność rośnie i jest permutacją danych wejściowych, ale nie ma oczywistego sposobu na „bezpośrednie wykonanie” tej specyfikacji i nie ma oczywistego sposobu, aby kompilator automatycznie skompilował ją do kodu. Zatem poprawne specyfikowanie i wykonywanie go często nie jest opcją.

Niemniej jednak sedno pozostaje takie samo: metody formalne nie są panaceum. Po prostu przenoszą (bardzo trudny) problem pewności co do poprawności kodu na (tylko trudny) problem pewności co do poprawności specyfikacji. Błędy w specyfikacji stanowią realne ryzyko, są częste i nie można ich przeoczyć. Rzeczywiście społeczność metod formalnych czasami dzieli problem na dwie części: weryfikacja polega na upewnieniu się, że kod spełnia specyfikację; weryfikacja polega na upewnieniu się, że specyfikacja jest poprawna (spełnia nasze potrzeby).

Możesz także cieszyć się formalną weryfikacją programu w praktyce i dlaczego nie badamy więcej w kierunku gwarancji czasu kompilacji? aby uzyskać więcej perspektyw z pewnym wpływem na to.

Odpowiedź DW jest świetna , ale chciałbym rozwinąć w jednym punkcie. Specyfikacja to nie tylko odniesienie, na podstawie którego weryfikowany jest kod. Jednym z powodów posiadania formalnej specyfikacji jest jej weryfikacja poprzez udowodnienie pewnych podstawowych właściwości. Oczywiście specyfikacji nie można całkowicie zweryfikować - walidacja byłaby tak złożona jak sama specyfikacja, więc byłby to niekończący się proces. Ale walidacja pozwala nam uzyskać silniejszą gwarancję niektórych krytycznych właściwości.

Załóżmy na przykład, że projektujesz autopilota samochodowego. Jest to dość złożona sprawa obejmująca wiele parametrów. Właściwości poprawności autopilota obejmują między innymi „samochód nie zderzy się ze ścianą” i „samochód będzie jechał tam, gdzie mu polecono”. Właściwość typu „samochód nie uderzy o ścianę” jest naprawdę bardzo ważna, dlatego chcielibyśmy to udowodnić. Ponieważ system działa w świecie fizycznym, musisz dodać pewne ograniczenia fizyczne; rzeczywista właściwość systemu obliczeniowego będzie przypominała „przy tych założeniach dotyczących materiałoznawstwa i tych założeniach dotyczących postrzegania przeszkód przez czujniki samochodu, samochód nie zderzy się o ścianę”. Ale mimo to wynik jest stosunkowo prostą właściwością, która jest wyraźnie pożądana.

Czy możesz udowodnić tę właściwość na podstawie kodu? Ostatecznie tak się dzieje, jeśli postępujesz zgodnie z całkowicie formalnym podejściem¹. Ale kod składa się z wielu różnych części; hamulce, kamery, silnik itp. są sterowane autonomicznie. Właściwość poprawności hamulców byłaby czymś w rodzaju „jeśli włączony jest sygnał„ włącz hamulce ”, wówczas hamulce zostaną uruchomione”. Właściwością poprawności silnika byłoby „jeśli sygnał sprzęgła jest wyłączony, wówczas silnik nie napędza kół”. Złożenie ich w całość zajmuje widok bardzo wysokiego poziomu. Specyfikacja tworzy warstwy pośrednie, w których różne elementy systemu mogą być połączone przegubowo.

W rzeczywistości tak złożony system, jak autopilot samochodowy, miałby kilka poziomów specyfikacji z różną ilością udoskonaleń. W projekcie często stosuje się podejście wyrafinowane: zacznij od niektórych właściwości wysokiego poziomu, takich jak „samochód nie zderzy się ze ścianą”, a następnie dowiedz się, że wymaga to czujników i hamulców, i opracuj podstawowe wymagania dotyczące czujników, hamulców i oprogramowanie pilotażowe, a następnie ponownie sprecyzuj te podstawowe wymagania w projekcie komponentu (w przypadku czujnika potrzebuję radaru, procesora DSP, biblioteki przetwarzania obrazu itp.) itp. W formalnym procesie opracowywania, udowodniono, że każdy poziom specyfikacji spełnia wymagania określone przez poziom nad nim, od właściwości najwyższego poziomu aż po kod.

Nie można być pewnym, że specyfikacja jest poprawna. Na przykład, jeśli źle zrozumiałeś fizykę, hamulce mogą nie być skuteczne, nawet jeśli matematyka odnosząca kod hamulca do wymagań formalnych jest poprawna. Nie jest dobrym dowodem na to, że przerwy są skuteczne przy 500 kg ładunku, jeśli faktycznie masz 5000 kg. Ale łatwiej jest zauważyć, że 500 kg jest błędne, niż zobaczyć w środku kodu hamulca, że ​​nie będą one wystarczające dla fizycznych parametrów samochodu.

¹ _{Przeciwieństwem w pełni formalnego podejścia jest „Myślę, że to działa, ale nie jestem pewien”. Kiedy stawiasz na to swoje życie, nie wydaje się to takie wspaniałe.}