[sisyphus] I: new package

[sisyphus] I: new package

[Vitaly Lugovsky]

 why-1.05-alt1.src.rpm ушёл в incoming.

 Это средство для автоматического доказательства аннотированных
программ (т.е. спецификация идёт внутри кода, а не отдельными
утверждениями), работает поверх Coq (и некоторых других
proof-assistant-ов). Понимает некоторое подмножество языка C (без
арифметики указателей) и подмножество Caml (без type inferrence,
и т.п.)

 A must have для любого уважающего себя программиста. Давайте
писать доказанно безошибочный код, и побольше!

 В ближайшее время в Сизиф пойдёт и система Krokatoa для
доказательства аннотированного Java-кода.

Re: [sisyphus] I: new package

[Pavel S. Khmelinsky]

Vitaly Lugovsky wrote:

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

Re: [sisyphus] I: new package

[Vitaly Lugovsky]

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

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

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

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

Re: [sisyphus] I: new package

[Pavel S. Khmelinsky]

Vitaly Lugovsky wrote:

>On Sun, 16 Mar 2003, Pavel S. Khmelinsky wrote:
>
>  
>
>>>писать доказанно безошибочный код, и побольше!
>>>
>>>В ближайшее время в Сизиф пойдёт и система Krokatoa для
>>>доказательства аннотированного Java-кода.
>>>
>>>
>>>      
>>>
>>А что такое "аннотированный"?
>>    
>>
>
> Комментарии к коду содержат констрейны (e.g., что такой-то
>параметр всегда больше нуля, что переменная x обязана быть больше
>суммы y и z, ну и т.п.).
>
> В качестве примера в Why было доказательство оптимальности
>алгоритма Бейзенхема, рекомендую ознакомиться.
>  
>
Понял, спасибо за разъяснение.

>
>_______________________________________________
>Sisyphus mailing list
>Sisyphus@altlinux.ru
>http://altlinux.ru/mailman/listinfo/sisyphus
>
>
>  
>