Jak stworzyć oprogramowanie krytyczne dla misji?

15

Uczę się metod formalnych. Słyszałem, że do tworzenia oprogramowania o kluczowym znaczeniu (takiego jak kontroler reaktora jądrowego, kontroler lotu statku powietrznego, kontroler sondy kosmicznej) stosuje się (i zwykle stosuje się) metody formalne. Dlatego chcę się tego nauczyć: str

Jednak po zapoznaniu się z metodami formalnymi (zwłaszcza LTL, CTL i ich rodzeństwem) czuję, że można ich użyć tylko do weryfikacji poprawności specyfikacji (bezpieczeństwo, żywotność, uczciwość itp.).

Ale jak sprawdzić, czy oprogramowanie (nie tylko specyfikacja) jest rzeczywiście poprawne?

Zastrzeżenie: Jestem 90% idiotą, jeśli chodzi o informatykę teoretyczną. Prosimy więc o litość podczas odpowiadania.

fajrian
źródło
2
Co dokładnie masz na myśli mówiąc „... że oprogramowanie jest rzeczywiście poprawne ...” ? Które z poniższych 2 masz na myśli: 1) Oprogramowanie jest zgodne ze specyfikacją 2) Określone bloki kodu uwzględniają pewną daną właściwość lub pewną relację wejścia-wyjścia.
Giorgio Camerani,
@GiorgioCamerani: Pierwszy
fajrian
2
Poprawność programu zwykle oznacza, że ​​(1) jest zgodny ze specyfikacją i (2) nigdy nie ulega awarii. Punkt (1) to tak naprawdę stwierdzenie dotyczące pary (programu, specyfikacji), a nie samego programu. Kolejną komplikacją jest to, że „program” jest zwykle skrótem dla „modelu programu”, ponieważ same programy są raczej zbyt skomplikowane lub nie mają precyzyjnej semantyki. Biorąc to pod uwagę, myślę, że pytasz o lukę między programem a jego modelem, ale nie jestem do końca pewien.
Radu GRIGore,
@RaduGRIGore: Właściwie to nie rozumiem, czym jest „model”. Ale myślę, że podchodzisz do mojego pytania dość dokładnie. Zasadniczo zastanawiam się nad luką między specyfikacją a kodem źródłowym programu. Wiele głupich rzeczy może się zdarzyć, gdy programiści (tacy jak ja) implementują specyfikację.
fajrian
1
@fajrian: Podejrzewam, że mówisz „specyfikacja” dla tego, co nazwałbym „modelem”. Istnieją narzędzia, które działają na programach napisanych w językach takich jak C lub Java, a nawet w kodzie maszynowym. (Jest to jednak nadal model, ponieważ muszą oni przyjąć pewną semantykę, która powinna , ale nie musi , odpowiadać temu, co robi kompilator / procesor.)
Radu GRIGore 12.12 o

Odpowiedzi:

11

Pytanie jest dość ogólne. Aby odpowiedzieć na to pytanie w rozsądnej przestrzeni, dokonam wielu uproszczeń.

Uzgodnijmy terminologię. Program jest poprawny, jeśli sugeruje jego specyfikację. To niejasne stwierdzenie jest precyzyjne na wiele sposobów, poprzez określenie, czym dokładnie jest program, a co dokładnie specyfikacją. Na przykład podczas sprawdzania modelu program ma strukturę Kripke, a specyfikacja jest często formułą LTL . Lub, program może być listą instrukcji PowerPC, a specyfikacją może być zestaw twierdzeń Hoare-Floyda zapisanych, powiedzmy, w logice pierwszego rzędu. Istnieje bardzo wiele możliwych wariantów. Kuszące jest stwierdzenie, że w jednym przypadku (struktura Kripke) nie weryfikujemy rzeczywistego programu, podczas gdy w drugim przypadku (lista instrukcji PowerPC) to robimy. Jednak ważne jest, aby zdać sobie sprawę, że naprawdę przyglądamy się modelom matematycznym w obu przypadkach, i jest to całkowicie w porządku. (Sytuacja jest bardzo podobna do fizyki, gdzie na przykład mechanika klasyczna jest matematycznym modelem rzeczywistości).

Większość formalizacji rozróżnia składnię i semantykę programu; to znaczy, w jaki sposób jest reprezentowany i co to znaczy. Z punktu widzenia weryfikacji programu liczy się semantyka programu. Ale oczywiście ważne jest, aby mieć jasny sposób przypisywania znaczeń programom (składnie) programów. Dwa popularne sposoby to:

  • (mały krok) semantyka operacyjna : Jest to bardzo podobne do definiowania języka programowania przez napisanie dla niego tłumacza. W tym celu musisz powiedzieć, jaki jest stan , na który wpływa każde zdanie w języku. (Możesz się zastanawiać, w jakim języku piszesz tłumacza, ale udam, że nie.)
  • semantyka aksjomatyczna : tutaj każdy typ instrukcji ma schemat aksjomatyczny. Z grubsza, za każdym razem, gdy używane jest określone stwierdzenie tego typu, przekłada się to na możliwość używania pewnych aksjomatów. Na przykład przypisanie ma schemat { P [ x / e ] }x:=e ; dane przypisanie x : = x + 1 ma aksjomat { x + 1 = 1 }{P[x/e]}x:=e{P}x:=x+1 jeśli utworzymy instancję schematu za pomocą P = ( x = 1 ) .{x+1=1}x:=x+1{x=1}P=(x=1)

(Są inne. Szczególnie źle czuję się, gdy pomijam semantykę denotacyjną, ale ta odpowiedź jest już długa.) Kod maszynowy i semantyka operacyjna są bardzo zbliżone do tego, co większość ludzi nazwałaby „prawdziwym programem”. Oto kluczowy artykuł, który wykorzystuje semantykę operacyjną dla podzbioru kodu maszynowego DEC Alpha:

Dlaczego miałbyś kiedykolwiek używać semantyki wyższego poziomu, takiej jak aksjomatyczna? Gdy nie chcesz, aby Twój dowód poprawności był zależny od sprzętu, na którym działasz. Podejście polega zatem na udowodnieniu poprawności algorytmu w odniesieniu do pewnej wygodnej semantyki wysokiego poziomu, a następnie udowodnieniu, że semantyka brzmi w odniesieniu do semantyki niższego poziomu, które są bliższe rzeczywistym maszynom.

Podsumowując, mogę wymyślić trzy przyczyny, które doprowadziły do ​​twojego pytania:

  1. Widziałeś tylko semantykę wysokiego poziomu, która nie wygląda tak, jak zwykłaś nazywać program, i zastanawiasz się, czy są semantyki niskiego poziomu. Odpowiedź brzmi tak.
  2. Zastanawiasz się, jak udowodnić, że model odpowiada rzeczywistości. Podobnie jak w fizyce, nie. Po prostu wymyślasz lepsze modele i porównujesz je z rzeczywistością.
  3. Nie widziałeś rozróżnienia między składnią i semantyką oraz różnymi sposobami przypisywania znaczenia programom. Dwa poprzednie pytania wymieniają niektóre książki.

Ta odpowiedź próbuje jedynie zidentyfikować trzy różne sposoby, w jakie zrozumiałem pytanie. Wchodzenie głęboko w którykolwiek z tych punktów wymagałoby dużo miejsca.

Radu GRIGore
źródło
8

Jednym ze sposobów zmniejszenia luki między programem a jego specyfikacją jest użycie języka z formalną semantyką. Ciekawym przykładem byłaby tutaj Esterel . Zajrzyj na stronę internetową Gérarda Berry'ego, gdzie znajdziesz ciekawe rozmowy na temat jego pracy nad wprowadzeniem metod formalnych do realnego świata. http://www-sop.inria.fr/members/Gerard.Berry/

ps Byłeś na Airbusie? Leciałeś metodami formalnymi!

Ross Duncan
źródło
1
pomocny byłby każdy przegląd sposobu, w jaki Airbus stosuje metody formalne. (rozumiem, że jest to możliwe zastrzeżona informacja)
wzn
@RossDuncan Znalazłem tę stronę po przejściu na stronę Berry i kilku wyszukiwaniach. Czy to są formalne metody, o których mówił Airbus?
scaaahu
Nie mam żadnych informacji wewnętrznych dotyczących korzystania z Esterel przez Airbusa; mój komentarz po prostu powtarza uwagę, którą Berry wypowiedział podczas wykładu. Ta strona stanowi jednak sukces w korzystaniu z produktu SCADE z Airbusem. Jeśli spojrzysz na historię Esterel, Dassault przyjęła ją dość wcześnie. Google to twój przyjaciel.
Ross Duncan
2
Airbus korzysta również z astree.ens.fr
Radu GRIGore,
7

Nauka budowy niezawodnego oprogramowania w „prawdziwym świecie” jest wciąż rozwijana i do pewnego stopnia opiera się na badaniach z natury kulturowych lub antropologicznych, ponieważ komputery i oprogramowanie nie „powodują” błędów - ludzie tak robią! odpowiedź ta skupi się na ogólnych podejściach do pytań / odpowiedzi, których formalną weryfikację oprogramowania można postrzegać jako jeden element.

niezwykłą spostrzeżeniem jest to, że często oprogramowanie, które jest „wystarczająco dobre”, ale „błędne”, często może wyprzedać lepiej przetestowane, ale o niższej funkcjonalności oprogramowanie na rynku. innymi słowy, rynek nie zawsze kładzie nacisk na jakość oprogramowania i nowoczesne techniki inżynierii oprogramowania, które nie zawsze kładą nacisk na jakość, nieco to odzwierciedlają. ponadto jakość może często stanowić znaczny wydatek na produkt końcowy. z tymi zastrzeżeniami, oto niektóre z podstaw:

  • systemy redundantne / odporne na uszkodzenia. jest to szeroki obszar badań. tolerancję i redundancję błędów można zaprojektować w wielu warstwach systemu. np. router, serwer, napęd dyskowy itp.

  • testowanie . wszystkie typy - testy jednostkowe, testy integracyjne, testy akceptacyjne użytkownika, testy regresyjne itp.

  • obecnie zautomatyzowane testowanie za pomocą pakietów testowych, które można uruchamiać bez nadzoru, jest bardziej rozbudowane / ważne. działające zestawy testowe są często połączone z narzędziem do budowania.

  • ważną koncepcją w testowaniu jest pokrycie kodu . tj. jaki kod jest wykonywany przez test. test nie może znaleźć błędu w kodzie, który nie jest „dotknięty” przez test.

  • Inną kluczową koncepcją w testach jest testowanie tego kodu ćwiczeń, do którego dostęp nie jest łatwy.

  • testy powinny wykonywać wszystkie poziomy oprogramowania. jeśli oprogramowanie jest dobrze zmodularyzowane, nie jest to trudne. testy wyższego poziomu powinny wnikać głęboko w kod. testy wykorzystujące duże ilości kodu przy małej konfiguracji testu zwiększają „dźwignię testową” .

  • Sprawienie, by kod był jak najmniej skomplikowany, jest możliwe do testowania. testy powinny być brane pod uwagę przy projektowaniu architektury. często istnieje wiele sposobów implementacji tej samej funkcji, ale niektóre mają wiele różnych implikacji dla zasięgu testowania / dźwigni. dla każdej gałęzi kodu jest to często kolejny przypadek testowy. gałęzie w gałęziach rosną do wykładniczego wzrostu ścieżek kodu. dlatego unikanie mocno zagnieżdżonej / warunkowej logiki poprawia zdolność do testowania.

  • badanie słynnych (ogromnych) awarii oprogramowania, których jest wiele przykładów, a studia przypadków są pomocne w zrozumieniu historii i rozwijaniu sposobu myślenia ukierunkowanego na względy jakościowe.

  • można dać się ponieść testom! istnieje zarówno problem ze zbyt małym, jak i zbyt dużym testowaniem. jest „słodkie miejsce”. oprogramowania nie można z powodzeniem wbudować ani w ekstremalne.

  • korzystaj ze wszystkich podstawowych narzędzi w najbardziej efektywny sposób. debuggery, profilery kodu, narzędzia pokrycia kodu testowego, system śledzenia defektów itp! niekoniecznie zobowiązują się do naprawy, ale śledzą nawet najmniejsze wady oprogramowania śledzącego.

  • staranne stosowanie SCM, zarządzanie kodem źródłowym i techniki rozgałęziania jest ważne w celu uniknięcia regresji, izolowania i postępu poprawek itp.

  • Programowanie w wersji N : praktyka często używana do tworzenia oprogramowania o znaczeniu krytycznym. Założeniem tej praktyki jest to, że N niezależnie opracowanych programów raczej nie ma tego samego wspólnego błędu / usterki. Zostało to skrytykowane w kilku artykułach . NVP jest jednak praktyką, a nie koncepcją teoretyczną.

Wierzę, że fizyk Feynman ma w swojej książce „Metodę NASA w celu zagwarantowania niezawodności systemów wahadłowców”. Co cię obchodzi, co myślą inni? - powiedział, że mają dwie drużyny, powiedzmy, że zespół A i zespół B. zbudowali oprogramowanie. drużyna B przyjęła przeciwne podejście do Drużyny A i próbowała złamać oprogramowanie.

pomaga to, jeśli Zespół B ma dobre przygotowanie inżynieryjne, tzn. że sami mogą pisać wiązkę kodu / testy programowe itp. w takim przypadku Zespół B miał prawie taki sam poziom zasobów jak Zespół A. Z drugiej strony takie podejście jest drogie, ponieważ może prawie podwoić koszty budowy oprogramowania. częściej jest to mniejszy zespół ds. kontroli jakości w porównaniu do zespołu programistów.

vzn
źródło
8
Ktoś powinien sprawdzić poprawność systemu operacyjnego w odniesieniu do specyfikacji, że naciśnięcie klawisza Shift i litery powoduje utworzenie dużej litery.
Andrej Bauer,
1
uzupełnienie: ograniczenia harmonogramu mogą wpływać na jakość. patrz także trójkąt projektu mgt złożony z zakresu, kosztów, harmonogramu z jakością „obszaru”, na który wpływ mają wszyscy 3. zobacz także „Dlaczego branża IT nie może dostarczyć dużych, bezbłędnych projektów tak szybko, jak w innych branżach?” . sam nie dodałem elementu w wersji N [jego inna odpowiedź], ale zauważ, że Feynman wspomniał, że NASA użyła go również w projekcie promu kosmicznego.
vzn
1
Innym interesującym studium przypadku jest łazik marsjański, który ma duże ilości kodu, z których większość jest generowana automatycznie. w takim przypadku poprzednie łaziki przetestowały większość oprogramowania i zostało ponownie wykorzystane.
vzn
6

Stare podejście (ale nadal jest używane w niektórych aplikacjach) to programowanie w wersji N.

Z Wikipedii:

Programowanie w wersji N ( NVP ), znane również jako programowanie w wielu wersjach , jest metodą lub procesem inżynierii oprogramowania, w którym wiele funkcjonalnie równoważnych programów jest generowanych niezależnie na podstawie tych samych specyfikacji początkowych. Koncepcja programowania w wersji N została wprowadzona w 1977 r. Przez Liming Chen i Algirdasa Avizienisa z centralnym przypuszczeniem, że „niezależność wysiłków programistycznych znacznie zmniejszy prawdopodobieństwo wystąpienia identycznych błędów oprogramowania w dwóch lub więcej wersjach programu”. Cel NVP ma na celu poprawę niezawodności działania oprogramowania poprzez budowanie tolerancji na błędy lub redundancji.

Zobacz na przykład: „ Wyzwania w usterce budynku - tolerancyjny system sterowania lotem dla samolotu cywilnego

Marzio De Biasi
źródło
Warto zauważyć, że programowanie w wersji n nie działa . Podstawowe założenie - mianowicie, że błędy w powtarzanych próbach procesu tworzenia oprogramowania są niezależne - jest całkowicie fałszywe . Pomysł ten nie ma teoretycznego sensu (trudny do wdrożenia algorytm nie stanie się magicznie łatwiejszy dla drugiego niezależnego zespołu) i został również obalony eksperymentalnie: eksperyment Johna Knighta i Nancy Leveson wykazujący, że założenie niezależności nie jest statystycznie uzasadnione jest jednym z najbardziej znanych artykułów z dziedziny inżynierii oprogramowania.
Neel Krishnaswami
@NeelKrishnaswami: Zgadzam się! Jednak myślę (ale nie jestem ekspertem), że nie działa, należy go zastąpić , nie poprawia niezawodności tak bardzo, jak powinno, w porównaniu z innymi podejściami . Powołując się na K&L: „ ... Nigdy nie sugerowaliśmy, że nasz wynik powinien być wykorzystany jako podstawa do podjęcia decyzji o skuteczności programowania w wersji N. Po prostu zasugerowaliśmy, że ostrożność byłaby właściwa ... ”. Myślę, że debata na temat tego, jak bardzo podejście NVP może być przydatne do krytycznego projektowania systemu, jest wciąż otwarta (patrz ostatnia praca Khoury i wsp.)
Marzio De Biasi,
4

fajrian, to pytanie, które postawiłeś, obejmuje dwa największe problemy w badaniach inżyniera oprogramowania: zgodność specyfikacji ze modelem oraz między modelem a kodem. Modeluj tutaj reprezentację tego, co zrobi system lub jak to będzie zrobione, istnieje wiele poziomów do modelowania systemu.

Są ludzie, którzy próbują znaleźć najlepszą odpowiedź na twoje pytanie. Ponieważ bardzo trudno jest sprawdzić poprawność oprogramowania opartego na modelu, na przykład przy użyciu metod formalnych. Znam JML jest na to sposobem, ale nie znam granic jego używania.

Podsumowując, jak trudno jest sprawdzić poprawność kodu, ludzie próbują łączyć metody formalne i testować, tworząc testy automatycznie na przykład ze specyfikacji. Jednym z przykładów systemów czasu rzeczywistego jest TIOSTS oparty na zdarzeniach czasowych wejścia / wyjścia.

Tylko testowanie nie jest formalnym podejściem metodycznym, ponieważ poprawia niezawodność, ale nie sprawdza poprawności.


źródło
3

Dwa lub trzy lata temu zacząłem przyglądać się formalnym metodom stosowanym w oprogramowaniu. Było to zadanie napędzane ciekawością i poczuciem, że musiałem nauczyć się narzędzi i metod programowania z dłuższymi okresami. Chociaż marzyłem życzliwie o Srebrnej Kuli , naprawdę myślałem, że nie ma odpowiedzi na pytanie: „Jak napisać poprawny program?”.

W tym momencie wyprawy po wypróbowaniu niektórych narzędzi (Z, B, VHDL i Estelle) używam TLA + . Jest to wariant logiki czasowej z narzędziami programowymi do sprawdzania modelu i prób mechanicznych. Myślę, że wybrałem to podejście, ponieważ L. Lamport był za tym, składnia była prosta, było wiele przykładów, istniała społeczność, a język i narzędzia były dość dobrze udokumentowane.

Jeśli chodzi o moje pierwsze pytanie, myślę, że nie ma pełnej odpowiedzi. Warto jednak nauczyć się, że opłaca się formalnie określać niektóre części systemu. Przydaje się również inżynieria wsteczna niektórych złożonych. Oznacza to, że skuteczne jest stworzenie planu dla trudnych i krytycznych części. Nie sądzę jednak, aby istniała skuteczna metoda automatycznego tłumaczenia specyfikacji na język programowania lub środowisko programistyczne (chyba że ograniczysz projekt do bardzo specyficznego środowiska). Nie uważam też, że posiadanie formalnej specyfikacji powinno uniemożliwić testowanie oprogramowania.

W skrócie, myślę, że następująca metafora (z Lamport) jest naprawdę potężna: „Czy spodziewasz się, że dom zostanie automatycznie zbudowany na podstawie planu? Czy kupisz dom, który nie został jeszcze zbudowany i nie ma planu?” .

Podczas tego zadania znalazłem przydatne zasoby:

  • Metody specyfikacji oprogramowania . Ta książka zawiera szeroki przegląd istniejących metod i narzędzi. Można tam znaleźć podstawowe wyjaśnienia i przykłady Z, SDL, TLA +, sieci Petriego, Coq itp.
  • Jeśli uważasz, że TLA + odpowiada Twoim potrzebom, naprawdę polecam książkę Specifying Systems . Możesz dostać książkę za darmo, a ona zawiera przykłady do zabawy :).
  • Niedawno przeczytałem kilka powiązanych artykułów, które przedstawiają dwie różne perspektywy najnowocześniejszych metod formalnych: przypadek metod formalnych i matematyka formalnie zweryfikowana .

Powodzenia!

marcmagransdeabril
źródło
1

Dotychczasowe odpowiedzi obejmowały już większość tego, co należy powiedzieć o podstawach wzajemnego powiązania specyfikacji i kodu. Chcę tylko dodać bardziej praktyczny punkt, który zbliża się do pytania w nagłówku tego wątku:

Jak stworzyć oprogramowanie o znaczeniu krytycznym?

Istnieją narzędzia, które automatycznie analizują kod pod kątem błędów (naruszenia specyfikacji lub „typowe błędy”). Według mojej wiedzy metody te opierają się głównie na analizie statycznej i nie są bezpośrednio związane z teoriami, o których wspominałeś (LTL / CTL / ...), ale znajdują błędy w prawdziwym kodzie i jest to już wykonalne, z praktycznego punktu widzenia zobacz, aby korzystać z takich narzędzi w projektach przemysłowych. Osobiście nie korzystałem z wielu z nich, ale wydaje się, że narzędzia te zaczynają być akceptowane przez praktyków. Do dalszego czytania mogę polecić następujący artykuł na blogu:

http://www.altdevblogaday.com/2011/12/24/static-code-analysis/

Markus
źródło
przykładowa implementacja z java, open source apache
findbugs
0

Algorytmy certyfikujące mogą być przydatne podczas tworzenia oprogramowania o znaczeniu krytycznym.

Algorytm certyfikujący to algorytm, który przy każdym wyjściu wytwarza certyfikat lub świadek (łatwy do zweryfikowania dowód), że błąd nie wpłynął na dane wyjście.

Przeczytaj więcej w tym artykule ankietowym Algorytmy certyfikujące McConnell, RM i Mehlhorn, K. i Naher, S. i Schweitzer, P.

Pratik Deoghare
źródło
W 1998 r. Pnueli, Siegel i Singerman opisali tę ideę w odniesieniu do kompilatorów pod nazwą weryfikacji tłumaczenia. Kompilatory są z natury wyższego rzędu (dane wejściowe to program, dane wyjściowe to program), więc trudno jest je zweryfikować. Ale są szaleni ludzie tacy jak X. Leroy, którzy i tak opracowują sprawdzone kompilatory. (Szalony w najlepszym możliwym sensie!)
Radu GRIGore
-2

Ale jak sprawdzić, czy oprogramowanie (nie tylko specyfikacja) jest rzeczywiście poprawne?

Testów jednostkowych? Napisz test dla każdego wymagania w specyfikacji, a następnie przetestuj każdą metodę w swojej implementacji, aby sprawdzić, czy dane wyjściowe / wejściowe są zgodne z tą specyfikacją. Można to zautomatyzować, aby testy były przeprowadzane w sposób ciągły, aby żadna zmiana nigdy nie uszkodziła wcześniej działających funkcji.

Teoretycznie, jeśli testy jednostkowe obejmują 100% pokrycia kodu (tj. Testowana jest każda metoda w kodzie), oprogramowanie powinno być poprawne, pod warunkiem, że same testy są dokładne i realistyczne.

gillesv
źródło
5
W przypadku każdego dość złożonego programu pokrycie kodu (przez testowanie) nie może zapewnić poprawności. Będziesz musiał pokryć wszystkie możliwe egzekucje; wszystkie wiersze kodu to za mało.
Radu GRIGore
1
Pojęcie kodu jest zbyt niejasne. Rozróżniamy między innymi, np. Pokrycie metod, pokrycie wyciągów, pokrycie oddziałów, pokrycie ścieżek itp. Jak zauważa Radu, w przypadku nietrywialnych programów testowanie często prowadzi do wybuchów kombinatorycznych. To powiedziawszy, oprogramowanie aeronautyczne ma dość długą historię, a jego poprawność często opiera się na rozległych testach.
Martin Berger,
Jeśli masz na myśli testowanie za pomocą narzędzi takich jak JUnit, ten rodzaj standardowych testów automatycznych nie może obejmować wszystkich przypadków (chyba że program jest bardzo mały). W typowych zastosowaniach tego rodzaju testy zwykle wystarczają. Ale w przypadku aplikacji o znaczeniu krytycznym nie wiem, czy to wystarczy (czy nie).
fajrian
2
@vzn: Z mojego doświadczenia wynika, że ​​pomiędzy naukowcami a odpowiednio praktykami istnieje niezwykła zgodność. Założę się również, że większość moich (byłych) kolegów z branży zgodziłaby się, że „każda metoda w twoim kodzie jest testowana” nie brzmi zbyt uspokajająco. (I nie, nie przegłosowałem. Prawie nigdy.)
Radu GRIGore
1
@vzn: Czy powiedziałem, że powiedziałeś inaczej? Próbowałem po prostu wyjaśnić, dlaczego uważam, że inni nie popierają tej odpowiedzi. W tej chwili nie mogę odpowiedzieć na to pytanie, ponieważ go nie rozumiem.
Radu GRIGore,