Прочитал возникшую недавно здесь на форуме дискуссию по поводу отладчиков -- их нужности/бесполезности и прочая смежная проблематика, прежде всего понимание "отладки" и "доказательства". В результате вспомнилась эта ветка форума -- вообще-то с непростым вопросом в начале. Лично я в своей практике напрямую не связан с жёсткой системой сертификации/валидации, поэтому мои впечатления лишь косвенные и неоднозначные, о чём ниже.
Дмитрий Дагаев писал(а): Для категории A установлены требования по стандарту 60880: Цитата: B.4ag Следует использовать циклы только с постоянными максимальными областями значений переменной цикла
Как реализовывать, в стандарте не сказано. Ваш пример - это, видимо, вариант линейного поиска, но с зафиксированным максимальным значением и результатом поиска. Для сертификационной комиссии такая реализация будет являться доказательством, в отличие от универсального цикла WHILE, где не гарантирован предел числа итераций...
Вот в том и дело, что весь смежный раздел форума про программирование "под доказательство" кричит о том, что сертификационная комиссия -- "контуперные гении", как и создатели этого стандарта, мол не умеют пользоваться инвариантами циклов, ограничивающей функцией и т.д.
Яркий пример попыток добиться соответствия подобным стандартам -- последний Safety-Critical Java, где учитывают уже накопленный опыт промышленных профилей. Там циклы задаются в форме с обязательной границей:
Код: // вместо аналогов:
for(Entry e = tab[i]; e != null; e = e.next)
// необходимо примерно так:
Entry e = tab[i];
for (int j = 0; j < entries.length; j++) {
if (e == null) break;
...
e = e.next;
}
А также требуется явно уточнять семантику границ, если она определяется косвенно, аля:
Код: @LoopBound(max=elementCount)
for (int i = 0; i < elementCount; i++){...}
Когда как в смежном разделе форума про программирование "под доказательство" мы наблюдаем даже специальные темы по поводу удаления break-ов и прочих exit-ов из циклов и их преобразование к "каноническому циклу Дейкстры" или к базовым "классическим" паттернам.
В принципе, понять "контуперных гениев" из стандартизации можно. Ниже пример техники автоматического поиска инварианта цикла и контроля завершимости:
Better termination proving through cooperation
Примерчик из статейки выше:
Код: y := 1;
while x > 0 do
x := x − y;
y := y + 1;
done
, где акцент на том, что изменение x (его уменьшение) зависит от изменения y -- понимание зависимостей есть основная забота при верификации (о чём и статья, кроме прочих не менее сложных проблем, как использование указателей и др.) и такая задача отнюдь не проста (в т.ч. и проверка корректности задаваемых деклараций контракта).
И, фактически, в той же Safety-Critical Java проблематика циклов, связанных с условно бесконечными данными, вводом-выводом и т.п. трансформируется в целом в проблему управленческих циклов -- построение и анализ моделей взаимодействующих процессов, с совсем другой природой проверок. В случае вычислительных алгоритмов поверх конечных структур данных поступают максимально "прямее", "в лоб" (к слову, аналогичная картина вырисовывается и в смежной ветке форума про Esterel/Lustre, однако вместо циклов "for" в языках применяются контролируемые функции-итераторы вида map/reduce и т.п.).
Как бы там ни было, стандарт, вроде как, требует "надёжной" ясности в том числе и для моделирующего человека (а точнее, прежде всего для человека, уж затем и для формальных методов/инструментов). И впечатление, что какой-нибудь Питон (особенно с учётом потенциальной аннотации типов и соответствующего контроля) лучше адаптирован к стандарту, чем те же Обероны -- наличие else-секции в операторах циклов, исполняющейся в случае несрабатывания break-ов по завершению цикла -- "широкая" приспособленность к паттернам стандарта.
Вот такой, может быть "неожиданный нежданчик" (если я, всё-таки, не ошибаюсь в понимании стандарта).
|
.