Uczyli mnie na studiach dowodzenia poprawności algorytmów w logice Hoare'a. Jednak
poprawności trudniejszych algorytmów człowiem nie dowiedzie, a automatyzacja jest
niemożliwa, bo nie da się zautomatyzować generowania niezmienników. Testowanie
dowiedzie występowania błędów, ale nie dowiedzie że ich nie ma. Zaprogramowałem
pewien algorytm w PHP5+MySQL i nie jestem pewien czy jest poprawny. Czy są jeszcze
jakieś metody weryfikacji poprawności algorytmów poza dowodzeniem i testowaniem?

do góry

On Monday, March 23, 2015 at 3:12:25 PM UTC+1, j...@p...onet.pl wrote:
> Uczyli mnie na studiach dowodzenia poprawności algorytmów w logice Hoare'a. Jednak
poprawności trudniejszych algorytmów człowiem nie dowiedzie, a automatyzacja jest
niemożliwa, bo nie da się zautomatyzować generowania niezmienników. Testowanie
dowiedzie występowania błędów, ale nie dowiedzie że ich nie ma. Zaprogramowałem
pewien algorytm w PHP5+MySQL i nie jestem pewien czy jest poprawny. Czy są jeszcze
jakieś metody weryfikacji poprawności algorytmów poza dowodzeniem i testowaniem?

A ręczne wpisywanie niezmienników?
Pozdrawiam

do góry

> A ręczne wpisywanie niezmienników?

Sugerujesz że są programy które po podaniu specyfikacji wejścia i wyników oraz
podaniu niemienników dowodzą automatycznie poprawności?

do góry

> Czy są jeszcze jakieś metody weryfikacji poprawności algorytmów poza dowodzeniem i
testowaniem?

Przegląd kodu przez innego programistę w moim przypadku nie wchodzi w grę, bo mój
zleceniodawca by się nie zgodził. Program muszę pisać sam.

do góry

W dniu poniedziałek, 23 marca 2015 16:15:58 UTC+1 użytkownik j...@p...onet.pl
napisał:
> > A ręczne wpisywanie niezmienników?
>
> Sugerujesz że są programy które po podaniu specyfikacji wejścia i wyników oraz
podaniu niemienników dowodzą automatycznie poprawności?

Są.

Problemem (największym) pozostaje ręczne pisanie niezmienników z zachowaniem
ciągłości logicznej pomiędzy wszystkimi elementami tak, aby automat dowodzący tej
ciągłości nie zgubił - a to będzie zależało od samego automatu.

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

do góry

On Monday, March 23, 2015 at 5:30:32 PM UTC+1, Maciej Sobczak wrote:
> W dniu poniedziałek, 23 marca 2015 16:15:58 UTC+1 użytkownik
j...@p...onet.pl napisał:
> > > A ręczne wpisywanie niezmienników?
> >
> > Sugerujesz że są programy które po podaniu specyfikacji wejścia i wyników oraz
podaniu niemienników dowodzą automatycznie poprawności?
Nie wiem jak to zabrzmialo, ale nic takiego nie zamierzałem sugerować.
Po prostu ręczne nafaszerowanie programu asercjami, to pomocna metoda
w usuwaniu błędów.

>
> Są.
>
> Problemem (największym) pozostaje ręczne pisanie niezmienników z zachowaniem
ciągłości logicznej pomiędzy wszystkimi elementami tak, aby automat dowodzący tej
ciągłości nie zgubił - a to będzie zależało od samego automatu.
>
Mógłbym rzucić okiem na jakieś przykłady?
Pozdrawiam

do góry

W dniu poniedziałek, 23 marca 2015 15:12:25 UTC+1 użytkownik j...@p...onet.pl
napisał:
> Uczyli mnie na studiach dowodzenia poprawności algorytmów w logice Hoare'a. Jednak
poprawności trudniejszych algorytmów człowiem nie dowiedzie, a automatyzacja jest
niemożliwa, bo nie da się zautomatyzować generowania niezmienników. Testowanie
dowiedzie występowania błędów, ale nie dowiedzie że ich nie ma. Zaprogramowałem
pewien algorytm w PHP5+MySQL i nie jestem pewien czy jest poprawny. Czy są jeszcze
jakieś metody weryfikacji poprawności algorytmów poza dowodzeniem i testowaniem?

PHP nie jest pod tym wzgledem najbardziej fortunnym systemem, ale mozesz
sobie recznie wypisac sygnatury typow dla zmiennych i funkcji i sprawdzic,
czy program jest prawidlowo napisany na poziomie typow.

Wydaje mi sie tez, ze w tej sytuacji najkorzystniej byloby po prostu
napisac sprytne testy obejmujace wszystkie warunki brzegowe, a jesli masz
taka mozliwosc, to rowniez wygenerowac dostatecznie duze losowe dane testowe
i sprawdzic, czy program zachowuje sie prawidlowo

do góry

W dniu poniedziałek, 23 marca 2015 21:41:10 UTC+1 użytkownik M.M. napisał:

> > Są.
> >
> > Problemem (największym) pozostaje ręczne pisanie niezmienników z zachowaniem
ciągłości logicznej pomiędzy wszystkimi elementami tak, aby automat dowodzący tej
ciągłości nie zgubił - a to będzie zależało od samego automatu.
> >
> Mógłbym rzucić okiem na jakieś przykłady?

Tutaj:

http://docs.adacore.com/spark2014-docs/html/ug/

a konkretnie tutaj:

http://docs.adacore.com/spark2014-docs/html/ug/gnatp
rove.html

a konkretnie szukaj słów "Loop_Invariant".

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

do góry

On 23/03/2015 16:17, j...@p...onet.pl wrote:
>> Czy są jeszcze jakieś metody weryfikacji poprawności algorytmów
>> poza dowodzeniem i testowaniem?
>
> Przegląd kodu przez innego programistę w moim przypadku nie wchodzi w
> grę, bo mój zleceniodawca by się nie zgodził. Program muszę pisać
> sam.

A zleceniodawca wymaga formalnego dowodu poprawności programu?

do góry

> A zleceniodawca wymaga formalnego dowodu poprawności programu?

nie wymaga, ale jeśli mój algorytm będzie niepoprawny to zostanie poważnie naruszona
reputacja jego firmy

do góry