OberonCore https://forum.oberoncore.ru/ |
|
Цикл для атомных станций https://forum.oberoncore.ru/viewtopic.php?f=86&t=6188 |
Страница 3 из 3 |
Автор: | PSV100 [ Четверг, 05 Апрель, 2018 18:59 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
Comdiv писал(а): Тут много неправды... Разбирать лень... В самом деле, разбирать буквоедство стандартов без практики -- толку мало. Когда и где допустимы while-ы (как и do...while/repeat..until), допустимы ли в условиях для for-а в C/Java-like иные выражения кроме диапазона по-паскалевски для одной переменной, и пр. -- всё это разборки с "сертификационными комиссиями", тогда буквоедство будет по делам уже. Comdiv писал(а): и программирование под доказательство не запрещает break Действительно, дисциплина программирования запретов наложить не может (в принципе-то, код можно хоть на goto оформить, если модель вычислений соблюдать). Формализмы теоретического доказательного программирования у Дейкстры/Гриса также break не запрещали (если не ошибаюсь, явных break-ов то вообще не было, разве что аля abort как крах программы, но в таких случаях и доказывать нечего). |
Автор: | Comdiv [ Четверг, 05 Апрель, 2018 19:28 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
PSV100 писал(а): В самом деле, разбирать буквоедство стандартов без практики -- толку мало. Можно и без практики разбирать, дело не в этом. Стандарты "безопасного" кодирования не претендуют на всеохватность и их соблюдение лишь означает, что были выполнены определённые меры предосторожности, что может подвтердить независимая комиссия. Но опора на стандарты как главный критерий безопасности - это вредительство, особенно вне области применимости.
|
Автор: | Comdiv [ Четверг, 05 Апрель, 2018 19:37 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
PSV100 писал(а): Действительно, дисциплина программирования запретов наложить не может (в принципе-то, код можно хоть на goto оформить, если модель вычислений соблюдать). Формализмы теоретического доказательного программирования у Дейкстры/Гриса также break не запрещали (если не ошибаюсь, явных break-ов то вообще не было, разве что аля abort как крах программы, но в таких случаях и доказывать нечего). Да, наличие "богатых" возможностей по управлению потоком выполнения не приводит к автоматическому злоупотреблению ими, но их наличие делает проверку злоупотребления сложной задачей. Более того, отсутствие разнообразных средств переходов не приводит к автоматическому запрету неструктурного программирования, а лишь делает его использование более накладным. Это следствие полноты по Тьюрингу. |
Автор: | ilovb [ Четверг, 05 Апрель, 2018 21:18 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
Comdiv писал(а): Исходя из рекомендаций к коду для атомных станций, которые регламентируют, что цикл должен иметь константное максимальное количество итераций и того, что в общем случае проанализировать количество итераций для инструментальных средств может быть затруднительным, то, по-хорошему, язык должен предоставлять цикл подобного вида: Код: Loop = IdentOk ":=" LOOP Limit WHILE Expression DO Statements END . Limit = ConstExpr | MIN(ExprLimit, ConstExpr) . Или какого другого? Или не должен? У меня года два назад была такая фантазия: Код: FOR i := 1 TO n UNTIL Expr DO ... END; Ну а в целом по теме ветки этот регламент совершенно логичен и вытекает из теории вычислимости. Т.е. это рекомендация ограничить вычисления только примитивной рекурсией. Я б вообще это ввел бы во все языки (опционально) А еще недавно мне пришла в голову мысль что и синтаксис тоже было бы неплохо ограничить примитивной рекурсией. Если глубина вложенности синтаксических конструкций будет ограничена в языке, то компилятор можно сделать надежнее и очевидно скомпилить его можно в более эффективный маш код. |
Автор: | Trurl [ Четверг, 05 Апрель, 2018 23:06 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
ilovb писал(а): У меня года два назад была такая фантазия: 50 лет назад у кое-кого тоже была. Это же цикл из Алгола-68. |
Автор: | Wlad [ Пятница, 06 Апрель, 2018 00:01 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
Вы знаете, я что-то совсем потерялся в том, ЧТО обсуждается... Старею, наверное. И скажу так, что в последние лет 10 у меня стало преобладать настроение "положить на стандарты". Нет, на базовые механизмы и идеи того или иного средства представления идей, естественно, "положить" уже нельзя, потому, что средство просто перестанет быть самим собой... Но вот комбинирование и манипулирование в зависимости от конкретной ситуации в задаче - лучше, чем изобретение и следование "стандартам" и догмам. ( Как там классики выражались? "Марксизм - не догма"... Как только от классиков отошли, получили загибон системы. ) С другой стороны, то, о чём я написал выше в своих сообщениях, конкретного языка не касается. Здесь уже нарабатываются законы "общеалгоритмического" и ООП подходов. Мне не нравятся ристалища по поводу внешнего вида и "непременной атрибутики" тех или иных синтаксических конструктов. В идеале лучше бы иметь язык с назначением оных собственных, наиболее подходящих задаче... А уж если этого нельзя поиметь, тогда ограничиваюсь минимальнонагруженными базовыми в данном формализме и переношу дополнительную семантику подразумеваемых атрибутов на библиотечные решения (как в случае с ForEach и Find). Всё равно такие решения "в малом" просто "утонут" и уйдут на семнадцатый план при проектировании системы "в большом". Более желательная цель - не в наборе/выборе множества догм и неукоснительном их соблюдении, аж - до усирачки и вопреки здравому смыслу в конкретной ситуации, а - воспитание и научение способностям к анализу этой конкретной ситуации и конструированию (или - через возможности расширения/добавления синтаксических конструкций и их семантики, или - через библиотечные/классовые примитивы) - до наиболее адекватного языка представления и интерпретации этой ситуации (DSL). |
Автор: | TAU [ Пятница, 06 Апрель, 2018 00:01 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
PSV100 писал(а): Р-комплексы были и в промышленности (включая и "военку") Были. Например, в космической отрасли. И вообще, насколько помнится, в Интернетах писали, Р-схемы возникли по заказу РВСН. |
Автор: | PSV100 [ Пятница, 06 Апрель, 2018 19:02 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
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-х надо было что-то выправлять для "мэйнстрима" (и видать не только циклы), чтобы не было сплошного "вредительства" теперь. |
Автор: | Сергей Оборотов [ Суббота, 07 Апрель, 2018 07:03 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
PSV100 писал(а): чтобы не было сплошного "вредительства" теперь. Удивительная легкость.
|
Автор: | Info21 [ Суббота, 07 Апрель, 2018 10:12 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
Чётто много буков. Кто-нить может объяснить пафос диспута в трёх строчках? Мне про циклы интересно в рационально-образовательных целях. |
Автор: | Дмитрий Дагаев [ Суббота, 07 Апрель, 2018 10:49 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
Info21 писал(а): Кто-нить может объяснить пафос диспута в трёх строчках? Есть такие задачи реального времени, для которых нужно гарантировать ограниченность числа итераций в цикле. Гарантия означает, что любой написанный или сгенеренный код, прошедший синтаксическую проверку, ограничен по числу итераций, как цикл FOR. Каким циклом(циклами) можно обойтись, исключив все остальные? Comdiv инициировал пример в начале раздела. |
Автор: | Info21 [ Суббота, 07 Апрель, 2018 15:03 ] |
Заголовок сообщения: | Re: Цикл для атомных станций |
Спасибо. |
Страница 3 из 3 | Часовой пояс: UTC + 3 часа |
Powered by phpBB® Forum Software © phpBB Group https://www.phpbb.com/ |