Классика баз данных - статьи
и именно этот институт по
и именно этот институт по мере готовности стандартов рекомендует
их к принятию Международной организации по стандартизации (ISO).
Как показывает наличие POSIX 1003.3, POSIX-сообщество справедливо
озабочено проблемой формальной проверки соответствия стандартам
конкретных реализаций. К сожалению, несмотря на наличие целого
ряда соответствующих программных продуктов, проверки носят только
синтаксический характер. Как и большинство современных
программных стандартов, все документы POSIX включают описание
семантики только на неформальном уровне.
Приведенные примеры, конечно, затрагивают лишь небольшую часть
современных программных стандартов. Однако этого достаточно,
чтобы продемонстрировать основную проблему: мы научились (и уже
давно) формально специфицировать синтаксис программных
конструкций, но не умеем на том же уровне простоты
специфицировать их семантику. И дело не в том, что отсутствуют
языки спецификации семантики (например, существует красивый язык
алгебраических спецификаций SDL). Беда в том, что при
использовании любого такого языка семантические спецификации
получаются слишком сложными. Сложность семантической спецификации
программной конструкции приближается к сложности реализации этой
конструкции на языке программирования. Поэтому, в частности,
возникает задача проверки правильности (или отладки?) самих
спецификаций. А на что при этом опираться? Снова на неформальное
описание семантики?
Поэтому, как это не печально, в ближайшем будущем нам придется
принимать на веру заявления производителей программных продуктов
об их соответствии стандартам. Некоторую уверенность может дать
процедура сертификации программного продукта, производимая
авторитетной и независимой организацией. Но и эта уверенность
может быть только относительной, поскольку эксперты, выполняющие
процедуру, тоже опираются на неформальные спецификации семантики.
