OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Пятница, 29 Март, 2024 02:41

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 52 ]  На страницу Пред.  1, 2, 3
Автор Сообщение
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Четверг, 05 Апрель, 2018 18:59 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
Comdiv писал(а):
Тут много неправды... Разбирать лень...

В самом деле, разбирать буквоедство стандартов без практики -- толку мало. Когда и где допустимы while-ы (как и do...while/repeat..until), допустимы ли в условиях для for-а в C/Java-like иные выражения кроме диапазона по-паскалевски для одной переменной, и пр. -- всё это разборки с "сертификационными комиссиями", тогда буквоедство будет по делам уже.
Comdiv писал(а):
и программирование под доказательство не запрещает break

Действительно, дисциплина программирования запретов наложить не может (в принципе-то, код можно хоть на goto оформить, если модель вычислений соблюдать). Формализмы теоретического доказательного программирования у Дейкстры/Гриса также break не запрещали (если не ошибаюсь, явных break-ов то вообще не было, разве что аля abort как крах программы, но в таких случаях и доказывать нечего).


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Четверг, 05 Апрель, 2018 19:28 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
PSV100 писал(а):
В самом деле, разбирать буквоедство стандартов без практики -- толку мало.
Можно и без практики разбирать, дело не в этом. Стандарты "безопасного" кодирования не претендуют на всеохватность и их соблюдение лишь означает, что были выполнены определённые меры предосторожности, что может подвтердить независимая комиссия. Но опора на стандарты как главный критерий безопасности - это вредительство, особенно вне области применимости.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Четверг, 05 Апрель, 2018 19:37 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
PSV100 писал(а):
Действительно, дисциплина программирования запретов наложить не может (в принципе-то, код можно хоть на goto оформить, если модель вычислений соблюдать). Формализмы теоретического доказательного программирования у Дейкстры/Гриса также break не запрещали (если не ошибаюсь, явных break-ов то вообще не было, разве что аля abort как крах программы, но в таких случаях и доказывать нечего).

Да, наличие "богатых" возможностей по управлению потоком выполнения не приводит к автоматическому злоупотреблению ими, но их наличие делает проверку злоупотребления сложной задачей. Более того, отсутствие разнообразных средств переходов не приводит к автоматическому запрету неструктурного программирования, а лишь делает его использование более накладным. Это следствие полноты по Тьюрингу.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Четверг, 05 Апрель, 2018 21:18 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 1549
Comdiv писал(а):
Исходя из рекомендаций к коду для атомных станций, которые регламентируют, что цикл должен иметь константное максимальное количество итераций и того, что в общем случае проанализировать количество итераций для инструментальных средств может быть затруднительным, то, по-хорошему, язык должен предоставлять цикл подобного вида:
Код:
Loop =
  IdentOk ":=" LOOP Limit WHILE Expression DO
    Statements
  END .

Limit = ConstExpr | MIN(ExprLimit, ConstExpr) .

Или какого другого? Или не должен?


У меня года два назад была такая фантазия:
Код:
FOR i := 1 TO n UNTIL Expr DO
    ...
END;

:)

Ну а в целом по теме ветки этот регламент совершенно логичен и вытекает из теории вычислимости.
Т.е. это рекомендация ограничить вычисления только примитивной рекурсией.
Я б вообще это ввел бы во все языки (опционально) :)

А еще недавно мне пришла в голову мысль что и синтаксис тоже было бы неплохо ограничить примитивной рекурсией. Если глубина вложенности синтаксических конструкций будет ограничена в языке, то компилятор можно сделать надежнее и очевидно скомпилить его можно в более эффективный маш код.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Четверг, 05 Апрель, 2018 23:06 

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1428
ilovb писал(а):
У меня года два назад была такая фантазия:

50 лет назад у кое-кого тоже была. Это же цикл из Алгола-68.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Пятница, 06 Апрель, 2018 00:01 

Зарегистрирован: Воскресенье, 28 Май, 2006 22:12
Сообщения: 1693
Вы знаете, я что-то совсем потерялся в том, ЧТО обсуждается...

Старею, наверное.

И скажу так, что в последние лет 10 у меня стало преобладать настроение "положить на стандарты".
Нет, на базовые механизмы и идеи того или иного средства представления идей, естественно, "положить" уже нельзя, потому, что средство просто перестанет быть самим собой...
Но вот комбинирование и манипулирование в зависимости от конкретной ситуации в задаче - лучше, чем изобретение и следование "стандартам" и догмам.
(
Как там классики выражались? "Марксизм - не догма"... Как только от классиков отошли, получили загибон системы.
)
С другой стороны, то, о чём я написал выше в своих сообщениях, конкретного языка не касается. Здесь уже нарабатываются законы "общеалгоритмического" и ООП подходов.
Мне не нравятся ристалища по поводу внешнего вида и "непременной атрибутики" тех или иных синтаксических конструктов. В идеале лучше бы иметь язык с назначением оных собственных, наиболее подходящих задаче... А уж если этого нельзя поиметь, тогда ограничиваюсь минимальнонагруженными базовыми в данном формализме и переношу дополнительную семантику подразумеваемых атрибутов на библиотечные решения (как в случае с ForEach и Find).
Всё равно такие решения "в малом" просто "утонут" и уйдут на семнадцатый план при проектировании системы "в большом".
Более желательная цель - не в наборе/выборе множества догм и неукоснительном их соблюдении, аж - до усирачки и вопреки здравому смыслу в конкретной ситуации, а - воспитание и научение способностям к анализу этой конкретной ситуации и конструированию (или - через возможности расширения/добавления синтаксических конструкций и их семантики, или - через библиотечные/классовые примитивы) - до наиболее адекватного языка представления и интерпретации этой ситуации (DSL).


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Пятница, 06 Апрель, 2018 00:01 

Зарегистрирован: Воскресенье, 09 Март, 2008 22:38
Сообщения: 372
PSV100 писал(а):
Р-комплексы были и в промышленности (включая и "военку")

Были. Например, в космической отрасли. И вообще, насколько помнится, в Интернетах писали, Р-схемы возникли по заказу РВСН.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Пятница, 06 Апрель, 2018 19:02 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
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-х надо было что-то выправлять для "мэйнстрима" (и видать не только циклы), чтобы не было сплошного "вредительства" теперь.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Суббота, 07 Апрель, 2018 07:03 

Зарегистрирован: Вторник, 29 Ноябрь, 2005 21:41
Сообщения: 1030
PSV100 писал(а):
чтобы не было сплошного "вредительства" теперь.
Удивительная легкость.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Суббота, 07 Апрель, 2018 10:12 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
Чётто много буков.

Кто-нить может объяснить пафос диспута в трёх строчках?

Мне про циклы интересно в рационально-образовательных целях.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Суббота, 07 Апрель, 2018 10:49 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 583
Откуда: Москва
Info21 писал(а):
Кто-нить может объяснить пафос диспута в трёх строчках?

Есть такие задачи реального времени, для которых нужно гарантировать ограниченность числа итераций в цикле. Гарантия означает, что любой написанный или сгенеренный код, прошедший синтаксическую проверку, ограничен по числу итераций, как цикл FOR. Каким циклом(циклами) можно обойтись, исключив все остальные? Comdiv инициировал пример в начале раздела.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл для атомных станций
СообщениеДобавлено: Суббота, 07 Апрель, 2018 15:03 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
Спасибо.


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 52 ]  На страницу Пред.  1, 2, 3

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 4


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2024, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB