From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <vsl@ontil.ihep.su>
Date: Sun, 16 Mar 2003 03:44:20 +0300 (MSK)
From: Vitaly Lugovsky <vsl@ontil.ihep.su>
To: devel@altlinux.ru
Cc: sisyphus@altlinux.ru
Message-ID: <Pine.LNX.4.53L.0303160336550.12796@ontil.ihep.su>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=koi8-r
Content-Transfer-Encoding: 8BIT
Subject: [sisyphus] I: new package
Sender: sisyphus-admin@altlinux.ru
Errors-To: sisyphus-admin@altlinux.ru
X-BeenThere: sisyphus@altlinux.ru
X-Mailman-Version: 2.0.9
Precedence: bulk
Reply-To: sisyphus@altlinux.ru
List-Unsubscribe: <http://altlinux.ru/mailman/listinfo/sisyphus>,
	<mailto:sisyphus-request@altlinux.ru?subject=unsubscribe>
List-Id: <sisyphus.altlinux.ru>
List-Post: <mailto:sisyphus@altlinux.ru>
List-Help: <mailto:sisyphus-request@altlinux.ru?subject=help>
List-Subscribe: <http://altlinux.ru/mailman/listinfo/sisyphus>,
	<mailto:sisyphus-request@altlinux.ru?subject=subscribe>
List-Archive: <http://altlinux.ru/pipermail/sisyphus/>
Archived-At: <http://lore.altlinux.org/sisyphus/Pine.LNX.4.53L.0303160336550.12796@ontil.ihep.su/>
List-Archive: <http://lore.altlinux.org/sisyphus/>

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

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

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

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