Comdiv писал(а):
Стандарты "безопасного" кодирования не претендуют на всеохватность и их соблюдение лишь означает, что были выполнены определённые меры предосторожности, что может подвтердить независимая комиссия. Но опора на стандарты как главный критерий безопасности - это вредительство, особенно вне области применимости.
Интересное мнение. Уверен, что таково не одиноко, и я не цепляюсь к взглядам, и реплика ниже адресована не в адрес кого-то лично. Скорее, здесь проявляется общий диагноз для сегодняшнего IT.
В частности, на любом этапе моделирования в любой предметке (хоть в школьной математике) в случае ограниченной рекурсии/итерации необходимо эти ограничения соблюдать (согласно задачам приближаться к конечной цели). Когда эти же естественные требования переносятся на этап программирования, то возникает "вредительство". Но не понятно, кто же "вредитель" -- здравый смысл или распространенные языки программирования.
В самом деле, понять разработчиков профиля для той же Safety-Critical Java можно: если они внесут существенные изменения в сам язык программирования, то для процедур сертификации возникают уже и соответствующие вопросы и проблемы иного масштаба (для всех потенциальных пользователей во всех отраслях). А поскольку путь убеждения комиссий лежит через runtime-гарантии, то среди языковых средств на этом пути лишь цикл for (и то с ограничениями). И вот циклы for, с возможными break-ами и всякими анализами, не располагают к рассуждениям насчёт инвариантов циклов и прочему согласно соответствующей дисциплины (возникает "вредительство"). В то же время такие циклы не очень то вписываются и для моделирования в стиле "управленческих рассуждений", о которых речь была выше в теме. Такая форма циклов (и проверок) требует и в этом случае ещё адаптации к функциональной форме (в этом плане не лучше и loop-ы с break-ами, которые возвращают данные, во всяких Rust-ах их вводят для других понтов). Лишь по своему характеру такие циклы и проверки ближе к дисциплине "по-управленческому".
На всякий случай уточню. Некая нестыковка дисциплин, о которой была речь в этой ветке, вовсе не означает какой-то там несовместимости, противоположности. Такого быть и не может, поскольку ведь рассуждения об одном и том же, но всего лишь чуть под разным соусом. К примеру, на сайте
майкрософтского F-Star (или под их крышей) -- модификация ML для задач моделирования -- в тамошнем туториале сразу же заметны ключевые позиции. Там не используют инварианты для while-циклов по мотивам Eiffel, Frama-C, Dafny и т.п. Собственно то, ничто не мешает их использовать (м.б. есть и плагины соответствующие), но в тех краях они не востребованы в той практике. Фактически, как бы, циклы вместе с связанными переменными "вырезаются" из императивной программы, трансформируются в "функцию-программу" (согласно "предикатному" программированию выше). Такая функция становится полностью детерминированной через пред- и постусловия, а также через соответствующую оценку рекурсии. Плюс не отменяется "weakest precondition calculus" для любых инвариантов, для функций хоть "леммы" привязывай. И такие обособленные "кирпичики" являются удобной формой для последующих рассуждений об их совокупности -- о взаимодействии в каком-либо виде. К тому же такая форма увеличивает потенциал для различных автоматических построений предикатов (в т.ч. и для рекурсий), по аналогии с ML-вским выводом типов.
По сути, даже "управленческое" взаимодействие "кирпичиков" есть аля "управленческий цикл Дейкстры". Однако базис рассуждений по Грису/Дейкстре является очень общим, верхнего уровня, и требует дальнейшей модельной формализации. Можем даже наблюдать некое "соединение" дисциплин, напр., в "классике" для "проверки на моделях" как Promela/Spin, где в базовом модельном Си-подобном языке есть оператор цикла почти как по Дейкстре (хотя семантически тамошнее понятие недетерминизма требует уточнение на фоне оригинала, и выделяется как "do...od", а также "if...fi"), но закулисная верификация на автоматных подходах.
И вот, условное принуждение для for+break+проверки -- есть "вредительство", якобы лишь мешающее. Предположим, что вместо такого костыля пусть существует возможность для Оберона адаптировать цикл while по мотивам, как предлагалось в начале темы по схеме:
LOOP Limit WHILE Expression DO Statements END
Пусть в т.ч. и как "цикл Дейкстры". С помощью "limit" вводятся runtime-гарантии, что удовлетворяет "независимую комиссию". Теперь предположим, что такое же расширение надёжности вводится и в Eiffel -- как некий "референсный" представитель дисциплины программирования под доказательство, мол он также теперь становится применимым для стандартов безопасности. Подобный цикл в таком случае выглядит аля:
Код:
from
i := 1
until
i > datas.count
variant
datas.count + 1 - i
limit
datas.count
loop
use_data ( datas.get_item(i) )
i := i + 1
end
Новый контракт "limit" не является вариантом или ограничивающей функцией цикла (как и прочими дефинициями для циклов) -- он здесь лишний для такой дисциплины, "не пришей кобыле хвост" (на всякий случай, в Eiffel-е необязательные операторы from и until -- не аналог for-а по-паскалевски). Опять "вредительство", как минимум для карьеры Мейера, ибо для "чистоты" моделирования этот контракт надо "заклеивать бумажкой", чтоб его никто не видел. А убрать контракт не дадут "комиссии", ибо контракт variant и прочее не обязательны и даже с ним Eiffel не всегда может догадаться о кривизне кода, да и нет у него "железных" гарантий.
В общем-то, стандарты безопасности "издеваются" над всеми. А, к примеру, Esterel-и 80-х годов с императивными циклами да Lustre тех же лет с "лямбдами" со стандартами дружат, причём от пользователей лишнего не требуют.
Видимо, ещё в 80-х надо было что-то выправлять для "мэйнстрима" (и видать не только циклы), чтобы не было сплошного "вредительства" теперь.