Dlaczego tak ograniczone wsparcie dla Design by Contract w większości nowoczesnych języków programowania?

40

Niedawno odkryłem Design by Contract (DbC) i uważam, że jest to niezwykle interesujący sposób pisania kodu. Wydaje się, że oferuje między innymi:

  • Lepsza dokumentacja. Ponieważ umowa jest dokumentacją, nie można być nieaktualnym. Ponadto, ponieważ umowa określa dokładnie, co robi procedura, pomaga w ponownym użyciu.
  • Prostsze debugowanie. Ponieważ wykonywanie programu kończy się w momencie niepowodzenia umowy, błędy nie mogą się rozprzestrzeniać, a naruszone twierdzenie zostanie prawdopodobnie podświetlone. Zapewnia to wsparcie podczas projektowania i konserwacji.
  • Lepsza analiza statyczna. DbC jest w zasadzie tylko implementacją logiki Hoare i powinny obowiązywać te same zasady.

W porównaniu koszty wydają się raczej niewielkie:

  • Dodatkowe pisanie palcami. Ponieważ umowy muszą zostać określone.
  • Trwa trochę szkolenia, aby poczuć się komfortowo z pisaniem umów.

Teraz, znając przede wszystkim Pythona, zdaję sobie sprawę, że w rzeczywistości możliwe jest napisanie warunków wstępnych (po prostu wyjątki dla nieodpowiednich danych wejściowych), a nawet możliwe jest użycie asercji do ponownego przetestowania pewnych warunków dodatkowych. Ale nie można symulować niektórych funkcji, takich jak „stary” lub „wynik” bez dodatkowej magii, która ostatecznie zostałaby uznana za nie-Pythonic. (Ponadto istnieje kilka bibliotek, które oferują wsparcie, ale ostatecznie mam wrażenie, że korzystanie z nich byłoby niewłaściwe, ponieważ większość programistów tego nie robi). Zakładam, że jest to podobny problem dla wszystkich innych języków (z wyjątkiem oczywiście , Eiffel).

Moja intuicja mówi mi, że brak wsparcia musi być wynikiem pewnego rodzaju odrzucenia praktyki, ale wyszukiwanie w Internecie nie było owocne. Zastanawiam się, czy ktoś może wyjaśnić, dlaczego większość współczesnych języków wydaje się tak mało wspierać? Czy DbC jest wadliwe lub zbyt drogie? A może jest to po prostu przestarzałe z powodu Extreme Programming i innych metodologii?

Ceasar Bautista
źródło
Brzmi jak zbyt skomplikowany sposób programowania sterowanego testem, bez korzyści testowania programu.
Dan
3
@ Dan, nie bardzo, myślę o tym bardziej jako o rozszerzeniu systemu pisma. np. funkcja nie przyjmuje tylko argumentu liczby całkowitej, lecz przyjmuje liczbę całkowitą, która zgodnie z umową musi być większa od zera
Carson63000,
4
Kontrakty @Dan znacznie zmniejszają liczbę testów, które należy wykonać.
Rei Miyasaka,
24
@ Dan, wolałbym powiedzieć, że TDD to kontrakty biedaka, a nie odwrotnie.
SK-logic
W dynamicznym języku możesz „ozdobić” swoje przedmioty umowami opartymi na opcjonalnej fladze. Mam przykładową implementację, która wykorzystuje flagi środowiskowe do opcjonalnego łączenia łatek istniejących obiektów z kontraktami. Tak, obsługa nie jest natywna, ale łatwo ją dodać. To samo dotyczy uprzęży testowych, nie są one rodzime, ale można je łatwo dodawać / pisać.
Raynos

Odpowiedzi:

9

Prawdopodobnie są one obsługiwane w praktycznie każdym języku programowania.

Potrzebne są „twierdzenia”.

Można je łatwo zakodować jako instrukcje „jeśli”:

if (!assertion) then AssertionFailure();

Dzięki temu możesz pisać kontrakty, umieszczając takie asercje u góry kodu dla ograniczeń wejściowych; te w punktach powrotu są ograniczeniami wyjściowymi. Możesz nawet dodawać niezmienniki w całym kodzie (chociaż tak naprawdę nie są częścią „projektu na podstawie umowy”).

Twierdzę więc, że nie są one rozpowszechnione, ponieważ programiści są zbyt leniwi, aby je kodować, a nie dlatego, że nie można tego zrobić.

Możesz uczynić je nieco bardziej wydajnymi w większości języków, definiując stałą logiczną podczas kompilacji „sprawdzanie” i nieco poprawiając instrukcje:

if (checking & !Assertion) then AssertionFailure();

Jeśli nie podoba ci się składnia, możesz skorzystać z różnych technik abstrakcji języka, takich jak makra.

Niektóre współczesne języki dają ci niezłą składnię, i myślę, że to właśnie rozumiesz przez „wsparcie nowoczesnego języka”. To wsparcie, ale jest dość cienkie.

To, czego większość współczesnych języków nie daje, to twierdzenia „czasowe” (w stosunku do dowolnych poprzednich lub następnych stanów [operator czasowy „w końcu”], których potrzebujesz, jeśli chcesz napisać naprawdę interesujące umowy. JEŚLI instrukcje nie pomogą ty tutaj.

Ira Baxter
źródło
Problem, który mam tylko z dostępem do stwierdzeń, polega na tym, że nie ma skutecznego sposobu sprawdzenia warunków dodatkowych w poleceniach, ponieważ często trzeba porównywać stan warunkowy ze stanem warunkowym (Eiffel nazywa to „starym” i automatycznie przekazuje go do procedury postcondition .) W Pythonie tę funkcję można w prosty sposób odtworzyć przy użyciu dekoratorów, ale pojawia się ona krótko, gdy przychodzi czas na wyłączenie asercji.
Ceasar Bautista
Ile z poprzedniego stanu faktycznie oszczędza Eiffel? Ponieważ rozsądnie nie może wiedzieć, do której części można uzyskać dostęp / modyfikować bez rozwiązania problemu zatrzymania (poprzez analizę swojej funkcji), musi albo zapisać pełny stan maszyny, albo, jako hueristic, tylko niektóre bardzo płytkie części. Podejrzewam to drugie; i mogą one być „symulowane” przez proste przypisania skalarne przed warunkiem wstępnym. Z przyjemnością dowiem się, że Eiffel robi inaczej.
Ira Baxter
7
... właśnie sprawdziłem, jak działa Eiffel. „old <exp>” to wartość <exp> przy wejściu do funkcji, więc robi płytkie kopie przy wejściu do funkcji, jak się spodziewałem. Ty też możesz to zrobić. Zgadzam się, że kompilator implementujący składnię dla pre / post / old jest wygodniejszy niż robienie tego wszystkiego ręcznie, ale chodzi o to, że można to zrobić ręcznie i to naprawdę nie jest trudne. Wróciliśmy do leniwych programistów.
Ira Baxter
@IraBaxter Nie. Kod staje się prostszy, jeśli można oddzielić umowę od rzeczywistej logiki. Ponadto, jeśli kompilator może powiedzieć umowy i kod siebie, może to zmniejszyć powielania przez wielu . Np. W D możesz zadeklarować umowę dotyczącą interfejsu lub nadklasy, a twierdzenia zostaną zastosowane do wszystkich klas implementujących / rozszerzających, niezależnie od kodu w ich funkcjach. Np. W Pythonie lub Javie musisz wywołać całą supermetodę i ewentualnie wyrzucić wyniki, jeśli chcesz sprawdzić kontrakty bez powielania. To naprawdę pomaga w implementacji czystego kodu zgodnego z LSP.
marstato,
@marstato: Już się zgodziłem, że wsparcie w języku jest dobrą rzeczą.
Ira Baxter,
15

Jak mówisz, Design by Contract to funkcja w Eiffel, która od dawna jest jednym z tych języków programowania, który jest powszechnie szanowany w społeczności, ale który nigdy się nie przyjął.

DbC nie jest w żadnym z najpopularniejszych języków, ponieważ stosunkowo niedawno społeczność programistów głównego nurtu przyjęła do wiadomości, że dodanie ograniczeń / oczekiwań do kodu jest „rozsądną” rzeczą, której można oczekiwać od programistów. Teraz programiści często rozumieją, jak cenne jest testowanie jednostkowe, co sprowadza się do tego, że programiści bardziej akceptują wprowadzanie kodu w celu weryfikacji swoich argumentów i dostrzegania korzyści. Ale dekadę temu zapewne większość programistów powiedziałaby „to tylko dodatkowa praca dla rzeczy, o których wiesz, że zawsze będą w porządku”.

Myślę, że gdybyś dzisiaj poszedł do przeciętnego programisty i porozmawiał o post-warunkach, entuzjastycznie skinąłby głową i powiedział: „OK, to jak testowanie jednostkowe”. A jeśli mówisz o warunkach wstępnych, powiedzą „OK, to jest jak sprawdzanie poprawności parametrów, co nie zawsze robimy, ale wiesz, myślę, że jest ok ...” A potem, jeśli mówisz o niezmiennikach , zaczęliby mówić: „Ojej, ile to narzutów? Ile jeszcze błędów będziemy łapać?” itp.

Myślę więc, że zanim DbC zostanie bardzo szeroko przyjęte, jest jeszcze wiele do zrobienia.

Larry OBrien
źródło
OTOH, programiści głównego nurtu byli przyzwyczajeni do pisania asercji dość długo. Brak użytecznego preprocesora w najnowocześniejszych językach głównego nurtu sprawił, że ta przyjemna praktyka była nieefektywna, ale nadal jest powszechna w C i C ++. Powraca teraz dzięki Microsoft Code Contracts (na podstawie AFAIK, przepisywania kodu bajtowego dla kompilacji wersji).
SK-logic
8

Moja intuicja mówi mi, że brak wsparcia musi wynikać z pewnego rodzaju odrzucenia praktyki ...

Fałszywe.

To praktyka projektowa . Może być wcielony jawnie w kodzie (styl Eiffla) lub pośrednio w kodzie (większość języków) lub w testach jednostkowych. Praktyka projektowania istnieje i działa dobrze. Obsługa języków jest dostępna na całej mapie. Jest jednak obecny w wielu językach w ramach testu jednostkowego.

Zastanawiam się, czy ktoś może wyjaśnić, dlaczego większość współczesnych języków wydaje się tak mało wspierać? Czy DbC jest wadliwe lub zbyt drogie?

To jest drogie I. Co ważniejsze, są pewne rzeczy, których nie można udowodnić w danym języku. Na przykład zakończenia pętli nie można udowodnić w języku programowania, wymaga ona zdolności sprawdzania „wyższego rzędu”. Tak więc niektóre rodzaje umów są technicznie niewyrażalne.

A może jest to po prostu przestarzałe z powodu Extreme Programming i innych metodologii?

Nie.

Najczęściej stosujemy testy jednostkowe, aby wykazać, że DbC jest spełnione.

W przypadku Pythona, jak zauważyłeś, DbC działa w kilku miejscach.

  1. Wyniki testu docstring i docstring.

  2. Asercje potwierdzające dane wejściowe i wyjściowe.

  3. Testy jednostkowe.

Dalej.

Możesz adoptować narzędzia w stylu programowania, aby pisać dokument, który zawiera informacje o DbC i który generuje czyste skrypty testu jednostkowego w języku Python plus. Umiejętne programowanie pozwala napisać niezłą literaturę, która zawiera umowy i kompletne źródło.

S.Lott
źródło
Możesz udowodnić trywialne przypadki zakończenia pętli, takie jak iteracja po ustalonej skończonej sekwencji. Jest to uogólniona pętla, której nie można pokazać w sposób trywialny (ponieważ może to być poszukiwanie rozwiązań dla „interesujących” matematycznych przypuszczeń); to cała istota problemu zatrzymania.
Donal Fellows
+1. Myślę, że jesteś jedynym, który omówił najbardziej krytyczny punkt - there are some things which cannot be proven. Formalna weryfikacja może być świetna, ale nie wszystko jest weryfikowalne! Ta funkcja faktycznie ogranicza możliwości języka programowania!
Dipan Mehta
@DonalFellows: Ponieważ nie można udowodnić ogólnego przypadku, trudno jest wprowadzić wiele funkcji, które są (a) drogie i (b) znane jako niekompletne. Chodzi mi o to, że łatwiej jest ominąć wszystkie te cechy i unikać ustanawiania fałszywych oczekiwań co do formalnych dowodów poprawności w ogóle, gdy istnieją ograniczenia. Jako ćwiczenie projektowe (poza językiem) można (i należy) zastosować wiele technik sprawdzających.
S.Lott,
Nie jest wcale drogi w języku takim jak C ++, w którym sprawdzanie kontraktów kompiluje się w kompilacji wydania. Używanie DBC prowadzi do wydania mniejszego kodu kompilacji, ponieważ wprowadzasz mniej kontroli czasu wykonywania, aby program był w stanie prawnym. Straciłem rachubę dużej liczby baz kodu, które widziałem, gdzie liczne funkcje sprawdzają stan nielegalny i zwracają wartość false, kiedy NIGDY nie powinien być w tym stanie w poprawnie przetestowanej wersji wydania.
Kaitain
6

Tylko zgaduję. Być może po części nie jest tak popularny, ponieważ „Design by Contract” jest znakiem towarowym firmy Eiffel.

DPD
źródło
3

Jedna hipoteza jest taka, że ​​w przypadku wystarczająco dużego złożonego programu, zwłaszcza z ruchomym celem, sama masa umów może stać się tak samo wadliwa i trudna do debugowania, a nawet bardziej, niż sam kod programu. Jak w przypadku każdego wzorca, użycie może być mniejsze niż w przeszłości, a także wyraźne zalety, gdy jest stosowany w bardziej ukierunkowany sposób.

Innym możliwym wnioskiem jest to, że popularność „języków zarządzanych” jest aktualnym dowodem wsparcia projektowania według umowy dla wybranych wybranych zarządzanych funkcji (ograniczenia tablic według umów itp.)

hotpaw2
źródło
> masa samych umów może stać się tak samo wadliwa i trudna do debugowania, a nawet bardziej niż sam kod programu, którego nigdy nie widziałem.
Kaitain
2

Powodem, dla którego większość popularnych języków nie ma funkcji DbC w języku jest stosunek kosztów do korzyści związanych z jego wdrożeniem, jest on zbyt wysoki dla implementatora języka.

jedna strona tego została już omówiona w innych odpowiedziach, testy jednostkowe i inne mechanizmy wykonawcze (lub nawet niektóre mechanizmy kompilacji czasu z szablonowym meta programowaniem) mogą już dać ci wiele z dobroci DbC. Dlatego, chociaż istnieje korzyść, prawdopodobnie jest postrzegana jako dość skromna.

Druga strona to koszt, retro dostosowanie DbC do istniejącego języka jest prawdopodobnie zbyt dużą przełomową zmianą i bardzo skomplikowane do uruchomienia. Wprowadzenie nowej składni w języku bez łamania starego kodu jest trudne. Aktualizacja istniejącej standardowej biblioteki w celu zastosowania tak daleko idącej zmiany byłaby kosztowna. Dlatego możemy stwierdzić, że wdrożenie funkcji DbC w istniejącym języku wiąże się z wysokimi kosztami.

Chciałbym również zauważyć, że koncepcje, które są prawie umowami na szablony, a zatem są nieco związane z DbC, zostały porzucone z najnowszego standardu C ++, ponieważ nawet po latach pracy nad nimi oszacowano, że wciąż potrzebowali lat pracy. Tego rodzaju duże, szerokie i rozległe zmiany w językach są po prostu zbyt trudne do wdrożenia.

jk.
źródło
2

DbC byłoby wykorzystywane w szerszym zakresie, gdyby kontrakty mogły być sprawdzane w czasie kompilacji, aby nie było możliwe uruchomienie programu, który naruszyłby jakąkolwiek umowę.

Bez obsługi kompilatora „DbC” to po prostu inna nazwa dla „sprawdzania niezmienników / założeń i zgłaszania wyjątku w przypadku naruszenia”.

Ingo
źródło
Czy to nie napotyka problemu zatrzymania?
Ceasar Bautista
@Ceasar To zależy. Niektóre założenia można sprawdzić, inne nie. Na przykład istnieją systemy typów, które pozwalają uniknąć podania pustej listy jako argumentu lub jej zwrócenia.
Ingo
Fajna uwaga (+1), chociaż Bertrand Meyer w swojej części „Masterminds of programowania” wspomniał także o ich systemie losowego tworzenia klas i sprawdzania połączeń pod kątem naruszenia umów. Jest to więc podejście oparte na mieszanym czasie kompilacji i czasie wykonywania, ale wątpię, aby ta technika działała w każdej sytuacji
Maksee,
Jest to do pewnego stopnia prawdziwe, chociaż powinna to być katastrofalna awaria, a nie wyjątek (patrz poniżej). Kluczową zaletą DBC jest metodologia, która faktycznie prowadzi do lepiej zaprojektowanych programów, oraz pewność, że każda metoda MUSI być w stanie prawnym po wejściu, co upraszcza wiele wewnętrznej logiki. Zasadniczo nie powinieneś zajmować się zgłaszaniem wyjątków w przypadku naruszenia umowy. Należy zastosować wyjątki, w których program PRAWNIE może znajdować się w stanie ~ X, a kod klienta musi to obsłużyć. Umowa mówi, że ~ X jest po prostu nielegalne.
Kaitain
1

Mam proste wyjaśnienie, większość ludzi (w tym programiści) nie chce dodatkowej pracy, chyba że uzna to za konieczne. Programowanie awioniki, w której bezpieczeństwo jest uważane za bardzo ważne Nie widziałem bez niego większości projektów.

Ale jeśli zastanawiasz się nad witryną, komputerem lub programowaniem mobilnym - awarie i nieoczekiwane zachowanie czasami nie jest uważane za złe, a programiści unikają dodatkowej pracy przy zgłaszaniu błędów, a później ich naprawianie jest uważane za wystarczające.

Jest to prawdopodobnie powód, dla którego myślę, że Ada nigdy nie wybrała się poza branżę programowania lotniczego, ponieważ wymaga więcej pracy przy kodowaniu, chociaż Ada jest niesamowitym językiem, a jeśli chcesz zbudować niezawodny system, jest to najlepszy język do pracy (z wyjątkiem SPARK, który jest zastrzeżony) język oparty na Adzie).

Biblioteki kontraktowe zaprojektowane dla C # były eksperymentalne przez Microsoft i są bardzo przydatne do budowy niezawodnego oprogramowania, ale nigdy nie nabrały rozpędu na rynku, w przeciwnym razie widzielibyście je teraz jako część podstawowego języka C #.

Twierdzenia to nie to samo, co w pełni funkcjonalne wsparcie dla warunków przed / po i niezmienne. Chociaż może próbować je emulować, ale język / kompilator z odpowiednią obsługą wykonuje analizę „abstrakcyjnego drzewa składni” i sprawdza błędy logiczne, których zwykłe twierdzenia nie potrafią.

Edycja: Przeprowadziłem wyszukiwanie, a następna związana jest dyskusja, która może być pomocna: https://stackoverflow.com/questions/4065001/are-there-any-provable-real-world-languages-scala

SIANO
źródło
-2

Przeważnie przyczyny są następujące:

  1. Jest dostępny tylko w językach, które nie są popularne
  2. Jest to zbędne, ponieważ każdy, kto chce to zrobić, może to zrobić inaczej w istniejących językach programowania
  3. Jest trudny do zrozumienia i użycia - wymaga specjalistycznej wiedzy, aby zrobić to poprawnie, więc jest to niewielka liczba osób
  4. wymaga do tego dużej ilości kodu - programiści wolą zminimalizować liczbę pisanych znaków - jeśli zajmuje to dużo czasu, coś musi być z tym nie tak
  5. zalety nie istnieją - po prostu nie można znaleźć wystarczającej liczby błędów, aby było warto
tp1
źródło
1
Twoja odpowiedź nie jest dobrze uzasadniona. Po prostu wyrażasz swoją opinię, że nie ma żadnych korzyści, że wymaga dużej ilości kodu i że nie jest to konieczne, ponieważ można to zrobić przy użyciu istniejących języków (PO specjalnie rozwiązał ten problem!).
Andres F.
Nie myślę o twierdzeniach itp. Jako ich zamienniku. To nie jest poprawny sposób na zrobienie tego w istniejących językach. (Tzn. Nie zostało to jeszcze rozwiązane)
tp1
@ tp1, jeśli programiści naprawdę chcieliby zminimalizować pisanie, nigdy nie wpadliby w coś tak gadatliwego i wymownego jak Java. I tak, samo programowanie wymaga „specjalistycznej wiedzy” „, aby zrobić to poprawnie”. Osoby nie posiadające takiej wiedzy po prostu nie powinny mieć prawa do kodowania.
SK-logic
@ Sk-logic: Wygląda na to, że połowa świata robi OO źle tylko dlatego, że nie chce zapisywać funkcji przekazywania z funkcji składowych do funkcji składowych członków danych. To duży problem z mojego doświadczenia. Jest to bezpośrednio spowodowane minimalizacją liczby znaków do napisania.
tp1
@ tp1, jeśli ludzie naprawdę chcieliby zminimalizować pisanie, nigdy nawet nie dotkną OO. OOP jest naturalnie wymowny, nawet w swoich najlepszych implementacjach, takich jak Smalltalk. Nie powiedziałbym, że to zła właściwość, elokwencja czasami pomaga.
SK-logic