[devel] I: new package

Vitaly Lugovsky =?iso-8859-1?q?vsl_=CE=C1_ontil=2Eihep=2Esu?=
Вс Мар 16 03:44:20 MSK 2003


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

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

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

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




Подробная информация о списке рассылки Devel