OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Пятница, 21 Июнь, 2019 01:08

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




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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 357
Илья Ермаков писал(а):
Дмитрий Дагаев писал(а):
Все-таки главное в 60880 - обеспечить(верифицировать) отсутствие зависаний в циклах путем ограничения числа итераций.

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

У меня сложилось впечатление, что требования ограничений итераций связаны с теми задачами, где, как правило, оперируют фиксированными структурами данных, с заранее приготовленными ресурсами (перед содержательным исполнением). И лимиты как таковы возникают естественно. В таких задачах важно, прежде всего, не допустить (верифицировать) алгоритмических ни deadlock-ов, ни livelock-ов. К тому же для случаев оценки временных затрат и всяких там тактов важна не столь индуктивная оценка верхней границы итераций/рекурсий (мол завершимость существует), а само точное значение.
Во всяком случае разборы полётов с такими вещами как Esterel, Safety-Critical Java ничего другого, вроде как, не отражают.

В то же время, рядом возможны, а точнее неизбежны и задачи с "безлимитными" циклами для того же ввода/вывода и т.п., и функциональные требования там иные. В буквоедстве стандартов не силён, скорее всего, для задач определяются разные level-ы или т.п.


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

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 333
Откуда: Москва
Илья Ермаков писал(а):
Дмитрий Дагаев писал(а):
Все-таки главное в 60880 - обеспечить(верифицировать) отсутствие зависаний в циклах путем ограничения числа итераций.


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

Ну тут несколько вариантов получается:
1. Цикл FOR для перебора фиксированного количества вариантов. Тут конец цикла не обрабатывается.
2. Цикл FOR с возможностью выхода по отказу. Стандарт 60880 регламентирует
Цитата:
B.4ac Следует избегать переходов из циклов, если они не ведут к полному окончанию цикла. Исключение - выход по отказу
далее отказ="преждевременное завершение" может как-то обрабатываться.
3. Цикл "Линейный поиск", завершение по исчерпанию как "не найдено".


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

Зарегистрирован: Вторник, 27 Февраль, 2018 09:18
Сообщения: 72
Comdiv писал(а):
Вы пишете, что компилятор тоже важен. Кто-то утверждает обратное?

Я пишу, что в первую очередь важна семантика.
Синтаксис это уже дело вспомогательное.
Например, в Python есть оператор goto (ну или его сделать какой-то там библиотекой -- не суть).

С точки зрения "общей теории", раз есть goto, то возможны самые сложные циклы, которые похлеще чем "простой бесконечный for".

С другой точки зрения, можно в сам компилятор/интерпретатор встроить подсчёт количества "обратных переходов" (ну, когда либо for, либо break, либо continue, либо ещё какой там оператор переходит на предшествующую строку в коде) и останавливать функцию при достижении критического значения.

Поэтому слова
Дмитрий Дагаев писал(а):
лучше всего писать специальный компилятор с одним и только одним циклом, как в начале темы

очень сильно намекают на то, что Дмитрий путает синтаксис, семантику и компилятор.

Илья закономерно указывает на то, что гораздо важнее каким-то образом определять "что будет выполняться при превышении количества итераций".


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

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 861
Откуда: Киев
Владимир Ситников писал(а):
... Поэтому слова ... очень сильно намекают на то, что Дмитрий путает синтаксис, семантику и компилятор.
Я даже не представляю, из чего сделан такой вывод.

Говорить о семантике без синтаксиса, это всё равно, что говорить о смысле слов без слов. Так что нет, синтаксис - это дело не вспомогательное, это основа для дальнейших размышлений. Более того, как можно видеть, синтаксис языков программирования, что в терминах естественных языков больше соответствует синтаксису и грамматике, задаётся не совершенно новыми символами, а используют термины естественных языков, интуитивно соответствующих смыслу конструкций. Это означает, что, отчасти, синтаксис ЯВУ задевает и семантику.

Возвращаясь к конкретному примеру возможного синтаксиса цикла в начале темы, то его семантика тем более ясна, что оперирует терминами уже известного языка с известной семантикой, и уточняется контекстом разговора. Что в семантике цикла непонятно для читателей? Как из отсутствия нудного разжёвывания можно сделать вывод, что кто-то путает синтаксис, семантику и компилятор?


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 357
Цитата:
Поэтому допилить для данной задачи именно Оберон-07 представляется разумным

По ходу дела возникают ещё соображения, если вдруг гипотетически что-то допиливать. Кроме проблематики "лимитов" для циклов есть ещё одна существенная штуковина. Если не использовать break/exit-ы и соблюдать инварианты и пр., то те же циклы вынуждают частенько прибегать к "грязным" приёмам в виде "побочных эффектов" в предикатах (условиях).

Вспоминается показательная дискуссия: "Выход из цикла или смерть Кощея"
, где требуется "эффективно" без лишних затрат (якобы важно) найти иглу (и ещё схожая задача):
Изображение

Изображение

Для понятности и "под доказательство" типовой стиль решения аля:
http://oberspace.dyndns.org/index.php/topic,425.msg13278.html#msg13278
Код:
PROCEDURE Store (obj: ANYPTR; VAR ptr: ANYPTR): BOOLEAN;
BEGIN
    ptr := obj;
RETURN obj # NIL
END Store;

i := 0;
WHILE (i < сундуки.length) &
    ~( Store(ЗАЯЦ(сундуки[i]), заяц)) & Store(УТКА(заяц(Заяц)), утка)) &
        Store(ЯЙЦО(утка(Утка)), яйцо)) & Store(ИГЛА(яйцо(Яйцо)), игла)) )
DO
    INC(i)
END

, где в условии while вместо ожидаемого анализа результатов работы выполняются непосредственно содержательные прикладные действия. Причём упорядоченность действий зависит от примененного порядка логических операций (и от порядка аргументов) -- семантически эти операции (как и порядок аргументов) для этого не предназначены, в технологическом языке (в данном языке программирования) последовательность определяется через ";" плюс "защитные" выражения (if-ы) да условия повторения действий.

Для С-подобных языков решение может быть таким (комментарий к коду был в "исходнике"):
http://oberspace.dyndns.org/index.php/topic,425.msg13047.html#msg13047
Код:
// На Си можно избежать дублирования кода пользуясь тем фактом,
// что оператор присваивания возвращает значение:

i = 0;
while ((i < колВоСундуков) && (
       !(заяц = ЗАЯЦ(сундуки[i]))
    || !(утка = УТКА(заяц)))
    || !(яйцо = ЯЙЦО(утка))
    || !(игла = ИГЛА(яйцо))
)) ++i;

Этот случай более "продвинутый" в том смысле, что в нём хоть заметны результаты прикладной работы -- присваивание переменных (вместо визуально скрытого изменения аргументов при вызове процедур в предыдущем варианте решения задачи). Правда в С это присваивание ещё нужно заметить. В ряде современных С-производных языков в таких случаях есть "прогресс" и могут требовать введения новых переменных по месту через модную попсовую конструкцию аля "let" вида:
!(let заяц = ЗАЯЦ(сундуки[i]))

Ну, а ключевое в той дискуссии было след. решение от её инициатора:
http://oberspace.dyndns.org/index.php/topic,425.msg13272.html#msg13272

Изображение

Изображение

, где с помощью нового оператора "andwile" условие while-цикла как бы временно "разрывается" (с проблемками), но с соблюдением "каноничности" инвариантов с постусловием и пр.:
http://oberspace.dyndns.org/index.php/topic,425.msg13861.html#msg13861

Вообще-то, проблематика "грязных" предикатов навязывается не только циклами. Поэтому решение выше если и приемлемое, но лишь частично, в смысле прочие аспекты не решает. К примеру -- там же вариант задачи "близко к идеальному" (заметка к коду была в "исходнике"):
http://oberspace.dyndns.org/index.php/topic,425.msg13083.html#msg13083
Код:
WHILE list.HasMoreElements() AND смерть = NIL DO
    сундук := list.GetNext();   
    IF  сундук.UnpackTo( заяц ) AND
        заяц  .UnpackTo( утка ) AND
        утка  .UnpackTo( яйцо ) AND
        яйцо  .UnpackTo( игла ) AND
        игла  .UnpackTo( смерт ) THEN
      Log.String("капец Кащею");
    END;
  END;

+1. Близко к идеальному. Смотришь и всё сразу понятно. 

Про "UnpackTo" и прочее:
http://oberspace.dyndns.org/index.php/topic,425.msg13078.html#msg13078

В варианте выше оператор "if" по сути-то пустой, указан лишь как необходимое синтаксическое средство для выражения порядка действий с "защитными" условиями в виде логической операции (композиции) -- ибо так проще, быстрее, удобнее и понятнее, вроде как. В некоторых современных языках ещё больше упрощают чтоб "не париться", как в Julia, где техника построения кода, такого как ниже, декларируется на уровне "report-а о языке" (с соответствующей поддержкой синтаксиса и семантики):
https://docs.julialang.org/en/stable/manual/control-flow/#Short-Circuit-Evaluation-1
Код:
function fact(n::Int)
    n >= 0 || error("n must be non-negative")
    n == 0 && return 1
    n * fact(n-1)
end

Кстати, можно обратить свое внимание: сходу ли понятна логика действий, если встречается не только сплошные "and"? (ну..., данный пример ещё не самый показательный).
Примечательно то, что ведь такой код для математической аудитории, на которую прежде всего ориентируется Julia, по сути-то есть высшая степень издевательства над математической формой коммутативных операций.

На фоне всех "издевательств" выше, вообще-то, как-то уже и не прилично утверждать, что в IT "контуперность" лишь крепчает, если, к примеру, обратить внимание на Rust, где внедряются "рекурсивные лямбды" -- в соответствие с концепцией продвинутого "expression-oriented функционально-императивного" языка и loop-ы должны быть с возможностью являться "expression по месту", в которых break-и могут возвращать данные (а может быть это есть попытка "спасти" предикаты?):
https://github.com/rust-lang/rfcs/blob/master/text/1624-loop-break-value.md

Попытки снять "издевательство" над предикатами были и на этом форуме, к примеру -- конструкция "AND THEN":
https://forum.oberoncore.ru/viewtopic.php?f=27&t=3175&hilit=andif

Тамошние идеи получили развитие в виде концептуальных конструкций "прогресса" и его циклической вариации (плюс прочее условные и циклические выражения) в проекте PureBuilder:
https://sites.google.com/site/purebuilder/

Однако, видимо, сложные и разнообразные конструкции не приживаются, если можно ведь "по-простому" на базе имеющихся логических средств.

В функциональных языках ситуация чуть иная. В тех же ML-подобных вариациях кроме популярности рекурсивных методов (со своими достоинствами и недостатками) есть и те же императивные итерационные циклы. Причём в тех краях имеется "внедрение" переменных в виде оператора "let ... in" (или математического "где": "... where ..." ) как на примере ниже:
https://realworldocaml.org/v1/en/html/imperative-programming-1.html#for-and-while-loops-1
Код:
let rev_inplace ar =
    let i = ref 0 in
    let j = ref (Array.length ar - 1) in
    (* terminate when the upper and lower indices meet *)
    while !i < !j do
      (* swap the two elements *)
      let tmp = ar.(!i) in
      ar.(!i) <- ar.(!j);
      ar.(!j) <- tmp;
      (* bump the indices *)
      incr i;
      decr j
    done

, где как раз i и j "внедряются" в while-цикл (на всякий случай: оператор "!" есть извлечение значения из "ссылки"). В данном случае let...in скомпонованы в цепочку, что явно выражает последовательность. В целом let (или where) содержат композицию "паттернов" (шаблонов для паттерн-матчинга) -- пусть это по-простому будут "уравнения".
Однако, как видно из примера, в целом семантика "let" предполагает вычисление соответствующего значения по требованию и дальнейшее его использование, в т.ч. и многократное. Т.е. в данном случае i и j вычисляются один раз (создаются "ссылки") и далее лишь используются.

В некоторых ML-вариациях вместо let...in может быть форма оператора "whith ...", как к примеру:
"with ... do ... done"
, что семантически имеет в большей степени окрас "подмешивания". А в "топорном" Lustre и его вариантах семантика вычислений "уравнений" уже чуть иная, там блоки "многоразового" вычисления ("бесконечно" работающие автоматы).
Без вводных объяснений попробую в порядке бреда изобразить потенциальное "внедрение" уравнений для цикла while по мотивам Lustre, но для Паскале-подобного языка. В Lustre-like языках как в Паскалях есть строгое требование определять переменные в начале (фактически аля те же var-секции перед телом процедуры), однако когда удобно возможны и локальные переменные, но в рамках своих подблоков, и также в начале задаются (нечто вроде ML-вских "local ... in ..."). Пусть блок уравнений задаётся в виде:
local <список переменных> with <уравнения> <выражение>

, где секция local с переменными не обязательная, <уравнения> "внедряются" для <выражение>, которое как-то идентифицируется (пока неважно как именно, пусть как "begin ... end" или любое иное допустимое, пока без подробностей).
Ниже псевдо-код по мотивам "поиска иглы":
Код:
...
var
  игла: pointer;
  i: integer;
begin
  ...
  игла := nil;
  i := 0;
  local
    заяц, утка, яйцо: pointer
  with
    rec заяц := ЗАЯЦ(сундуки[i])
    and утка := if заяц <> nil then УТКА(заяц) else nil
    and яйцо := if утка <> nil then ЯЙЦО(утка) else nil
    and игла := if яйцо <> nil then ИГЛА(яйцо) else nil
  while (i <> len(сундуки)) && (игла = nil) do
    i = i + 1;
  end;
  ...
end;

, где оператор "and" как в ML -- отделяет условно (или потенциально) рекурсивные объявления (уравнения в данном случае, в ML возможны и иные виды деклараций), "rec" -- необязательное "начало" рекурсивных объявлений, указано просто для выделения and-ов в один столбец.
Семантику оператора with подразумеваем как некие Lustre-блоки, выражающие такты автомата. Поскольку уравнения в примере привязаны к циклу, то при каждой итерации происходит вычисление уравнений (а точнее -- изменение переменных). В данном случае как только первично обращаются к переменной "игла" при каждой итерации (в рамках привязанного <выражение>) происходит предварительное её вычисление (обновление), что приводит к редукции, т.е. к "раскручиванию" всех связанных уравнений (как обычно в функциональных языках или во всяких Modelica и т.п.). Переменная "игла" является внешней по отношению к оператору with.

В примере в уравнениях используются if-ы для "защиты". В функциональных языках и в их подражателях часто для таких случаев используют алгебраические типы аля "Option[a] = Some(a) | None" и соответствующий "паттерн-матчинг". Однако, в Lustre есть стандартное понятие "наличие данных", как бы некий типовой виртуальный Option, используемый по умолчанию и отчасти скрыто (что снижает необходимость явно использовать соответствующие операции проверок). Уравнение вычисляется (исполняется действие) только тогда, если доступны все(!) необходимые данные. Если при "раскручивании" такта автомата выясняется, что данные на входе действия не могут быть получены в полной мере, то действие не совершается, и его результат считается отсутствующим (в тех краях это есть понимание наличия/отсутствия сигналов и реакции на них).
По мотивам выше приведенного, попробуем оптимизировать (упростить) пример. Вместо алгебраического типа (соответственно без потребности хранить в памяти вспомогательные тэги типов или значений, но enum-ы и т.п. не отменяются) будем использовать обычный integer, но укажем компилятору условие для типа, что бы он понимал "наличие данных" -- директива "present", и значение "по умолчанию" -- нет данных (в Esterel/Lustre-краях так интерпретируется состояние "проводов" в цифровых схемах -- есть/нет сигнал):
Код:
...
var
  игла: integer default (0) present (> 0);
  i: integer;
begin
  ...
  игла := 0;
  i := 0;
  local
    заяц, утка, яйцо: integer default (0) present (> 0)
  with
    rec заяц := ЗАЯЦ(сундуки[i])
    and утка := УТКА(заяц)
    and яйцо := ЯЙЦО(утка)
    and игла := ИГЛА(яйцо)
  while (i <> len(сундуки)) && (not игла) do
    i = i + 1;
  end;
 
  if игла then
     ...
  end;
end;

Функция (или процедура) как "УТКА(заяц: integer): integer" может быть разработана в сторонке со "строгими" обычными integer-ами, но при конкретном её использовании её результат может быть преобразован к "null-able" типу (как в примере). Процедура может задавать в своём объявлении на входе (и выходе) "null-able" тип (соответственно внутри процедуры требуются соответствующий анализ или чего там нужно). У компилятора есть возможность отслеживать потребность в проверках (и "нагибать" разработчика при случаях), или же организовывать runtime-проверки по аналогии отслеживания доступа по nil-значению. В случае "null-able" типа его интерпретация как boolean выглядит вполне понятной.

Недостатки также имеются. Прежде всего, не всегда система уравнений достаточна наглядна и может потребовать явного указания возникающих связей. В таких случаях помогают аля dataflow-схемы в каком-либо виде. Или же в редакторе "отсортировать" уравнения по зависимостям. Но поскольку речь о "подмешивании" уравнений, то требуется некий "баланс", подмешивать в меру.

В Оберонах оператор with используется для другого, но это не важно, поскольку дальнейшее расширение концепции выше для Оберона, скорее всего, является именно что бредом. Во-первых, не соответствует стереотипам "максимального sample", как минимум возникает некое дублирование функционала, т.е. прикручиваются альтернативные средства для базовых. К тому же требуются if-ы как expression (и аналог "match...with..." из ML), а то и "инфиксные защиты" для удобства аля:
яйцо := ЯЙЦО(утка) when заяц = подходящий

Во-вторых -- согласно иным распространённым принципам -- слишком много "закулисной магии", якобы нет явного предписания действий. Это в каком-нибудь ML-выкрутасе "инъекции уравнений" -- нормальны и естественны (или же инъекции "императивщины" в системы уравнений, в зависимости от стиля кода).

А жаль. Ведь язык соблюдает некоторые математические устои. В самом деле, "обновление" или присваивание переменной вместо "x := x + 1" такая форма как "x = x + 1" также есть "издевательство" над "сравнением", если взглянуть на само содержимое операции. Множество в виде "{...}" и др.
Но, всё-таки, неоднозначно то, что издевательство над предикатами в виде "побочных эффектов" является простой и надёжной формой выражения действий.


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

Зарегистрирован: Воскресенье, 28 Май, 2006 22:12
Сообщения: 1369
А - зачем всё это?
В двух словах.


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

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8135
Откуда: Троицк, Москва
Wlad писал(а):
А - зачем всё это?
В двух словах.

Подобные примеры встречались в "Алгоритмах и структурах данных" в главе про рекурсию -- поиск с backtracking, типа.

Там присутствует цикл поиска, но предикат "найдено" может быть установлен только когда обнаружена конструкция, которую нужно по смыслу сохранить. И вот эта конструкция оказывается побочным эффектом предиката.

Найти вполне удовлетворительную форму не удалось, хотя получилось вполне обозримо. Вроде бы.

Те задачки дают хороший контекст для обсуждения локальных процедур и побочных эффектов. О чём и речь в этой ветке, если я правильно понял (до конца не вчитывался).


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

Зарегистрирован: Воскресенье, 28 Май, 2006 22:12
Сообщения: 1369
Ну, я думаю, тут опять будет война личных предпочтений.
К "общему знаменателю" - не приводимо в принципе.
Всяк конструктор языка сам для себя решает.
Мне, вот, в последнее время, Eiffel-подход нравится. Ну, там по циклу (одному виду на всё хозяйство) и в if-ах связки по условиях. Хотя - кто на нём пишет нонче-то? Насколько я понял, даже в Иннополисе Бертран Мейер его только в начальном курсе даёт. Народ недовольно пыхтит. А потом все на что-то мэйнстримовское переползают.

Баловство всё это.

Насколько я понимаю, подобные дискуссии чаще всего возникают между теми, кто SICP не читал, и теми, кому он уже не нужен.


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 357
Wlad писал(а):
А - зачем всё это?
В двух словах.

Воспринимайте изложения выше всего лишь как эмоциональную разрядку, имевшую место (накануне был повод: пришлось долго въезжать в чужой код, где функция внутри условий иногда по указателю изменяла объект, что незаметно. Код не на Обероне, но проблематика характерна для всех распространённых императивных языков).
Я прежде всего акцентировал внимание на широком издевательстве (отчасти вынужденном) над пониманием, что есть предикат (что с циклами также повязано, и часто). И дополню по поводу. Для себя со временем выработался следующий некий критерий.

На сайте Глушковцев имеется хороший примерчик на Р-схемах Вельбицкого:
Пример документирования в визуальной Р-технологии «Вычисления факториала натурального числа»

ИзображениеИзображениеИзображение
ИзображениеИзображениеИзображение

Пусть для некой задачи необходимо пройти путь от постановки (док.1) через спецификации (док. 2.X) до реализации (док. 3.X). В Р-схемах "железное" правило: вверху дуги -- предикат (условие и т.п.), внизу -- действие. Р-схемы по сути есть граф переходов автомата, где чётко разделяются понятия условия перехода и сам переход/шаг системы, как и в любой математической теории насчёт систем переходов в каком-либо виде, нигде ничего не смешивается в одну кучу, иначе никакой теории не будет. Без детального буквоедства конкретного примера на рисунках уточню: документ 2 есть не алгоритмическая, а структурная схема процессов, "Ввод(n)" на док. 2.1 и 2.2 считаем как декларацию входных данных как входные аргументы процедуры. Спецификации могут быть заданы на естественном языке, частично или полностью формализованном, в виде математической нотации и пр. Короче говоря, считается, что они необходимо и достаточно понятны, полны, проверены, надёжны и т.д. (со всеми "циклами Дейкстры" как на ладони, если надо).

Доходит очередь до реализации на технологическом языке (программирования). Если где-то в условии if-ов и прочих while-ов или в шаблонах "паттерн-матчинга" вылазит функция/процедура с "побочным эффектом" -- однозначно нет ей места над дугой в Р-схеме. Если выясняется, чтобы выдержать это правило становится затруднительно без нарушения спецификации, т.е. требуется некая корректировка "предыдущих" утверждённых документов -- то в топку такой технологический язык.

Конечно, последнее утверждение условно. Я всего лишь хочу сказать, что достаточно мысленного эксперимента в общих чертах в рамках любых задачек. Мол накидай себе в уме Р-схемку на понятном естественном языке (условно частично формализованном) в максимально удобном виде (плюс математика, если нужно и т.п.) и Р-схемку на языке программирования без нарушения правил предикатов и сопоставь. И мозги вправятся на место, и оценку языка программирования получишь заодно.

В технологическом языке необходимо чётко выделять "чистые" функции/операции и прочие процедуры и контролировать "чистоту" предикатов (как сделано, например, в упомянутом здесь Lustre, иначе не видать никакой dataflow-модели, как и верификации). Однако чтобы реализовывать такие ограничения необходимы и соответствующие алгоритмические средства для удовлетворения потребностей.


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

Зарегистрирован: Воскресенье, 28 Май, 2006 22:12
Сообщения: 1369
PSV100 писал(а):
На сайте Глушковцев

ЧУР меня! ЧУР!!!
Вы бы ещё какое-нибудь РСА на ночь глядя вспомните!
Пустое это всё. Как минимум. Как максимум - вредительство. (что, впрочем, всегда у Глушкова. Ибо вредитель.)
Формального инструмента так никто и не создал для какого-то внятного оперирования со схемами алгоритмов. Всё вылилось в пронзительную междисциплинарщину и окучивание бюджетов на почве кафедр и институтов "кибернетики".
Забейте.
Мой вам совет. Если уж что-то действительно стоящее хотите почитать - ищите труды (совместные и порознь) Котова и Сабельфельда. Самая известная книжка: "Теория схем программ" (особенно последние две главы).


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 357
Wlad писал(а):
PSV100 писал(а):
На сайте Глушковцев

ЧУР меня! ЧУР!!!
...
Забейте.

Р-схемы в рассуждениях выше не принципиальны. Можно воспользоваться блок-схемами или Драконом, и попытаться вписать в них свои программы. Речь всего лишь о том, что языки программирования вынуждают взять квадратик (действие) и наложить на ромбик (условие). В блок-схемах хрень получается, а не "понятность и наглядность", и все (или в большинстве случаев) в том и дело, что забивают на это дело. В итоге, в целом-то, в IT "народ имеет того правителя, которого заслуживает", где под правителем понимается правящий бал технологический язык программирования (у каждого свой, но в данном контексте основные "правящие" языки принципиально не отличаются). И "пожирание кактуса" не прекращается, а лишь прогрессирует.
Wlad писал(а):
Вы бы ещё какое-нибудь РСА на ночь глядя вспомните!

И РСА (если это регулярные схемы алгоритма), и ЛСА с МСА (логические и матричные схемы), и схемы программ по Ляпунову и их производные, и ряд операторных схем и пр. -- все они применимы, но у каждого формализма своё предназначение для соответствующего класса задач.

Р-схемы же есть графические структуры для отражения последовательной, параллельной и вложенной композиции, с направленными (ограничено) связями да с "петлёй". Нагружая граф предметно можно получить описание и программ, и данных, и хоть БНФ-формы и много чего потребного. По началу даже и не подозреваешь, что ряд вещей можно выражать на такой "топорной" технологии, хоть "лямбды" вписывай, хоть те же уравнения "подмешивай" и т.д. (что крайне проблематично на тех же блок-схемах и всех их модификациях). Причём если в текстовых формализмах те же уравнения вынуждены задавать как совокупность или как параллельная композиция без формализованного порядка, то Р-схемы как раз можно использовать для отражения упорядоченности.
Wlad писал(а):
Пустое это всё. Как минимум. Как максимум - вредительство. (что, впрочем, всегда у Глушкова. Ибо вредитель.)

Не в курсе, в чём Глушков был вредителем. Во всяком случае, весь мир благодарен ему за сделанный вклад, начиная от теории автоматов. В плане алгоритмики его алгебраические методы развиваются до сих пор (система алгоритмических алгебр, "инсерционное" моделирование взаимодействующих процессов, да и сопутствующие идеи имеют развитие, как "алгоритм очевидности" для доказательства теорем и др., а в нынче модном "искусственном интеллекте" до народа только сейчас потихоньку начинает доходить (и то, для тех, кто об этом знает) в чём были соль в результатах его школы, как те же растущие пирамидальные сети, метод группового учёта аргументов и др.). Я не знаток деталей тамошней школы, но, вроде как, методы используются на практике в ряде корпораций (моделирование, включая и имитационное, верификация и т.п.).
Wlad писал(а):
Формального инструмента так никто и не создал для какого-то внятного оперирования со схемами алгоритмов. Всё вылилось в пронзительную междисциплинарщину и окучивание бюджетов на почве кафедр и институтов "кибернетики".

Р-комплексы были и в промышленности (включая и "военку"). Если не ошибаюсь, среди участников данного форума товарищ Kemet имел возможность их пощупать. Поинтересуйтесь впечатлениями (если бы тем же математикам вместо Julia предложили бы Р-схемы, да ещё бы с удобным редактором построения формул, то неизвестно ещё, на что именно они бы выразили своё "ЧУР").


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

Зарегистрирован: Воскресенье, 28 Май, 2006 22:12
Сообщения: 1369
PSV100 писал(а):
Поинтересуйтесь впечатлениями (если бы тем же математикам вместо Julia предложили бы Р-схемы, да ещё бы с удобным редактором построения формул, то неизвестно ещё, на что именно они бы выразили своё "ЧУР").

Поинтересовался в своё время.
И - в Ахтубе, и - возле Витино, и - ещё в паре-тройке похожих мест.
И - у Шалыто, и - у Каршенбойма.
В конце концов остановился на комбинации подходов Мейера, ГолубойБутылки и Миро Самека.
Просто потому, что "об алгоритмах", само по себе - "сферический конь в вакууме".
Первично - описание окружения и его свойств, элементов модели самой системы, представление внешних воздействий и комбинации внутренних условий. А уж алгоиртмика (аки тасование (структур и элементов) данных) на уровне прикладной области - последнее, чем будет заниматься программист в процессе проектирования и реализации системы. Пэтому там, скорее всего, каких-то условий по данным (в грамотно спроектированной системе) НЕ будет. А то, что будет - вполне хорошо ложится в подход Мейера на счёт классификации интерфейсных методов объектов в его книгах.


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 357
Wlad писал(а):
... "об алгоритмах", само по себе - "сферический конь в вакууме".
Первично - описание окружения и его свойств, элементов модели самой системы, представление внешних воздействий и комбинации внутренних условий. А уж алгоиртмика (аки тасование (структур и элементов) данных) на уровне прикладной области - последнее, чем будет заниматься программист в процессе проектирования и реализации системы. Пэтому там, скорее всего, каких-то условий по данным (в грамотно спроектированной системе) НЕ будет. А то, что будет - вполне хорошо ложится в подход Мейера на счёт классификации интерфейсных методов объектов в его книгах.

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

А алгоритмы по определению есть свёрнутая форма развёрток выше, или порождающая их форма. Отсюда, в общем случае, условия по данным на практике неизбежны. И не всегда удобны/применимы таблицы переходов, решений.
И в императивном языке, мягко говоря, очень и очень желательно как раз поступать по Мейеру -- соответствовать его принципу "command/query separation principle" (если мне память не изменяет, или как-то так он обзывался), о чём говорилось выше в теме -- чётко отделять предикаты от действий, иначе потоки работ и потоки данных не нарисуешь (вменяемо, лишь "протокол о намерениях" получишь).

И если вернуться к дискуссии про Кощея выше, то в ней акцентировалось в т.ч. и на следующем. Пусть типовая схема поиска аля (схематично):
Код:
игла := nil;
i := 0;
while (i <> len(сундуки)) and (игла = nil) do
    игла := unpack(сундуки[i]);
    i := i + 1;
end;

Процедура unpack имеет свёрнутую форму всех проверок, когда как в оригинале требовалось или было желанным иметь все проверки рядом на виду. Но сейчас это второстепенно, упрощаем.
Якобы в подобной схеме поиска возникает некая лишняя операция подготовки к следующей итерации (определение следующей ситуации поиска, которое может быть и не тривиальным в общем случае). Т.е. хочется как-то так:
Код:
игла := nil;
i := 0;
while (i <> len(сундуки)) and (игла = nil) do
    игла := unpack(сундуки[i]);
    if игла = nil then
       i := i + 1;
end;

Но тогда есть как бы дублирование проверок (в условии цикла и внутри него). Поэтому хочется и как-то по "Си"-шному:
Код:
игла := nil;
i := 0;
while (i <> len(сундуки)) and (игла := unpack(сундуки[i])) do
    i := i + 1;
end;

Короче говоря, в данном случае принципиальны не столь циклы как таковы, сколько потребность на практике осуществлять некие "монадические" вычисления в относительно простых случаях простыми же средствами (особенно, когда других-то и нет). Или же и без "монад", в любой случае предикат должен быть как "query" по Мейеру -- недопустимость модификации внешних объектов, кроме результата, что должно быть (или желательно) контролируемо со стороны компилятора.
Для Паскале-подобных языков в таком случае предикаты могли бы быть в таком стиле:
Код:
function unpack(obj: pointer; out p: pointer): boolean;
begin
  p := extract(obj);
  Result := (p <> nil);
end;

if (i < len(сундуки)) and
   unpack(сундуки[i], out игла) and
   (игла.размер = образец) then ...

, где такие функции/процедуры как unpack могут лишь изменять/устанавливать результат и/или var-параметры (плюс локальные переменные для внутренних вычислений). Причём при вызове процедуры в рамках предиката ключевое слово аля "out" должно быть указано обязательно для выделения всех результатов "query" (даже если рядом и нет связанных выражений как проверка "игла.размер = образец" выше в примере, но результаты в любом случае где-то могут быть востребованы чуть дальше по коду, и всё должно быть однозначно заметно, как минимум). Для "command" требование всегда явно писать "out" может быть излишним, к тому же не лаконичными будут такие формы как: "inc(out i)".

Если придерживаться по Мейеру, то и необходимо использовать адаптированный язык (вместе с адаптированными мозгами).


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

Зарегистрирован: Воскресенье, 28 Май, 2006 22:12
Сообщения: 1369
PSV100 писал(а):
...

Странно, в ваших примерах смешиваются семантики способов хранения элементов коллекции, навигации по ним и применения предикатов, и - логики более высокого, "прикладного" уровня.
Например, более высокий уровень не должен знать о "границах" или "размерах" коллекции.

Есть базовые операции перебора всех элементов и операция поиска элемента по условию.

Для частных, "учебных" примеров, может возникнуть желание обосновать такую "семантикосмесительную" архитектуру аргументами быстродействия. Но, лучше его всячески в себе подавлять. Даже - позывы к такому действию. В достаточно больших/огромных проектах это - НЕ работает и только способствует разбуханию и усложнению кода.


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 357
Wlad писал(а):
Странно, в ваших примерах смешиваются семантики способов хранения элементов коллекции, навигации по ним и применения предикатов, и - логики более высокого, "прикладного" уровня.
Например, более высокий уровень не должен знать о "границах" или "размерах" коллекции.

В данном случае контекст связан с "низким" уровнем, но не в "уровнях" дело.
К предикатам выше, скорее, можно предъявить претензии следующего плана. Вот такой предикат для while:
Код:
function unpack(obj: pointer; out p: pointer): boolean;
begin
  p := extract(obj);
  Result := (p <> nil);
end;
...
var игла: pointer;
...
while (i < len(сундуки)) and
      unpack(сундуки[i], out игла) and
      (игла.размер = образец) do
...

со скрипом как-то ещё можно переварить. Однако, лишь непосредственно само условие в while. Ведь, скорее всего, такие переменные как "игла" где-то будут использоваться далее, и, фактически-то, "unpack" трансформируется из "query" в "command".

Поэтому, требуются сильнее ограничения. Если гипотетически адаптировать для себя язык программирования (о чём была речь выше в теме), то в предикатах необходимо допускать лишь "чистые" функции и не возвращающие "кортежи". Иначе компилятор должен банить. Это мой основной месседж.
И если в тех же циклах кто-то решил поступить иногда якобы по-проще, "выкручиваясь" через предикаты, то "побочные эффекты" не так уж просто заметить и лучше их пресекать (пусть лучше будут лишние проверки или действия, а те же возможно лишние тривиальные инкременты переменных на себя внимание даже не обращают).


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

Зарегистрирован: Воскресенье, 28 Май, 2006 22:12
Сообщения: 1369
PSV100 писал(а):
Код:
function unpack(obj: pointer; out p: pointer): boolean;
begin
  p := extract(obj);
  Result := (p <> nil);
end;
...
var игла: pointer;
...
while (i < len(сундуки)) and
      unpack(сундуки[i], out игла) and
      (игла.размер = образец) do
...

А зачем вы вводите лишний слой в виде unpack() ?
Код:
for игла in сундуки :
    if игла.размер = образец :
        ...

или - из моего собственного сишного (не плюсплюсного) "класса" List:
Код:
void DoSomethingWithJobListItem( void* object, void* arg )
{
    Job job = (Job)object;
    if( job->_size == *(int*)arg ) {
        ... // do
    }
}

...
List_ForEach( jobList, &DoSomethingWithJobListItem, &size );
...

естественно, что есть два места, где обобщение — ну просто само просится на реализацию.
Первое — это предикат на место условия внутри функции элемента.
Второй — это собственно действие по истинности условия/предиката.
То есть, функция элемента вырождается в нечто:
Код:
void ItemFunc( void*            object
             , ListItemPred*    Pred
             , ListItemAction*  OnTrue
             , ListItemAction*  OnFalse
             , void*            args
             )
{
    if( Pred ) {
        if( (*Pred)( object, args ) ) {
            if( OnTrue ) (*OnTrue)( object, args );
        }
        else {
            if( OnFalse ) (*OnFalse)( object, args );
        }
    }
    else {
        if( OnTrue  ) (*OnTrue )( object, args );
        if( OnFalse ) (*OnFalse)( object, args );
    }
}

Теперь здесь указатель на функцию-предикат несёт дополнительную нагрузку-смысл. В случае, если он != NULL, выполняется классическая проверка в ветвлением. Если же он пуст, то обе функции-действия являются просто двумя фазами выполнения какого-то действия.

Осталось поменять заголовок List_ForEach (и места её вызовов)

Код:
bool Pred( void const*const object, void const*const arg )
{
   return ((Job)object)->_size == *(int*)arg;
}
void OnTrue( void* object, void* arg )
{
   // do ...
}

...
List_ForEach( jobList, &Pred, &OnTrue, NULL/*OnFalse*/, &size );
...

Дальше, сама функция ItemFunc может быть исключена из программы, а её тело переходит в функцию List_ForEach.


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 357
Wlad писал(а):
А зачем вы вводите лишний слой в виде unpack() ?

Ага, кстати, выше была ошибка в цикле (у меня, прежде всего, были мысли по поводу предикатов как таковых, а не циклов). Не было указано отрицание аля:
Код:
function unpack(obj: pointer; out p: pointer): boolean;
begin
  p := extract(obj);
  Result := (p <> nil);
end;
...
var игла: pointer;
...
while (i < len(сундуки)) and
      not ( unpack(сундуки[i], out игла) and
            (игла.размер = образец) ) do
...

Исходная дискуссия про Кощея была связана с "доказательным программированием" и в т.ч. с "линейным поиском". Тогда цикл вида:
Код:
for игла in сундуки :
    if игла.размер = образец :
        ...

должен иметь break в случае обнаружения необходимого элемента. Что, кстати, и соответствует стандартам безопасности, которые требуют эти break-и анализировать в последствии. Однако, как было отмечено выше в теме, "программирование под доказательство" в целом break-ов не допускает:
Цитата:
Поподробнее об инварианте цикла.
Инвариант - "рельсы", по которым он едет - что истинно до начала цикла ("поставили на рельсы") и в конце каждого витка. (А раз в конце каждого витка, то и после завершения цикла тоже. Вот ещё одна причина не делать досрочных выходов из цикла. Тогда пишущему и читающему придётся дополнительно убеждаться, что в каждом месте цикла, где он прерывается, инвариант восстановлен.)

Такое положение возникает исходя из природы императивного изменения состояния (переменных). Тем не менее, имеется нестыковка "доказательного программирования" с реальными стандартами безопасности. Но эта несостыковка несколько шире в целом, о чём далее. Как-то неправильно её игнорировать и при этом заниматься, вроде как, "доказательствами".


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 357
Цитата:
или - из моего собственного сишного (не плюсплюсного) "класса" List:
...

И, кстати, "закулисная магия на лямбдах" также как-то не вписывается в каноны "доказательного программирования". Как и не приветствуется хвостовая рекурсия, где можно избежать лишних проверок или/и действий (прочие рекурсивные методы -- отдельный вопрос, и они применимы).

Здесь на форуме где-то недавно была ссылка на хороший пост по поводу, процитирую здесь для наглядности (для дальнейших изложений) вместе с связанными картинками, несмотря на их громоздкость:
https://forum.oberoncore.ru/viewtopic.php?f=82&t=1896#p27087

Изображение

Изображение

Валерий Лаптев писал(а):
Info21 писал(а):
Валерий Лаптев писал(а):
как это писать "под доказательство"?
Ой. Хороший вопрос, но полный ответ требует подготовки материала.
На самом грубом уровне разница видна здесь:

http://www.inr.ac.ru/~info21/texts/2005 ... ide13.html
http://www.inr.ac.ru/~info21/texts/2005 ... ide14.html

Две программы эквивалентны. Но правильность первой была установлена предварительным преобразованием ко второй.
Вторая -- как раз "под доказательство".

Да, хорошо видать разницу.
Однако меня и при первом прочтении книги Дейкстры, и сейчас не покидает мысль, что написание "под доказательство" касается только самого начального программирования.
То есть максимум до уровня написания процедур и функций.
В любой промышленной системе есть развитое окружение, которое частенько позволяет заменить показанные вами проги одной строкой.
Таким образом, получается, что Дейкстрины методы хороши при обучении программированию, при создании стандартных библиотек.
Ну, и если промышленному программеру действительно приходится писать нетривиальные процедуры. Однако если следовать советам экстремальных программистов, то размер методов следует ограничивать 1-5 строками. Тут и без всякого доказательства все сразу видать.

В промышленном программировании гораздо более важным является хорошая декомпозиция. Причем на всех уровнях (см. опять же Дейкстра - архитектура THE).
А в этом деле формальные методы фактически отсутствуют. И что с этим делать - пока неясно. Полно книжек с советами, как надо делать, или как делать не надо.
Однако все это - только опыт экспертов.

Тут ещё необходимо не забывать, что "экстремальные программисты" в "мэйнстриме" могут накидать "1-5 строк" в стиле:
L = getArray(...).map(x => ...).filter(x => ...).toList(...).takeWhile(x => ...)

, где "без всякого доказательства все сразу видать", но в процессе работы могут создаваться немало промежуточных временных структур и отправляться в мусор (с соответствующими последствиями для мусорщиков). Но там, правда, и не обращают внимание на такие дела. Речь не об этом.
Однако, формальные методы необходимы не только для декомпозиции. Ведь, те же "лямбды" необходимо связывать со всяким прочим и доказывать. Формальные методы около языков программирования в подобных случаях часто обзываются в стиле "зависимых типов" или "liquid types" и т.п.

Для акцента на разнице стиля моделирования "без циклов" (или их инвариантов) можно взглянуть на соседний форум -- "предикатное" и "автоматное" программирование:
https://forum.oberoncore.ru/viewtopic.php?f=152&t=6049&start=20#p103245

, где автор в т.ч. имеет и некую критику "структурного" программирования. Прежде всего, контекст в том, что в структурном программировании убран goto и есть лишь оператор while (да if), но нет ничего для "логики более высокого прикладного уровня". Как-то так, без прочих нюансов.
Из "Шелехов В.И. Язык и технология автоматного программирования":
Код:
Класс невзаимодействующих  программ  или  класс  программ-функций.

Программа принадлежит этому классу, если она не взаимодействует с внешним окружением. Точнее,
если возможно перестроить программу таким образом, чтобы все операторы ввода данных
находились  в  начале  программы,  а  весь  вывод  собран  в  конце  программы,  то  такая
программа относится к классу невзаимодействующих программ. Программа обязана всегда
завершаться,  поскольку  бесконечно  работающая  и  невзаимодействующая  программа
бесполезна.  Следовательно,  программа  определяет  функцию,  вычисляющую  по  набору
входных данных (аргументов) некоторый набор результатов. Класс программ-функций, по
меньшей мере, содержит программы для задач дискретной и вычислительной математики.
Программа-функция реализует решение (алгоритм) некоторой математической задачи.
Решение  задачи  строится  на  базе  логики  решения  –  набора  математических  свойств
(теорем).  Программирование  –  это  реализация  логики  решения  в  конструкциях  языка
программирования.  Понимание  программы  реализуется  в  процессе  сопоставления  кода
программы с логикой решения. В качестве иллюстрации рассмотрим логику решения для
простейшей программы умножения натуральных чисел a и b через операцию сложения:
      a * b = b + (a - 1) * b,   0 * b = 0 .                        (1)
Ниже  приведены  логическая,  функциональная  и  императивная  программы,  являющиеся
реализациями логики решения (1).
      0 * b -> 0;  a * b -> b + (a – 1) * b                         (2)
      nat mult(nat a, b) { if (a = 0) 0 else b + mult(a – 1, b) }   (3)
      nat c = 0; while (a != 0) { c = c + b; a = a – 1 }            (4)
Различия логической программы  (2)  и  логики  (1)  чисто  синтаксические.  Фактически  они
тождественны. Функциональная программа (2) и логика (1) отличаются. Однако они также
тождественны – программа (2) легко транслируется в логику (1). Императивная программа
(4)  также  построена  из  логики  (1),  однако  понять  ее  и  установить  тождественность  с
логикой (1), – нетривиальная задача из-за трудности понимания циклов типа while [1].

-----------
[1]: Косвенным подтверждением является чрезвычайная трудность  автоматического построения инвариантов циклов

Насчёт циклов while выше в теме была статейка по поводу (однако там прежде всего тематика оценки завершимости). В "предикатном" программировании (мат. спецификациях) вместо циклов рекурсивные функции, с пред- и постусловием, а также с оценкой рекурсии. И ключевое в той технологии -- некая "реабилитация" goto, но в особой форме, которая связана с понятием управляющего состояния в автоматах:
Вложение:
goto.png
goto.png [ 29.35 КБ | Просмотров: 1288 ]

Однако управляющее состояние представляется в целом шире:
Код:
Гиперфункции.

Рассмотрим типичное решение задачи: взять второй элемент списка s и
обработать его программой B; если второго элемента нет, запустить программу D.
    Elem2(s: e, exists); if (exists) B(e…) else D(…);        (5)   
Программа Elem2 на языке P:
    pred Elem2(list(int) s: int e, bool exists )
    {  if (s = nil \/ s.cdr = nil)   exsts = false
      else   { e = s.cdr.car || exists = true }
    } post exists = (s <> nil & s.cdr <> nil) & (exists => e = s.cdr.car);
Использование логической переменной exists для реализации ветвления в (5) – плохое
решение,  загромождающее  и  усложняющее  программу.  Золотое  правило
программирования [2] состоит  в  том,  чтобы  не  использовать  логических  переменных  для
реализации  ветвления  в  программе [3].  Правильным  решением  является  следующая
гиперфункция для Elem2:
    hyper Elem2(list (int) s : int e #1: #2 ) 
    pre 1: s <> nil & s.cdr <> nil 
    {  if (s = nil \/ s.cdr = nil) #2 
       else   { e = s.cdr.car;   #1 } 
    } post 1: e = s.cdr.car;
Гиперфункция Elem2 имеет две ветви результатов: первая ветвь включает переменную e, а
вторая ветвь не имеет результатов – она пуста. Метки 1 и 2 – дополнительные параметры,
обозначающие два различных выхода гиперфункции. Спецификация гиперфункции состоит
из двух частей. Утверждение после “pre 1:” есть предусловие первой ветви; предусловие
второй ветви – просто отрицание предусловия первой ветви. Утверждение после “post 1:”
есть постусловие для первой ветви. Фрагмент (5) заменяется следующим:
    Elem2(s: e #L1: #L2)  case L1: B(e…) case L2: D(…);
Исполнение вызова гиперфункции завершается переходом либо по метке L1, либо по метке
L2.  Операторы  перехода  #L1  и  #L2  внутри  вызова  гиперфункции  явным  образом
фиксируют  точки  передачи  управления  в  отличие  от  вызова  вида  Elem2(s, e, L1, L2)  на
языке  типа  Алгол-60, где  переходы по  меткам  L1 и  L2  синтаксически не  выделены  и их
можно не заметить. Эта одна из причин, почему оператор перехода goto L1 записывается в
виде #L1.

--------------------
[2] Геннадий Кожухин, разработчик транслятора АЛЬФА, собирал золотые правила программирования в 1960-х гг.

[3] Это  противоречит  принципу  структурного  программирования,  поскольку  структурирование  произвольной
программы  в  соответствии  с  теоремой  Боэма  и  Джакопини  реализуется  с  использований  дополнительных
логических переменных

(в "аргументах" функций двоеточие ":" отделяет вход от выхода, выходов может быть несколько. Оператор "||" -- параллельная композиция вычислений). В общем, стиль моделирования направлен на определение управляющих состояний. И тогда, к примеру, вместо "классических" дополнительных проверок после цикла while как на рисунке "эквивалентная программа" выше ("стандартная обработка окончания цикла") после исполнения функции (возможно рекурсивной) сразу выполняется переход в необходимое состояние, с проверенными данными и условиями (и тогда программные структуры как бы приобретают истинный "структурный" вид. В рамках "императивщины" подобные переходы после while-ов и пр. должны выполнять и компиляторы с мощным dataflow-анализом, не делая лишних проверок при нормальных "чистых" предикатах).
В частности для циклов в виде рекурсий в итоге имеется контроль границ (оценка рекурсии через спецпредикаты) и имеется анализ управленческих состояний.
Имеются и "циклы Дейкстры"-"автоматы" аля:
Код:
process atFloor( : #idle  : #start) {
    open -> openDoor(), set t, opened;
    opened, closeButton() or t >= Tdoor -> closeDoor(), close;
    close, closedDoor() -> decisionClosed( : #idle  : #start);
    close, blockedDoor() -> open;
}

где:
- находясь в управляющем состоянии "open" выполняются "openDoor(), set t" и выполняется переход в состояние "opened";
- в состоянии "opened" при завершении работы closeButton() или при возникновении "t >= Tdoor" выполняется "closeDoor()", и переходим в состояние "close" и т.д.
Функция "decisionClosed()" возвращает два управляющих состояния, которые "улетают" наружу функции-процесса "atFloor" и её работа прекращается.
Кстати, именно такие ограниченные "линейные" формы "циклов Дейкстры" или всякого "паттерн-матчинга" удобны, почти что как в оригинале -- по мотивам Prolog/Datalog-а (откуда все эти "матчинги" растащили по IT). Т.е. когда возникает лес вложенных блоков по условиям -- не то пальто совсем.


Короче говоря, в стандартах безопасности, видимо, придерживаются методики некоей условно "управленческой дисциплины". Игнорировать не следует, как и не отбрасывать и "доказательство для человеков по-простому". В самом деле, как раз примерчик умножения натуральных чисел в цитате выше может быть показателен в том смысле, что иногда требуются математические/логические или функциональные формы/спецификации для того, чтобы понять императивщину. Но также может быть и наоборот -- императивщина может вдолбить понимание происходящего.

Изложения выше есть уточнение к тезисам в этой ветке насчёт соотношения "доказательного программирования" и стандартов безопасности.
Кстати, стандартизация возможна и для "лямбд":
https://forum.oberoncore.ru/viewtopic.php?f=152&t=6049&start=20#p103144


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

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

Да, и компилятор должен следить за чистотой функциональных типов для "лямбд"/указателей на функции в рамках "command/query separation principle", когда функция используется в условиях.


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

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


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

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


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

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


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

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