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