Dowód jest znacznie trudniejszy w świecie OOP ze względu na skutki uboczne, nieograniczone dziedziczenie i nullbycie członkiem każdego rodzaju. Większość dowodów opiera się na zasadzie indukcji, aby pokazać, że wykorzystałeś wszystkie możliwości, a wszystkie 3 z tych rzeczy utrudniają udowodnienie.
Powiedzmy, że wdrażamy drzewa binarne, które zawierają wartości całkowite (dla uproszczenia składni nie będę wprowadzał do tego programowania ogólnego, chociaż nic by to nie zmieniło). W Standardowym ML zdefiniowałbym to jako to:
datatype tree = Empty | Node of (tree * int * tree)
Wprowadza to nowy typ o nazwie, treektórego wartości mogą występować w dokładnie dwóch odmianach (lub klasach, których nie należy mylić z koncepcją OOP klasy) - Emptywartość, która nie przenosi żadnych informacji, oraz Nodewartości, które niosą 3-krotkę, której pierwsza i ostatnia elementy to trees, a środkowym elementem jest int. Najbliższe zbliżenie do tej deklaracji w OOP wyglądałoby tak:
public class Tree {
private Tree() {} // Prevent external subclassing
public static final class Empty extends Tree {}
public static final class Node extends Tree {
public final Tree leftChild;
public final int value;
public final Tree rightChild;
public Node(Tree leftChild, int value, Tree rightChild) {
this.leftChild = leftChild;
this.value = value;
this.rightChild = rightChild;
}
}
}
Z zastrzeżeniem, że zmienne typu Drzewo nigdy nie mogą być null.
Napiszmy teraz funkcję do obliczenia wysokości (lub głębokości) drzewa i załóżmy, że mamy dostęp do maxfunkcji, która zwraca większą z dwóch liczb:
fun height(Empty) =
0
| height(Node (leftChild, value, rightChild)) =
1 + max( height(leftChild), height(rightChild) )
Zdefiniowaliśmy heightfunkcję według przypadków - istnieje jedna definicja dla Emptydrzew i jedna definicja dla Nodedrzew. Kompilator wie, ile istnieje klas drzew i wyda ostrzeżenie, jeśli nie zdefiniujesz obu przypadków. Wyrażenie Node (leftChild, value, rightChild)w podpisie funkcji wiąże wartości 3-krotki do zmiennych leftChild, valueoraz rightChildodpowiednio więc możemy odnieść się do nich w definicji funkcji. Jest to podobne do zadeklarowania takich zmiennych lokalnych w języku OOP:
Tree leftChild = tuple.getFirst();
int value = tuple.getSecond();
Tree rightChild = tuple.getThird();
Jak możemy udowodnić, że heightpoprawnie wdrożyliśmy ? Możemy użyć indukcji strukturalnej , która składa się z: 1. Udowodnij, że heightjest poprawna w przypadku (przypadkach) bazowych naszego treetypu ( Empty) 2. Zakładając, że wywołania rekurencyjne heightsą poprawne, udowodnij, że heightjest to poprawne w przypadku przypadku nie będącego podstawą ) (gdy drzewo to tak naprawdę Node).
W kroku 1 widzimy, że funkcja zawsze zwraca 0, gdy argumentem jest Emptydrzewo. Jest to prawidłowe z definicji wysokości drzewa.
W kroku 2 funkcja powraca 1 + max( height(leftChild), height(rightChild) ). Zakładając, że wywołania rekurencyjne naprawdę zwracają wzrost dzieci, możemy zauważyć, że jest to również poprawne.
I to stanowi dowód. Łączne kroki 1 i 2 wyczerpują wszystkie możliwości. Zauważ jednak, że nie mamy mutacji, żadnych zer i istnieją dokładnie dwie odmiany drzew. Po usunięciu tych trzech warunków dowód szybko staje się bardziej skomplikowany, jeśli nie niepraktyczny.
EDYCJA: Ponieważ ta odpowiedź osiągnęła szczyt, chciałbym dodać mniej trywialny przykład dowodu i nieco dokładniej objąć indukcję strukturalną. Powyżej udowodniliśmy, że jeśli heightzwraca , to zwracana wartość jest poprawna. Jednak nie udowodniliśmy, że zawsze zwraca wartość. Możemy również użyć indukcji strukturalnej, aby to udowodnić (lub dowolną inną właściwość). Ponownie, podczas kroku 2, możemy przyjąć, że wstrzymania własności wywołań rekurencyjnych są zachowane, o ile wszystkie wywołania rekurencyjne działają na bezpośrednim potomku drzewo.
Funkcja może nie zwrócić wartości w dwóch sytuacjach: jeśli zgłosi wyjątek i zapętli się na zawsze. Najpierw udowodnijmy, że jeśli nie zostaną zgłoszone żadne wyjątki, funkcja kończy się:
Wykazać, że (jeśli nie zostaną zgłoszone wyjątki) funkcja kończy się dla przypadków bazowych ( Empty). Ponieważ bezwarunkowo zwracamy 0, to kończy się.
Wykazać, że funkcja kończy się w przypadkach innych niż bazowe ( Node). Są trzy wywołania funkcji tutaj: +, max, i height. Wiemy o tym +i maxrozwiązujemy, ponieważ są one częścią standardowej biblioteki języka i są zdefiniowane w ten sposób. Jak wspomniano wcześniej, możemy założyć, że właściwość, którą próbujemy udowodnić, jest prawdziwa w przypadku wywołań rekurencyjnych, o ile działają one w bezpośrednich poddrzewach, więc również wezwania do heightzakończenia.
To kończy dowód. Pamiętaj, że nie można udowodnić zakończenia przy pomocy testu jednostkowego. Teraz pozostaje tylko pokazać, że heightnie rzuca wyjątków.
- Udowodnij, że
heightnie wyrzuca wyjątków na przypadek podstawowy ( Empty). Zwrócenie 0 nie może zgłosić wyjątku, więc skończyliśmy.
- Udowodnij, że
heightnie zgłasza wyjątku w przypadku innym niż bazowy ( Node). Załóżmy jeszcze raz, że wiemy +i maxnie rzucamy wyjątków. A indukcja strukturalna pozwala nam założyć, że wywołania rekurencyjne też nie rzucą (ponieważ działają na bezpośrednie dzieci drzewa). Ale czekaj! Ta funkcja jest rekurencyjna, ale nie rekurencyjna . Możemy zdmuchnąć stos! Nasz próbowany dowód odkrył błąd. Możemy to naprawić, zmieniając heightsię w rekurencyjny .
Mam nadzieję, że to pokazuje, że dowody nie muszą być przerażające ani skomplikowane. W rzeczywistości za każdym razem, gdy piszesz kod, nieformalnie konstruujesz dowód w swojej głowie (w przeciwnym razie nie byłbyś przekonany, że właśnie zaimplementowałeś tę funkcję). Unikając zerowej, niepotrzebnej mutacji i nieograniczonego dziedziczenia, możesz udowodnić, że twoja intuicja jest poprawić dość łatwo. Te ograniczenia nie są tak surowe, jak mogłoby się wydawać:
null jest wadą językową i zlikwidowanie go jest bezwarunkowo dobre.- Mutacja jest czasem nieunikniona i konieczna, ale jest potrzebna o wiele rzadziej, niż się wydaje - zwłaszcza gdy masz trwałe struktury danych.
- Jeśli chodzi o posiadanie skończonej liczby klas (w sensie funkcjonalnym) / podklas (w sensie OOP) w porównaniu z nieograniczoną liczbą z nich, to temat jest zbyt duży, by dać jedną odpowiedź . Wystarczy powiedzieć, że istnieje kompromis między projektem - sprawdzalność poprawności a elastyczność rozszerzenia.