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