Mam pytanie:
Jak się weryfikuje poprawność programu? Znam: testowanie, dowodzenie
poprawności. Jak jeszcze?

--
Wysłano z serwisu OnetNiusy: http://niusy.onet.pl

do góry

On 6 Sie, 07:43, j...@p...onet.pl wrote:

> Jak się weryfikuje poprawność programu? Znam: testowanie, dowodzenie
> poprawności. Jak jeszcze?

Jest bardzo wiele metod:
- hobbyści: przez przypatrzenie
- studenci: przez zaliczenie
- firmy komercyjne: przez dochód
- ...

Zależy, co komu potrzebne. ;-)

--
Maciej Sobczak * http://www.inspirel.com

do góry

On 08/06/2010 07:43 AM, j...@p...onet.pl wrote:
> Mam pytanie:
> Jak się weryfikuje poprawność programu? Znam: testowanie, dowodzenie
> poprawności. Jak jeszcze?
>
http://scholar.google.com/scholar?hl=en&q=+proving+p
rogram+correctness&btnG=Search&as_sdt=2000&as_ylo=&a
s_vis=0

do góry

> dowodzenie poprawności

Czy którykolwiek z zaglądających na tą grupę programistów-praktyków dowodził w
pracy poprawność swojego programu?
Uczono mnie logiki Hoare'a. Czy takie akademickie rozważania bywają stosowane w
praktyce?

--
Wysłano z serwisu OnetNiusy: http://niusy.onet.pl

do góry

> Uczono mnie logiki Hoare'a. Czy takie akademickie rozważania bywają stosowane w
> praktyce?

Pytam, bo zdaję sobie sprawę, że dowodzenie poprawności nawet prostego programu,
np. algorytmu sortowania, jest żmudne.

--
Wysłano z serwisu OnetNiusy: http://niusy.onet.pl

do góry

Czy jest tu jakiś poważny człowiek, który mógłby mi odpowiedzieć na moje pytanie?

--
Wysłano z serwisu OnetNiusy: http://niusy.onet.pl

do góry

On 10 Sie, 20:46, j...@p...onet.pl wrote:

> Czy jest tu jakiś poważny człowiek, który mógłby mi odpowiedzieć na moje pytanie?

Formalnie nie używam.
Intuicyjnie średnio 12 godzin dziennie od 15 lat.
Z poważaniem :)

do góry

j...@p...onet.pl pisze:
>> Uczono mnie logiki Hoare'a. Czy takie akademickie rozważania bywają stosowane w
>> praktyce?
>
A do czego Ci to potrzebne? Poza tym dobrze zrobione testy są
wystarczające. Czegoś trudniejszego od "hallo world" nie jesteś w stanie
dowieść.


> Pytam, bo zdaję sobie sprawę, że dowodzenie poprawności nawet prostego programu,
> np. algorytmu sortowania, jest żmudne.
>
Ktoś na którejś grupie już poruszał kwestię - opracowano algorytm,
dowiedziono poprawności po czym okazało się, że algorytm się sypie bo
rzeczywisty komputer ma skończony zbiór wartości reprezentowanych w int.

--
Pozdrawiam
Michoo

do góry

On 10 Sie, 21:17, Michoo <m...@v...pl> wrote:

> Ktoś na którejś grupie już poruszał kwestię - opracowano algorytm,
> dowiedziono poprawności po czym okazało się, że algorytm się sypie bo
> rzeczywisty komputer ma skończony zbiór wartości reprezentowanych w int.

W takim razie źle dowiedziono jego poprawności.

Dowodzenie poprawności czegokolwiek powinno się odbywać a) na kodzie
źródłowym (a nie na obrazkach) i b) z uwzględnieniem typów docelowych.
Wtedy nie ma problemów jak powyżej.
Przykładowo, SPARK robi to całkiem sprawnie.

Nie odrzucałbym metod formalnych tylko dlatego, że ktoś kiedyś ich źle
użył.

--
Maciej Sobczak * http://www.inspirel.com

do góry

On 10 Sie, 20:46, j...@p...onet.pl wrote:
> Czy jest tu jakiś poważny człowiek, który mógłby mi odpowiedzieć na moje pytanie?

Poważnie to testy nie służą weryfikowaniu czegokolwiek, tylko
poprawianiu sobie samopoczucia. Zostają metody formalne.
Problem w tym, że w mainstreamowych językach programowania te metody
nie działają a przecież nikt nie będzie używał języków niszowych - i
stąd przepaść pomiędzy teorią a praktyką.

W praktyce jest to, co napisałem wcześniej - to wcale nie była
niepoważna odpowiedź. :-)

A tak konkretnie - co w ogóle chcesz udowodnić?

--
Maciej Sobczak * http://www.inspirel.com

do góry