AK <n...@n...com> wrote:
> 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++:)

No, np. w Adzie typowe wymaganie w takich sytemach to brak
wyjatkow. I problem wraca.

> > 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).

Wez sobie przeczytaj:

https://sel4.systems/FAQ/proof.pml

Nie ma co dyskutowac dlaczego tworcy L4 wybrali C. ZTCW to jest
pierwszy przyklad w jakimkolwiek jezyku gdzie udalo sie pokazac
tak wiele. Zalozenie ze Ada jest lepsza do weryfikacji jest
naturalne. Ale narzedzia do Ady (SPARK) na razie daja mniej.

--
Waldek Hebisch
h...@m...uni.wroc.pl