> -- Comdiv писал(а):
> Кто на кого кричит?
"Крики" были (и очень полезные) в соответствующем разделе форума лет так 6-8 назад, когда тамошние темы были актуальны, да и участники баталий были помоложе, поэнергичнее, "мочили" т.н. контуперных гениев ("должность" популярная в тех ветках форума), игнорирующих методику "под доказательство".
> -- Comdiv писал(а):
> Сертификация должна быть осуществима, желательно простыми средствами. С учётом ограниченного круга применения, требование не выглядит слишком странно.
И вот, если дело доходит до реальных стандартов безопасности, то выясняется, что дисциплина "доказательства для человеков" не является достаточно убедительной и надёжной. Конечно же, реальные процессы сертификации/стандартизации не только технические, но и политические, где возможны всяк разные варианты соглашений о "доверии". Однако, всё же в целом необходимы какие-то средства доказательства, те же контракты в каком-то виде, к примеру, с гарантией корректности, полноты деклараций и т.д. (поэтому, напр., в упомянутой здесь выше Esterel/Lustre недопустимы широкие произвольные рассуждения по Хоару/Дейкстре/Грису и т.п., как минимум в рамках базовых средств валидации). Если соответствующих инструментов нет, то в рамках Паскале/С-подобных языков имеется лишь одно допустимое стандартами средство -- цикл for, без него не о чем говорить (видимо, в т.ч. и насчёт "принципов Калашникова" тоже). Иными словами, "бяка" по методике "под доказательство" -- for + break/exit -- является единственной допустимой формой в реальных стандартах безопасности.
> -- Comdiv писал(а):
> Интересное впечатление  .
Ситуация действительно смешная. Если на борту нет средств доказательств, и в простом "надёжном" императивном языке нет цикла for или break/exit для него -- язык теоретически не применим для стандартов безопасности (в отличие от того же Питона с его паттернами for+break+else, будь у него полноценная статическая типизация. А может быть для некоторых "сертификационных комиссий" и такая сойдёт -- она же есть, мол стандарту соответствует).

Повторюсь, что в реальной практике, видимо, какие-то компромиссы возможны (а то и неизбежны). Может быть для задач и достаточно for-а без exit-а, или возможно введение каких-то библиотечных средств для циклов (аля map/reduce/fill и пр.) с подтверждением "доверия" и т.п. Я не акцентирую на буквоедстве насчёт самого Оберона. Возникают неоднозначности в "классической" методике "под доказательство", если не игнорировать реальные промышленные стандарты безопасности. Или в стандартах безопасности, уж не знаю.