Jakie bariery uniemożliwiają powszechne przyjęcie metod formalnych? [Zamknięte]

14

Formalnych metod można użyć do określenia, udowodnienia i wygenerowania kodu dla aplikacji. Jest to mniej podatne na błędy - dlatego najczęściej stosowane w programach bezpieczeństwa / krytycznych.

Dlaczego nie używamy go częściej do codziennego programowania, aplikacji internetowych itp.?

Bibliografia :

Toto
źródło
3
Mogliśmy budować domy o grubości 5 stóp - jak średniowieczne zamki. Przez większość czasu byłoby to więcej kłopotów niż jest to warte.
Baldrickk
5
Możesz spróbować zastosować formalne metody do projektu web dev i przekonać się, jak to działa. Najprawdopodobniej zauważysz, że wkładasz dużo wysiłku w działalność o niskiej wartości. Porównaj to z szybkimi testami dymu, które już wychwycą wiele błędów. Co ciekawe, systemy typu statycznego są prostym rodzajem systemu dowodowego, jednak szczególnie web development unika tych języków (zamiast tego preferuje bardzo dynamiczne języki, takie jak Ruby, PHP lub JavaScript). Korelacja nie implikuje związku przyczynowego, ale daje do myślenia.
amon
1
Wolisz więc podać język specyfikacji zamiast programowania w języku programowania? Ok, będziesz w stanie udowodnić, że działa zgodnie ze specyfikacją. Ale jak udowodnisz, że specyfikacja odzwierciedla prawdziwy problem?
Christophe,
3
@toto pytanie brzmi: robienie rzeczy we właściwy sposób (praca zgodnie ze specyfikacjami) lub robienie właściwych rzeczy (posiadanie dobrych specyfikacji). Podczas gdy teoretycznie specyfikacja jest tym, czego chcemy, w praktyce rzadko wiemy na pewno, co jest naprawdę potrzebne: beyssonmanagement.com/2012/10/29/…
Christophe
3
Dla tych, którzy są rozczarowani, że to jest zamknięte, jest teraz świetny post na blogu: Dlaczego ludzie nie używają metod formalnych?
icc97

Odpowiedzi:

19

Inżynier to osoba, która może zrobić z dolarem to, co każdy idiota może zrobić z 10.

Ograniczenia zasobów, ograniczenia budżetowe, ograniczenia czasowe - wszystkie są ważne.

Tworzenie oprogramowania przy użyciu metod formalnych jest zwykle znacznie droższe i trwa znacznie dłużej niż bez niego. Ponadto w przypadku wielu projektów najtrudniejszą częścią jest zrozumienie wymagań biznesowych. Wszystko, co przy użyciu metod formalnych kupuje w takim przypadku, jest dowodem, że Twój kod odpowiada w 100% niekompletnemu i niepoprawnemu zrozumieniu wymagań biznesowych.

Z tego powodu stosowanie formalnych metod, dowodów, weryfikacji programu i podobnych technik jest zwykle ograniczone do „rzeczy, które mają znaczenie”, tj. Oprogramowania awioniki, systemów kontroli sprzętu medycznego, elektrowni itp.

Jörg W Mittag
źródło
1
Dodałbym również, że wprowadzenie formalnych metod do języka programowania jest obecnie obszarem aktywnych badań, tzn. Nie jest jeszcze gotowe do włączenia do głównego nurtu
jk.
1
Akceptuję tę odpowiedź, ale chciałem również podejść do tego, dlaczego metody formalne są nadal uważane za „drogie” i „czasochłonne”, zwłaszcza gdy wiemy, jak drogie jest utrzymanie i śledzenie / debugowanie kodu w dużych projektach.
toto
1
TDD i BDD są podejściami zbudowanymi na zasadach logiki Hoare'a, stanowiących podstawę podejść formalnych. Poprawiają wydajność, nie umniejszając jej.
Martin Spamer,
1
@toto Dowody są naprawdę, NAPRAWDĘ trudne. Wiele rzeczy, które matematycy uważają za oczywiste w dowodach, nie ma zastosowania w programach. Na przykład, w C ++, dodatek nie jest łączne: (-1 + 1) + INT_MAX = INT_MAX, -1 + (1 + INT_MAX)jest niezdefiniowane zachowanie.
Hovercouch
1
@toto: Uważa się je za „drogie” i „czasochłonne”, ponieważ możemy przyjrzeć się projektom opracowanym przy użyciu metod formalnych i empirycznie zweryfikować, czy opracowanie tych projektów trwa znacznie dłużej. Spójrz na czas rozwoju seL4 / L4. Zweryfikowany, na przykład, w porównaniu do jakiejkolwiek innej implementacji L4.
Jörg W Mittag
12

Programować czy nie programować?

Aby rozwiązać problem z oprogramowaniem, po zapoznaniu się z wymaganiami możesz EITHER napisać program przy użyciu języków programowania LUB określić program przy użyciu języka formalnego i użyć narzędzi do generowania kodu. Ten ostatni dodaje poziom abstrakcji.

Czy robisz to dobrze, czy robisz dobrze?

Podejście formalne daje dowód, że oprogramowanie działa zgodnie ze specyfikacjami. Twój produkt robi to dobrze. Ale czy robi to dobrze?

Wymagania, nad którymi pracujesz, mogą być niepełne lub niejednoznaczne. Mogą nawet mieć problemy. W najgorszym przypadku rzeczywiste potrzeby nie są nawet wyrażone. Ale zdjęcie jest warte tysiąca słów, wystarczy użyć obrazów Google dla „Czego chce klient”, na przykład z tego artykułu :

wprowadź opis zdjęcia tutaj

Koszt formalności

W idealnym świecie od samego początku miałbyś w pełni szczegółowe i idealne wymagania. Następnie możesz w pełni określić swoje oprogramowanie. Jeśli zdecydujesz się na formalny, kod zostanie wygenerowany automatycznie, dzięki czemu będziesz bardziej produktywny. Wzrost wydajności zrównoważyłby koszty narzędzi formalnych. I wszyscy teraz używaliby metod formalnych. Dlaczego więc nie jest?

W praktyce rzadko jest to rzeczywistością! Właśnie dlatego tak wiele projektów wodospadu nie powiodło się i dlaczego wiodące były metody iteracyjne (zwinne, RAD itp.): Potrafią poradzić sobie z niekompletnymi i niedoskonałymi wymaganiami, projektami i implementacjami oraz dopracować je, dopóki nie będą w porządku.

I tu chodzi o sedno. W przypadku metod formalnych każda iteracja wymaga posiadania całkowicie spójnej specyfikacji formalnej. Wymaga to starannego myślenia i dodatkowej pracy, ponieważ logika formalna nie wybacza i nie lubi niekompletnych myśli. Proste eksperymenty z wyrzucaniem stają się kosztowne pod tym ograniczeniem. Podobnie dzieje się z każdą iteracją, która doprowadziłaby do wycofania się (np. Pomysł, który nie zadziałał lub wymaganie, które zostało źle zrozumiane).

W praktyce

Gdy nie jest się zobowiązanym do korzystania z metod formalnych z przyczyn prawnych lub umownych, można również osiągnąć bardzo wysoką jakość bez formalnych systemów, na przykład stosując programowanie oparte na umowie i inne dobre praktyki (np. Przegląd kodu, TDD itp.). Nie będziesz w stanie udowodnić, że twoje oprogramowanie działa, ale Twoi użytkownicy będą mogli cieszyć się działającym oprogramowaniem wcześniej.

Aktualizacja: zmierzony wysiłek

W wydanym w październiku 2018 r. Wydaniu Communications of ACM znajduje się interesujący artykuł na temat formalnie zweryfikowanego oprogramowania w świecie rzeczywistym, zawierający niektóre szacunki nakładu pracy.

Co ciekawe (w oparciu o rozwój systemu operacyjnego dla sprzętu wojskowego) wydaje się, że formalnie udowodnione oprogramowanie wymaga 3,3 razy więcej wysiłku niż w przypadku tradycyjnych technik inżynieryjnych. To jest naprawdę kosztowne.

Z drugiej strony, uzyskanie 2,3 razy mniejszego wysiłku, aby uzyskać oprogramowanie o wysokim bezpieczeństwie w ten sposób niż w przypadku tradycyjnie opracowanego oprogramowania, jeśli dodasz wysiłek, aby takie oprogramowanie było certyfikowane na wysokim poziomie bezpieczeństwa (EAL 7). Tak więc, jeśli masz wysokie wymagania dotyczące niezawodności lub bezpieczeństwa, to zdecydowanie jest uzasadnienie biznesowe do formalnego.

Projekt i opracowanie kodu seL4 zajęło dwie osoby na lata. Zsumowanie wszystkich dowodów serospecyficznych na przestrzeni lat daje w sumie 18 osobolat dla 8700 linii kodu C. Dla porównania, opracowanie L4Ka :: Pistachio, kolejnego mikrojądra w rodzinie L4, porównywalnego pod względem wielkości z seL4, zajęło sześć osobolat, i nie zapewnia znaczącego poziomu pewności. Oznacza to, że istnieje tylko współczynnik 3.3 między zweryfikowanym oprogramowaniem a tradycyjnie opracowanym oprogramowaniem. Według metody szacowania Colberta i Boehm'a 8, tradycyjna certyfikacja Common Criteria EAL7 dla 8700 linii kodu C zajęłaby ponad 45,9 osobolat. Oznacza to, że formalna weryfikacja implementacji na poziomie binarnym jest już ponad 2,3 mniej kosztowne niż najwyższy poziom certyfikacji Common Criteria, ale zapewnia znacznie lepszą pewność.

Christophe
źródło
Programowanie kontraktowe wykorzystuje przynajmniej nieformalne dowody.
Frank Hileman
@FrankHileman tak! A sam fakt wyjaśnienia warunków wstępnych, późniejszych i niezmiennych znacznie pomaga w efektywnym przeglądaniu kodu, ograniczaniu błędów i usystematyzowaniu testów.
Christophe
To zdecydowanie najlepsza odpowiedź.
Hashim
0

Każdy program w dowolnym języku może być traktowany jako formalna specyfikacja (odpowiednik jakiejś tokarki). Każda „formalna specyfikacja” wyższego poziomu, którą należy zastosować w celu udowodnienia poprawności formalnej, jest także - po prostu innym programem. Ale to (zwykle) zły, niekompletny, niejasny, niewystarczająco przemyślany program. I nieprzypadkowo, zwykle napisane przez ludzi, którzy nie wiedzą, jak programować (zwykle są ekspertami w dziedzinie).

Udowadniając, że jeden program jest kompatybilny (daje te same odpowiedzi lub niezależnie od tego, jak go charakteryzujesz) z jego wymogami formalnymi wyższego poziomu, niezmienny sprowadza się do sposobu rozwiązywania dwuznaczności w specyfikacji formalnej wyższego poziomu. Nie ma na to dobrego sposobu ogólnego przeznaczenia.

To odwzorowanie wymagań wysokiego poziomu na szczegóły niższego poziomu stanowi sedno prawdziwego programowania. Nie powinno dziwić, że podstawowa praca wykonywana przez programistę czytającego i interpretującego specyfikację nie może być zastąpiona machaniem ręką i mówieniem „teraz wystarczy sprawdzić, czy ten przykładowy program spełnia tę wysoką specyfikację formalną”.

Nawet we wczesnych dniach programowania logicznego, gdzie ta koncepcja wydawała się tak obiecująca (ponieważ zarówno specyfikacja wysokiego poziomu, jak i rzeczywiste programy bazowe mogły być napisane w tym samym języku), ten podstawowy problem okazał się trudny do rozwiązania.

Lewis Pringle
źródło