[sisyphus] I: new package

[Vitaly Lugovsky]

On Sun, 16 Mar 2003, Pavel S. Khmelinsky wrote:

> >писать доказанно безошибочный код, и побольше!
> >
> > В ближайшее время в Сизиф пойдёт и система Krokatoa для
> >доказательства аннотированного Java-кода.
> >
> >
> А что такое "аннотированный"?

 Комментарии к коду содержат констрейны (e.g., что такой-то
параметр всегда больше нуля, что переменная x обязана быть больше
суммы y и z, ну и т.п.).

 В качестве примера в Why было доказательство оптимальности
алгоритма Бейзенхема, рекомендую ознакомиться.