Re: [OT] Du?a kasa i kiepski wynik - dlaczego? - Grupy dyskusyjne w eGospodarka.pl

eGospodarka.pl › Grupy › pl.comp.programming › [OT] Duża kasa i kiepski wynik - dlaczego? › Re: [OT] Du?a kasa i kiepski wynik - dlaczego?

Path: news-archive.icm.edu.pl!news.icm.edu.pl!newsfeed.pionier.net.pl!pwr.wroc.pl!new
s.wcss.wroc.pl!not-for-mail
From: Waldek Hebisch <h...@m...uni.wroc.pl>
Newsgroups: pl.comp.programming
Subject: Re: [OT] Du?a kasa i kiepski wynik - dlaczego?
Date: Mon, 14 Sep 2015 19:51:28 +0000 (UTC)
Organization: Politechnika Wroclawska
Lines: 51
Message-ID: <mt78g0$1fd$1@z-news.wcss.wroc.pl>
References: <mosvh7$bpl$1@node1.news.atman.pl> <msvaa3$15k$1@node1.news.atman.pl>
<mt10d4$v8$1@node2.news.atman.pl> <mt16oq$t5c$1@node1.news.atman.pl>
<mt1b2u$bf8$1@node2.news.atman.pl> <mt1et9$5tj$2@node1.news.atman.pl>
<mt1j7s$ado$1@node1.news.atman.pl> <mt1oci$oob$1@node2.news.atman.pl>
<mt2euk$joa$1@z-news.wcss.wroc.pl> <mt3oub$j8r$1@node1.news.atman.pl>
<mt4huo$491$1@z-news.wcss.wroc.pl> <mt4kh4$hp0$1@node1.news.atman.pl>
<mt55pc$h4g$1@z-news.wcss.wroc.pl> <mt6121$11g$1@node2.news.atman.pl>
NNTP-Posting-Host: math.uni.wroc.pl
X-Trace: z-news.wcss.wroc.pl 1442260288 1517 156.17.86.1 (14 Sep 2015 19:51:28 GMT)
X-Complaints-To: a...@n...pwr.wroc.pl
NNTP-Posting-Date: Mon, 14 Sep 2015 19:51:28 +0000 (UTC)
Cancel-Lock: sha1:GZnSzHY7fV0BK8VPtovRxLXkXa0=
User-Agent: tin/2.2.1-20140504 ("Tober an Righ") (UNIX) (Linux/4.1.3 (x86_64))
Xref: news-archive.icm.edu.pl pl.comp.programming:208288
[ ukryj nagłówki ]
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