Jeśli nauczyłeś się formalnych metod dla oprogramowania, w jaki sposób je znalazłeś?

Jeśli zostałeś przeszkolony w zakresie korzystania z metod formalnych (FM) do programowania:

• Jak bardzo Ci się podobało?
• Na czym polegało twoje szkolenie FM (np. Kurs, książka)?
• Z jakich narzędzi FM korzystasz?
• Jakie zalety ma szybkość / jakość w porównaniu z nieużywaniem FM?
• Jakie oprogramowanie tworzysz za pomocą FM?
• A jeśli nie używasz teraz FM bezpośrednio, czy warto było się uczyć?

Jestem ciekawy, aby usłyszeć tyle doświadczeń / opinii na temat FM, ile można znaleźć w tej społeczności; Zaczynam o tym czytać i chcę wiedzieć więcej.

tło

Programowanie i rozwój / inżynieria oprogramowania to jedne z najnowszych ludzkich umiejętności / zawodów na Ziemi, więc nic dziwnego, że pole jest niedojrzałe - co pokazuje główny wynik naszej dziedziny, jako kod, który jest zwykle spóźniony i podatny na błędy. Niedojrzałość branży przejawia się również w szerokim marginesie (co najmniej 10: 1) w wydajności pomiędzy średnią a najlepszymi programistami. Takie ponure fakty są dobrze omówione w literaturze i przedstawione w książkach takich jak Steve McConnell's Code Complete .

Wykorzystanie metod formalnych (FM) zostało zaproponowane przez główne postacie w oprogramowaniu / CS (np. Nieżyjącego E. Dijkstry ) w celu zaradzenia (jednej z) podstawowych przyczyn błędów: braku matematycznego rygoru w programowaniu. Na przykład Dijkstra opowiadał się za wspólnym opracowaniem programu i jego dowodu .

FM wydaje się być znacznie bardziej rozpowszechniony w programach CS w Europie niż w USA. Ale w ciągu ostatnich kilku lat nowe „lekkie” podejścia FM i narzędzia, takie jak Alloy , przyciągnęły pewną uwagę. Nadal jednak FM nie jest powszechnym zastosowaniem w przemyśle i mam nadzieję, że otrzymam informację zwrotną na temat tego, dlaczego.

Aktualizacja

Na dzień dzisiejszy (14.10.2010), spośród 6 poniższych odpowiedzi, nikt nie poparł wyraźnie użycia FM w pracy w „świecie rzeczywistym”. Jestem naprawdę ciekawy, czy ktoś może i chce; a może FM naprawdę ilustruje podział na środowisko akademickie (FM to przyszłość!) i przemysł (FM jest w większości bezużyteczny).

Absolutnie bezużyteczne dla wszystkiego, co nieistotne.

Miałem kurs zatytułowany „Metody formalne”, który koncentrował się na stopie - nigdzie nie widzę, aby go można było użyć. Miał inną klasę, która koncentrowała się na modelowaniu współbieżności z LTSA - równie bezużyteczna.

Problem polega na tym, że większość błędów i problemów w oprogramowaniu (przynajmniej z mojego doświadczenia) wynika ze złożoności, która występuje poniżej poziomu abstrakcji tych narzędzi.

Mam doświadczenie w CSP (Communicating Sequential Processs). Nie trącić własnym rogiem, ale napisałem pracę magisterską na temat Timed CSP, w szczególności „kompilując” specyfikacje napisane metodami formalnymi do wykonywalnego C ++. Mogę powiedzieć, że mam pewne doświadczenie z metodami formalnymi. Kiedy skończyłem studia i dostałem pracę w branży, w ogóle nie stosowałem metod formalnych. Metody formalne są wciąż zbyt teoretyczne, aby można je było stosować w przemyśle. Metody formalne znalazły praktyczne zastosowanie w dziedzinie systemów wbudowanych. Na przykład NASA stosuje formalne metody w swoich projektach. Spekulowałbym, że metody formalne są bardzo dalekie od szerokiego zastosowania w branży. Po prostu nie ma sensu pisać specyfikacji oprogramowania metodami formalnymi, a następnie „interpretować” je przez człowieka według własnego wyboru. Zwykły angielski i diagramy działają do tego lepiej, podczas gdy testy jednostkowe i integracyjne wykonują całkiem niezłą robotę „weryfikując” poprawność kodu. Myślęmetody formalne pozostaną w świecie akademickim przez pewien czas .

Diagramy stanów i sieci Petriego są przydatne do modelowania i analizy protokołów i systemów czasu rzeczywistego. Najpierw pomagają zaprojektować rozwiązanie. Po drugie, pomagają znaleźć przypadki testowe dla ekscytującego oprogramowania w bardzo specyficznych sytuacjach.

Przeczytałem kilka książek o metodach formalnych i zastosowałem kilka. Moja natychmiastowa reakcja brzmiała: „Ojej, te książki mówią mi, jak być dobrym programistą, dopóki jestem doskonałym matematykiem”. Kolejną słabością jest to, że można udowodnić równoważność tylko z innym formalnym opisem. Napisanie formalnej specyfikacji programu jest równoznaczne z napisaniem programu w języku wyższego poziomu i nie ma sposobu, aby uniknąć wprowadzenia błędów w dość dużej specyfikacji.

Nigdy nie sprawiłem, że metody formalne działają na dużą skalę. Mogą być przydatne w uzyskaniu czegoś małego i trudnego do poprawienia oraz w przekonaniu mnie, że są poprawne. W ten sposób mogę pracować z nieco większymi blokami konstrukcyjnymi i czasami mogę zrobić trochę więcej.

Jedną rzeczą, którą wybrałem, która jest bardziej użyteczna, jest koncepcja niezmiennika, stwierdzenie o programie i jego stanie, które jest zawsze prawdziwe. Wszystko, z czego możesz rozumować, jest dobre.

Jak wspomniano powyżej, nie jestem doskonałym matematykiem, więc moje dowody czasami zawierają błędy. Z mojego doświadczenia wynika jednak, że są to duże głupie błędy, które można łatwo złapać i naprawić.

Ukończyłem kurs dla absolwentów formalnej analizy programów, gdzie skupiliśmy się na semantyce operacyjnej. Zrobiłem swój ostatni artykuł na temat wysiłku seL4, przeglądając stosowane przez nich metody formalne. Pod względem praktycznym moim głównym podejściem było to, że ma ono wartość marginalną. Nie tylko musisz napisać program, musisz napisać dowód. Łał. Dwa źródła błędów. Nie tylko jeden. Ponadto na rzeczywisty kod nałożono ogromną liczbę ograniczeń. Bardzo trudno jest formalnie opisać fizyczny komputer, w tym także operacje wejścia / wyjścia.

Samouka TLA + w zeszłym roku, używam go od tego czasu. Jest to jedno z pierwszych narzędzi, do których sięgam po rozpoczęciu projektu. Błąd, jaki popełniają większość ludzi, zakłada, że ​​metody formalne to wszystko albo nic: albo nie używasz metod formalnych, albo masz całkowitą weryfikację. Jest jednak coś między nimi: specyfikacja formalna , w której sprawdza się, czy abstrakcyjna specyfikacja projektu nie psuje niezmienników. W przeciwieństwie do weryfikacji, specyfikacja jest wystarczająco praktyczna, aby można ją było zastosować w przemyśle.

Języki specyfikacji są bardziej wyraziste niż języki programowania. Na przykład, oto (bardzo) prosta specyfikacja PlusCal dla rozproszonego magazynu danych:

process node \in 1..5 \* Nodes
variables online = TRUE,
          stored \in SUBSET data; \* Some set
begin 
  Transfer:
    either
      with node \in Nodes, datum \in stored do
        node.stored := node.stored \union {datum};
      end
    or \* crash
      online := FALSE;
    end either;
end process;

Ten fragment określa pięć węzłów działających jednocześnie, wykonujących transfery w dowolnej kolejności, przy czym każdy transfer jest dowolną częścią danych do dowolnego węzła. Ponadto ustaliliśmy, że dowolny transfer może się nie powieść i spowodować awarię węzła. I możemy symulować wszystkie te zachowania w module sprawdzania modelu TLA +! W ten sposób możemy przetestować, że niezależnie od zamówienia, wskaźnika awaryjności itp. Nasze wymagania nadal obowiązują. Mówiąc o tym, dodajmy kilka wymagań. Po pierwsze, że nigdy nie przesyłamy danych do węzła offline:

[][\A node \in Nodes: ~online => UNCHANGED node.stored]_vars

W naszej uproszczonej wersji moduł sprawdzania modelu znajdzie stan awarii. Możemy również określić „dowolny fragment danych znajduje się w co najmniej jednym węźle online”:

\A d \in data: \E n \in Nodes: n.online /\ d \in n.stored

Co również się nie powiedzie. Powodzenia w sprawdzaniu ich za pomocą testu jednostkowego!

Głównym ograniczeniem specyfikacji jest to, że istnieje ona niezależnie od faktycznego kodu. Może tylko powiedzieć, że twój projekt jest poprawny, a nie, że poprawnie go wdrożyłeś. Ale szybsze jest określenie niż weryfikacja i wychwytywanie błędów, które są zbyt subtelne do testowania, więc uważam, że warto. Prawie każdy kod obejmujący współbieżność lub wiele systemów jest dobrym miejscem na formalną specyfikację.

Pracowałem w dziale w ICL, zanim zostały wykupione przez Fujitsu. Mieli duże kontrakty rządowe, które wymagały dowodu, że oprogramowanie działało zgodnie z reklamą, więc zbudowali maszynę, która przyjmowałaby formalną specyfikację napisaną w Z i sprawdzała poprawność kodu podczas pracy, z dużym zielonym lub czerwonym światłem dla przepustki / zawieść.

To była niesamowita rzecz, ale, jak podkreśla ceniony @FishToaster , była bezużyteczna dla wszystkiego, co nie było trywialne.

1. „ Jak przydatna jest dla Ciebie? ”

Zastosowanie sieci Petriego do programowania komputerów jest bardzo przydatne. Stworzyłem „Elementy sieciowe i adnotacje”, metodę opartą na sieciach Petriego (Chionglo, 2014). Stosuję tę metodę od 2014 r. Do pisania programów JavaScript, które używają interfejsu Acrobat / JavaScript API dla aplikacji formularzy PDF.

2. „Na czym polegało twoje szkolenie FM (np. Kurs, książka)? ”

„Trenowałem” w sieciach Petriego poprzez samokształcenie. Przeczytałem rozdziały na temat sieci Petriego z podręcznika „Sieci Petriego i Grafcet: narzędzia do modelowania systemów dyskretnych zdarzeń” (David i Alla, 1992). Czytałem także artykuły badawcze na temat sieci Petriego. Po utworzeniu i udokumentowaniu „Elementów sieciowych i adnotacji” ćwiczyłem stosowanie tej metody przez kilka tygodni.

3. „ Z jakich narzędzi FM korzystasz? ”

Rysuję schematy Petri Net za pomocą programu PowerPoint. Tworzę widok formularza adnotacji za pomocą programu Word. Gry tokena tworzę również jako aplikacje w formacie PDF, używając Acrobata i Notatnika. Po dodaniu wpisów do formularza tłumaczenie tych wpisów na kod JavaScript jest systematyczne. Dlatego powinna istnieć możliwość zautomatyzowania tłumaczenia. Jeśli „wpisy” zostały dodane do obiektów graficznych w programie PowerPoint, powinna istnieć możliwość systematycznego tłumaczenia ich na kod JavaScript oraz automatyzacji tego tłumaczenia. Korzystam również z zestawu narzędzi w toku, które wykonują te tłumaczenia i do tworzenia dodatkowych zasobów do tworzenia aplikacji formularzy PDF (Chionglo, 2018; 2017).

4. „ Jakie zalety ma szybkość / jakość w porównaniu z nieużywaniem FM? ”

Potrafię pisać programy JavaScript za pomocą „Elementów netto i adnotacji” szybciej niż mogę pisać program JavaScript bez użycia „Elementów netto i adnotacji”. W przypadku dużych programów mogę przestać kodować i powrócić do kodowania później (lub znacznie później), nie zastanawiając się, gdzie kontynuować (Chionglo, 2019). W niektórych przypadkach mogę pisać programy JavaScript za pomocą „elementów sieci i adnotacji”, ale nie mogę pisać programów JavaScript bez użycia „elementów netto i adnotacji”. Na przykład nie mogłem stworzyć nierekurencyjnych implementacji funkcji rekurencyjnych bez użycia „elementów sieciowych i adnotacji” (Chionglo, 2019b; 2018b; 2016). Są to prawdziwe z narzędziami w toku lub bez nich.

5. „ Jakie oprogramowanie tworzysz za pomocą FM? ”

Używam „elementów sieciowych i adnotacji” do tworzenia programów JavaScript, które używają interfejsu Acrobat / JavaScript API dla aplikacji formularzy PDF. Mogę również zastosować tę metodę do tworzenia programów JavaScript do dokumentów HTML i do tworzenia szkiców Arduino (Chionglo, 2019c; 2019d).

6. „ A jeśli nie używasz teraz FM bezpośrednio, to czy warto było się uczyć? ” Nie dotyczy.

Bibliografia

Chionglo, JF (2019b). Obliczanie n-tego terminu relacji rekurencyjnej: użycie funkcji nierekurencyjnej - odpowiedź na pytanie na giełdzie stosów matematycznych. < https://www.academia.edu/38496025/Computing_the_N-th_Term_of_a_Recursive_Relation_Using_a_Non-Recursive_Function_A_Reply_to_a_Question_at_Mathematics_Stack_Exchange >.

Chionglo, JF (2019c). Logika kontroli efektu płomienia, symulacja i szkic: odpowiedź na zapytanie na forum społeczności Arduino. https://www.academia.edu/40342956/Flame_Effect_Control_Logic_Simulation_and_Sketch_A_Reply_to_a_Request_at_the_Arduino_Community_Forum .

Chionglo, JF (2019). Jak kontynuować kodowanie aplikacji po długiej przerwie? Odpowiedz na „Skąd wiesz, gdzie zatrzymałeś się w swoich kodach po 2-tygodniowej przerwie?” - Software Engineering Stack Exchange. https://www.academia.edu/39705042/How_I_Continue_Coding_an_Application_after_a_Long_Break_Reply_to_How_do_you_know_where_you_stopped_in_your_codes_after_a_2-week_break_Software_Engineering .

Chionglo, JF (2019d). Pokaż i ukryj logikę sterowania: Zainspirowany pytaniem o przepełnienie stosu. < https://www.academia.edu/40283015/Show-and-Hide_Control_Logic_Inspired_by_a_Question_at_Stack_Overflow >.

Chionglo, JF (2018b). Model sieci Petriego dla silni liczby: i nierekurencyjna funkcja JavaScript do jej obliczenia. <>.

Chionglo, JF (2018). Utwórz Hyper Form ™ - proces w toku: aktualizacja badań programistycznych Net. https://www.academia.edu/37697498/Create_Hyper_Form_-A_Workflow_in_Progress_Update_on_the_Net_Programming_Research .

Chionglo, JF (2017). Programowanie w sieci: propozycja badawcza: do tworzenia aplikacji formularzy PDF w programach PowerPoint i Acrobat. https://www.academia.edu/33374809/Net_Programming_A_Research_Proposal_For_Developing_PDF_Form_Applications_with_PowerPoint_and_Acrobat..

Chionglo, JF (2016). Model sieci Petriego do obliczania liczby Fibonacciego.https://www.academia.edu/31748108/A_Petri_Net_Model_for_Computing_the_Fibonacci_Number.

Chionglo, JF (2014). Elementy sieciowe i adnotacje do programowania komputerowego: obliczenia i interakcje w formacie PDF. https://www.academia.edu/26906314/Net_Elements_and_Annotations_for_Computer_Programming_Computations_and_Interactions_in_PDF .

David, R. i H. Alla. (1992). Sieci Petriego i Grafcet: narzędzia do modelowania systemów dyskretnych zdarzeń. Upper Saddle, NJ: Prentice Hall.