Dlaczego niezmienniki są ważne w informatyce

Rozumiem „niezmienny” w dosłownym tego słowa znaczeniu. Rozpoznaję je również po wpisaniu kodu. Ale nie sądzę, że rozumiem znaczenie tego terminu w kontekście informatyki.

Ilekroć czytam rozmowy \ białe księgi na temat projektowania języka od znanych programistów \ informatyków, termin „niezmienny” pojawia się jako żargon; i tej części nie rozumiem. Co jest takiego specjalnego w tym?

Algorytm jest procesem powtarzalnym. Jeśli jest powtarzalny, musi mieć atrybuty, które nie zmieniają się wraz z powtarzaniem. To są twoje niezmienniki. Niezmienniki są łączone i / lub działają na (potencjalnie) zmiennych danych, które zostaną wprowadzone do twojego algorytmu.

Dlatego celem programowania jest identyfikacja tego, co się nie zmienia - to w zasadzie twój program.

W programie zorientowanym obiektowo istnieje przekonanie, że każdy obiekt powinien zrobić jedną rzecz dobrze. Zasadniczo oznacza to, że (dla OOP opartego na klasach) klasa definiuje niezmienniki dla pojedynczego algorytmu wraz z elementami zastępczymi (zmiennymi) dla dowolnych wariantów danych, których mogą potrzebować jej obiekty. Idealnie byłoby w OO izolować to, co różni się tak bardzo, jak to możliwe, aby każdy obiekt był w większości niezmienny.

Pojęcie niezmiennika jest silnie powiązane z „efektami ubocznymi”. Wierzę, że został promowany przez Bertranda Meyera „Design by Contract (DbC)” do projektowania oprogramowania.

DbC wzbogaca abstrakcyjne typy danych (szkielet klas) o 3 ważne pojęcia, warunki wstępne, warunki dodatkowe, niezmienniki . Łatwo to wyjaśnić, odnosząc się do procedur, więc postaram się wyjaśnić w związku z tym:

1. Warunek reprezentuje dane wejściowe warunkiem procedura musi przestrzegać w celu wywołania tej procedury. Klient musi przestrzegać tego warunku i go egzekwować. Projektant procedury może jednak bronić się przed klientami, którzy nie spełniają warunku wstępnego, uznając ten warunek za pierwszy wiersz procedury. Na przykład posiadanie metody double divide(double dividend, double divisor)może być warunkiem wstępnym divisor != 0.

2. Postcondition reprezentuje stan na dane wyjściowe po wyjściu procedury; przestrzeganie tego warunku końcowego jest całkowicie obowiązkiem projektanta procedury, pod warunkiem że warunek ten został spełniony; w stylu programowania obronnego przed powrotem można spełnić warunek końcowy.

3. Niezmienna można traktować zarówno jako warunek wstępny i postcondition, ale z innego rozumienia za warunek wstępny oraz postcondition z powyższych pojęć. Niezmiennik zasadniczo mówi, że jeśli wejście ma określony warunek spełniony przed wywołaniem procedury, to ten konkretny warunek jest ważny po wywołaniu procedury. Na przykład prawidłowy niezmiennik dla procedury boolean search(int term, int array[])może powiedzieć, że stan arrayprzed wywołaniem jest taki sam, jak po wywołaniu.

Egzekwowanie niezmienników procedur (i nie tylko procedur) jest świetną rzeczą, ponieważ zmniejsza skutki uboczne ; jest to przydatne, ponieważ skutki uboczne są wielkim złem w programowaniu. Określona procedura może zmienić stan argumentów wejściowych lub zmienić stan niektórych zmiennych globalnych lub zależeć od niektórych zmiennych globalnych; może to prowadzić do nieprzyjemnych sytuacji, w których dwa identyczne wywołania tej samej procedury (z tym samym wejściem) mogą dawać różne wyniki. Prowadzi to do znajomości historii połączeń i jest bardzo trudne do debugowania, szczególnie w kontekście wielowątkowości.

Niezmiennik to właściwość logiczna, która jest zachowywana przez niektóre operacje.

• Potrzebujesz niezmienników do rozumowania o pętlach. Ponieważ nie wiesz z góry, ile będzie iteracji (inaczej nie potrzebujesz pętli), każda iteracja musi zachować niezmiennik, aby na końcu można było udowodnić użyteczną właściwość pętli.

• Niezbędne są niezmienniki do uzasadnienia właściwości enkapsulowanych danych. Często różne dane w module lub obiekcie muszą spełniać określone właściwości dla poprawnego działania (na przykład zawsze należy posortować listę reprezentującą zestaw). Chcesz, aby każda funkcja lub metoda działająca na danych zachowała te właściwości, więc są one również niezmienne.

Z tego, co wiem, znaczenie niezmiennika wynika z faktu, że jest to element składowy do udowodnienia, że ​​algorytm oblicza pewną funkcję. Na przykład opracowałeś nowy algorytm sortowania, ale jak możesz być pewien, że tak naprawdę sortuje się on przy każdym wejściu lub przy każdym poprawnym wyjściu. Następnym krokiem jest zbudowanie niezmienników, które odpowiadają przepływowi algorytmu i udowodnienie, że sortuje przy użyciu niezmienników.

W kontekście systemu typów w języku programowania typ niezmienny jest typem niewymienialnym. Na przykład w języku Java podczas przeciążania metody wszystkie parametry są niezmienne, a typ zwracany jest kowariantem (może być taki sam lub podtyp).