SPARK, инструментарий статической верификации, гарантирующий безопасность и защищённость, теперь лицензирован на условиях GPL (http://libre.adacore.com/libre/tools/spark-gpl-edition/). Благодаря этому теперь и Tokeneer (http://www.openproofs.org/wiki/Tokeneer), проект, где используются формальные методы для математической верификации биометрической системы безопасности, становится "open proof (http://www.openproofs.org/wiki/Main_Page)". Это в свою очередь означает, что весь инструментарий, необходимый для верификации Tokeneer, отныне будет доступным в рамках открытых технологий.
В GPL-релиз SPARK входят следующие технологии:
- Описание языка SPARK
- Полный инcтрументарий SPARK, включая Examiner, Simplifier и Checker
- Вспомогательные инструменты: SPARKSimp, SPARKMake, SPARKFormat и POGS
- Вводные учебные материалы по SPARK и SPARK Pro, с примерами из Tokeneer, включены в сопроводительный релиз пакета Tokeneer Discovery (http://www.adacore.com/home/products/sparkpro/tokeneer/di...URL: http://www.dwheeler.com/blog/2009/06/05/#spark-open-source
Новость: http://www.opennet.me/opennews/art.shtml?num=22070
Звучит как приговор
Что это вообще такое? Что за верификатор?
>Что это вообще такое? Что за верификатор?Верификатор - проверятель истинности (правильности).
То бишь для людей от которых требуют 100% гарантию правильности работы программы
Ага, не забыть только критерии правильностьи верифицировать для начала. На 100%. А перед этим верифицировать критерии оценки критериев :))
Помню была то ли теорема толи что о том, что программ без ошибок не может существовать. Вот и IMHO гарантировать 100% правильность значит заведомо врать.
Не 100% Правильности
а 100% соответствия формальным критериям
Такой теоремы не может быть в принципе.
Вы путаете теорему и гипотезу.«Гипотеза», как бы научно и серьезно это слово не звучало, не является доказанной и, соответственно, верной.