Użytkownik "Waldek Hebisch" <h...@m...uni.wroc.pl> napisał:

>> Nie wierze. C nie nadaje sie do weryfikacji formalnej poprawnosci programow
>> w nim pisanych (chyba ze jest to baaardzo okrojone C - i to o wiele bardziej niz
Misra C),
>> a jadro to jaderko na przyslowiowych "kilku kartkach" i "specjalnie pisane" pod
werfyfikacj?.
>>
>> W zwyklym C/C++ formalna weryfikacja pooprawnosci to zwykla
>> uluda (i taka na zawsze zostanie).
>>
>
> Mikrojado L4 ma kolo 8000 lini kodu.

No to naprawde... Potega !
PS: "My ze szwagrem" zweryfikujemy takie cus w miesiac za 34PLN/h :)

> ZCW weryfikacja obemuje np. sprawdzenie ze nie ma przepelnien buforow.

a wystarczylo uzyc jezyka w ktorym np. przepelnienie buforow nie wystepuje/
nie grozi kolapsem (ehh ta "wysokopoziomowosc" C /C++:)

> Co do C to jest rozpracowana odpowiednia logika i ponoc teraz
> nie sprawia wiecej problemow niz inne jezyki.

Jaasne. Wystaczy po prostu zrezygnowac z pointerow :)

PS: Nie moge "wyjsc z podziwu" dlaczego do napisania tak malych przeciez rzeczy
jak to mikrojadro nie uzyc chocby Ady , ktora z zalozenia o niebo lepiej
nadaje sie do weryfikacji poprawnosci formalnej programow.
Z C/C++ to najpierw stwarza sie problemy (poprzez samo jego uzycie) a pozniej
bohatersko i wielkim nakladem sil sie rozwiazuje (typowe slodzienie herbaty
przez mieszanie w lewo). Poza tym o ile jeszzce pamietam to glowna materia
formalnej weryfikacji poprawnosci priogramow to nie wylapywanie jakiegos
przepelnienia bufora, ale sprawdzanie zgodnosci "flow" kodu programu
z "flow" projektu (badanie zgodnosci kodu z zalozeniami logicznymi).

AK


---
Ta wiadomość została sprawdzona na obecność wirusów przez oprogramowanie antywirusowe
Avast.
https://www.avast.com/antivirus