Czym są niezmienniki, jak można ich używać i czy kiedykolwiek używałeś ich w swoim programie?

48

Czytam Coders at Work , a w nim dużo mówi się o niezmiennikach. O ile rozumiem, niezmiennik jest warunkiem, który utrzymuje się zarówno przed, jak i po wyrażeniu. Przydają się między innymi do udowodnienia, że ​​pętla jest poprawna, jeśli dobrze pamiętam mój kurs logiki.

Czy mój opis jest poprawny, czy coś przeoczyłem? Czy używałeś ich kiedyś w swoim programie? A jeśli tak, to na czym skorzystali?

gablin
źródło
@Robert Harvey: Tak, właśnie to przeczytałem. Wydaje mi się jednak, że niezmienniki są użyteczne tylko wtedy, gdy próbujesz coś udowodnić. Czy to jest poprawne (bez zamierzonej gry słów)?
gablin
To jest moje zrozumienie; gdy próbujesz uzasadnić swój program, aby udowodnić jego poprawność.
Robert Harvey
3
@ user9094: Asercja jest deklaracją, że coś jest prawdą w określonym punkcie środowiska wykonawczego i jest reprezentowana w kodzie. Niezmiennik jest stwierdzeniem (jeden ma nadzieję, że jest dobrze uzasadniony), który zawsze będzie prawdziwy, gdy ma zastosowanie, i nie jest reprezentowany w samym kodzie.
David Thornley,
1
Niezmienniki są rzeczywiście przydatne do udowodnienia poprawności, ale nie są ograniczone do tego przypadku. Są również przydatne do programowania obronnego i podczas debugowania. Nie tylko pomagają udowodnić, że Twój kod jest poprawny, ale pomagają uzasadnić kod i znaleźć lokalizację błędów blisko źródeł.
Dziwne,

Odpowiedzi:

41

W OOP niezmiennikiem jest zestaw twierdzeń, które muszą zawsze być prawdziwe przez cały czas istnienia obiektu, aby program był ważny. Powinien on obowiązywać od końca konstruktora do początku destruktora, ilekroć obiekt nie wykonuje obecnie metody zmieniającej jego stan.

Przykładem niezmiennika może być to, że dokładnie jedna z dwóch zmiennych składowych powinna mieć wartość NULL. Lub, jeśli jedna ma określoną wartość, to zestaw dozwolonych wartości dla drugiej jest taki czy inny ...

Czasami używam funkcji członka obiektu, aby sprawdzić, czy niezmiennik ma. Jeśli tak nie jest, podnoszony jest aser. Metoda jest wywoływana na początku i na końcu każdej metody zmieniającej obiekt (w C ++ jest to tylko jedna linia ...)

Xavier Nodet
źródło
11
+1 za wzmiankę o niezmiennikach nie musi być prawdziwe w trakcie wykonywania metody.
Dziwne,
1
@Oddthinking Najlepiej, aby tego uniknąć, jeśli to możliwe. Łatwo byłoby wejść w stan niszczenia niezniszczalnego i zapomnieć przywrócić wszystko poprawnie przed powrotem. Wyjątki mogą również sprawiać kłopoty.
Alexander
3
@Alexander: W przypadku nietrywialnych niezmienników uniknięcie jest prawie niemożliwe. Jeśli musisz zaktualizować więcej niż jedną zmienną w metodzie, jak opisano w odpowiedzi, istnieje punkt, w którym zaktualizowano tylko jedną zmienną, a niezmiennik ma wartość false. Jest wystarczająco dużo ograniczeń dotyczących pisania dobrego kodu bez dodawania nowych.
Dziwne,
@Oddthinking Tak, często jest to zupełnie nieuniknione. Ale na przykład, jeśli istnieje grupa zmiennych, które logicznie należą do siebie (np. Tablica i indeks „wybranej” pozycji w tablicy), prawdopodobnie warto je wyodrębnić do określonego typu. Stamtąd mutacje tablicy lub typu można wyrazić jako pojedyncze przypisanie nowej instancji tego typu
Alexander
13

Cóż, rzeczy, które widzę w tym wątku, są świetne, ale mam definicję „niezmiennika”, który był dla mnie niezwykle pomocny w pracy.

Niezmiennikiem jest każda logiczna reguła, której należy przestrzegać podczas wykonywania programu, którą można przekazać człowiekowi, ale nie kompilatorowi.

Ta definicja jest pomocna, ponieważ dzieli warunki na dwie grupy: te, którym można zaufać kompilatorowi, oraz te, które należy udokumentować, omówić, skomentować lub w inny sposób przekazać współautorom, aby mogli wchodzić w interakcje z bazą kodu bez wprowadzania błędów .

Również ta definicja jest pomocna, ponieważ pozwala na zastosowanie uogólnienia „Niezmienniki są złe”.

Na przykład dźwignia zmiany biegów w samochodzie z manualną skrzynią biegów została zaprojektowana tak, aby uniknąć niezmiennika. Gdybym chciał, mógłbym zbudować skrzynię biegów z jedną dźwignią dla każdego biegu. Ta dźwignia może być do przodu („załączona”) lub do tyłu („odłączona”). W takim systemie stworzyłem „niezmiennik”, który można udokumentować jako taki:

„Bardzo ważne jest, aby aktualnie włączony bieg był wyłączany, zanim inny bieg zostanie włączony. Włączenie dowolnych dwóch biegów jednocześnie spowoduje naprężenia mechaniczne, które spowodują rozerwanie przekładni. Zawsze wyłączaj aktualnie włączony bieg, zanim włączysz inny.”

I tak można winić zepsute transmisje za niechlujną jazdę. Nowoczesne samochody używają jednak jednego drążka, który obraca się między biegami. Jest zaprojektowany w taki sposób, że w nowoczesnym samochodzie z drążkiem zmiany biegów nie można włączyć dwóch biegów jednocześnie.

W ten sposób moglibyśmy powiedzieć, że skrzynia biegów została zaprojektowana do „usunięcia niezmiennika”, ponieważ nie pozwala ona na mechaniczną konfigurację w sposób naruszający regułę logiczną.

Każdy niezmiennik tego rodzaju, który usuwasz z kodu, stanowi ulepszenie, ponieważ zmniejsza obciążenie poznawcze związane z jego obsługą.

Daniel Burbank
źródło
1
Jeśli niezmiennikiem jest jakakolwiek logiczna reguła, której należy przestrzegać podczas wykonywania programu, a twoją logiczną regułą jest to, że nie mogą być włączone jednocześnie dwa koła zębate, to nie jest niezmienne, że żadne dwa biegi nie mogą być włączone jednocześnie czas? Bez tego niezmiennego przekładnia mogłaby być na dwóch biegach jednocześnie, a tym samym rozerwać się na części. Po pierwsze, czy pojedynczy drążek zmiany biegów nie egzekwuje tego niezmiennika? Po drugie, dlaczego niezmiennik byłby z natury dobry lub zły?
Dustin Cleveland,
1
Porównanie z biegami samochodu jest dla mnie bardzo jasne. Dzięki!
Marecky
„Niezmiennikiem jest każda logiczna reguła, której należy przestrzegać podczas wykonywania programu, którą można przekazać człowiekowi, ale nie kompilatorowi”. - Podoba mi się to, zwięzłe i łatwe do zapamiętania.
ZeroKnight
@DustinCleveland Myślę, że w tym przykładzie mechanizmami przesunięcia drążka są „kompilatory”, które „egzekwują” reguły, podczas gdy sterownik, który w przeciwnym razie mógłby spowodować incydent, jest jednym z wielu klientów, którzy muszą konsumować i zapamiętywać informacje, które są zostały „udokumentowane, omówione, skomentowane lub w inny sposób przekazane”.
ebernard
Świetne wyjaśnienie! Naprawdę rozumiem teraz powód, dla którego niezmienniki w kodzie są złą praktyką.
Ben C Wang
3

Niezmiennik (w zdrowym znaczeniu) oznacza pewne warunki, które muszą być spełnione w pewnym momencie lub nawet zawsze podczas działania programu. np. PreConditions i PostConditions mogą być wykorzystane do zapewnienia pewnych warunków, które muszą być spełnione, gdy funkcja jest wywoływana i gdy zwraca. Niezmienniki obiektu mogą służyć do stwierdzenia, że ​​obiekt musi mieć prawidłowy stan przez cały czas jego istnienia. Jest to zasada „na podstawie umowy”.
Nieformalnie użyłem niezmienników, używając czeków w kodzie. Ale ostatnio bawię się biblioteką kontraktów kodowych dla .Net, która bezpośrednio obsługuje niezmienniki.

softveda
źródło
3

Na podstawie następującego cytatu z Coders At Work ...

Ale gdy poznasz niezmiennik, który utrzymuje, możesz zobaczyć, ah, jeśli utrzymamy ten niezmiennik, wówczas uzyskamy czas wyszukiwania dziennika.

... Chyba „niezmienny” = „warunek, który chcesz utrzymać, aby zapewnić pożądany efekt”.

Wydaje się, że niezmiennik ma dwa zmysły, które różnią się subtelnie:

  1. Coś, co pozostaje takie samo.
  2. Coś, co próbujesz zachować bez zmian, aby osiągnąć cel X (np. „Czas wyszukiwania dziennika” powyżej).

Więc 1 jest jak twierdzenie; 2 jest jak narzędzie do sprawdzania poprawności, wydajności lub innych właściwości - tak myślę. Zobacz artykuł z Wikipedii na przykład 2 (potwierdzający poprawność rozwiązania zagadki MU).

Właściwie trzecie poczucie niezmiennika to:

.3 Co program (lub moduł lub funkcja) ma zrobić; innymi słowy, jego cel.

Z tego samego wywiadu Coders At Work:

Ale tym, co sprawia, że ​​dużym oprogramowaniem można zarządzać, jest posiadanie globalnych niezmienników lub ogólnych oświadczeń o tym, co powinno robić i jakie rzeczy mają być prawdą.

Jonathan Aquino
źródło
1

Niezmiennik jest jak reguła lub założenie, które może być użyte do dyktowania logiki twojego programu.

Załóżmy na przykład, że masz aplikację, która śledzi konta użytkowników. Załóżmy również, że użytkownik może mieć wiele kont, ale z jakiegokolwiek powodu musisz rozróżnić konto główne użytkownika i konto „aliasowe”.

Może to być rekord DB lub coś innego, ale na razie załóżmy, że każde konto użytkownika jest reprezentowane przez obiekt klasy.

klasa userAccount {private char * pUserName; prywatny char * pParentAccountUserName;

...}

Niezmiennikiem może być założenie, że jeśli pParentAccountUserName ma wartość NULL lub jest puste, to ten obiekt jest kontem nadrzędnym. Możesz użyć tego niezmiennika do rozróżnienia różnych typów kont. Prawdopodobnie istnieją lepsze metody rozróżniania różnych typów kont użytkowników, więc pamiętaj, że to tylko przykład pokazujący, w jaki sposób można użyć niezmiennika.

Pemda
źródło
Niezmienniki sprawdzają stan programu. Nie są to decyzje projektowe.
Xavier Nodet,
3
Niezmienniki niczego nie sprawdzają. Możesz sprawdzić stan programu, aby sprawdzić, czy niezmiennikiem jest PRAWDA, czy FAŁSZ, ale same niezmienniki „nic” nie robią.
Pemdas
2
Zazwyczaj w C ++ można zaobserwować pewien rodzaj niezmienności klas, taki jak członek x musi być mniejszy niż 25 i większy niż 0. To jest niezmiennik. Wszelkie kontrole względem tego niezmiennika są twierdzeniami. W powyższym przykładzie moim niezmiennikiem jest, jeśli pParentAccountUserName ma wartość NULL lub jest puste, to jest to konto nadrzędne. Niezmienniki są projektowanymi decyzjami.
Pemdas
Jak sprawdzić, czy jeśli pParentAccountUserName ma wartość NULL lub jest puste, obiekt ten jest kontem nadrzędnym? Twoja instrukcja określa tylko, co powinna reprezentować wartość pusta / pusta. Niezmiennikiem jest to, że system jest z tym zgodny, tzn. Że pParentAccountUserName może być zerowy lub pusty tylko wtedy, gdy jest to konto nadrzędne. To subtelne rozróżnienie.
Cameron
1

Pochodząc z fizyki, w fizyce mamy niezmienniki, które są zasadniczo wielkościami, które nie zmieniają się podczas całego obliczenia / symulacji. Na przykład w fizyce dla układu zamkniętego zachowana jest całkowita energia. Lub ponownie w fizyce, jeśli zderzą się dwie cząstki, powstałe fragmenty muszą zawierać dokładnie energię, z której zaczęły, i dokładnie ten sam pęd (wielkość wektorową). Zwykle nie ma wystarczającej liczby niezmienników, aby całkowicie określić wynik. Na przykład w zderzeniu dwuczęściowym mamy cztery niezmienniki, trzy składowe pędu i składnik energetyczny, ale układ ma sześć stopni swobody (sześć liczb opisujących jego stan). Niezmienniki powinny być zachowane w ramach błędu zaokrąglania, ale ich zachowanie nie dowodzi, że rozwiązanie jest poprawne.

Zazwyczaj rzeczy te są ważne jako kontrole poczytalności, ale same w sobie nie mogą udowodnić poprawności.

Omega Centauri
źródło
1
-1 Niezmienniki w fizyce są różne. Obliczenie rozwiązania nie jest tym samym, co udowodnienie, że algorytm jest poprawny. W tym drugim przypadku niezmienniki mogą okazać się poprawne.
aaronasterling