[devel] I: new package

[devel] 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: [devel] I: new package

[aen]

Vitaly Lugovsky пишет:

> why-1.05-alt1.src.rpm ушёл в incoming.
>
> Это средство для автоматического доказательства аннотированных
>программ (т.е. спецификация идёт внутри кода, а не отдельными
>утверждениями), работает поверх Coq (и некоторых других
>proof-assistant-ов). Понимает некоторое подмножество языка C (без
>арифметики указателей) и подмножество Caml (без type inferrence,
>и т.п.)
>
> A must have для любого уважающего себя программиста. Давайте
>писать доказанно безошибочный код, и побольше!
>

Давайте :-)

Rgrds, Алексей

>  
>