Qmail +relaying

[Michal Moskal]

On Fri, Mar 29, 2002 at 06:02:58PM +0100, Tomasz Kłoczko wrote:
> > > [..]
> > > > jedyna znana mi "_obiektywna_ analiza" byla analiza matematyczna ktora to
> > > > zameczalem z wzajemnoscia w ramach studiow ...khhhmm... lat temu. Te analize
> > > > bede robil calkowicie subiektywnie z perspektywy wlasnego pepka :))
> > >
> > > I potrafisz udowodnić poprawność programu który ma więcej niż paręnaście 
> > > linijek ? Zaiste .. godne podziwu i zastanowienia :)
> > 
> > yyuups??? - to nawet nie wiedzialem, ze analiza matematyczna zajmuje sie rowniez
> > dowodzeniem poprawnosci programow komputerowych
> 
> To widać że jeszcze mało wiesz :>
> 
> > - z tego co pamietam w wielkim uogolnieniu analiza matematyczna zajmuje
> > sie badaniem funkcji, a obiektywna jest w tym sensie ze tam kazda rzecz
> > o ktorej sie mowi jest dowodzona, a nie szacowana.
> 
> Proponuję cofnąć się do prac Neumana i wcześniejszych czyli tak mniej
> więcej z przed pół wieku.

1. dowodzenie poprawności algorytmów jest nierozstrzygalne
2. gdy dowód da się przeprowadzić, ma on rozmiar wykładniczy w stosunku
   do rozmiaru algorytmu
3. widziałeś gdzieś formalny opis semantyki (np. operacyjnej) C?
   a może C++ (co byłoby podwójnie ciekawe, ze względu, na wewnętrzną
   sprzeczność tego języka). Jeśli tak to proszę o URL, jeśli to nie to
   względem czego te dowody?
4. ale co TY możesz o tym wiedzieć, skoro twierdzisz, że analiza
   matemtyczna zajmuje się dowodami poprawności algorytmów...

-- 
: Michal Moskal :::::::: malekith/at/pld.org.pl :  GCS {C,UL}++++$ a? !tv
: PLD Linux ::::::: Wroclaw University, CS Dept :  {E-,w}-- {b++,e}>+++ h