Pull to refresh
-3
0
Send message
ничего абсолютно обязательного быть не может, но какой то критерий конечно важнее
А не использовать ли нам «плечи титанов»?
Например, «список некоторых ограничений, вводимых SPARK» для того, что бы мы могли применять инструментарий формальной верификации:

  1. Все выражения (в том числе вызовы функций) не производят побочных эффектов. Хотя функции в Ада 2012 могут иметь параметры с режимом in out и out, в SPARK это запрещено. Функции не могут изменять глобальные переменные. Эти ограничения помогают гарантировать, что компилятор волен выбирать любой порядок вычисления выражений и подчеркивают различие между процедурами, чья задача изменять состояние системы, и функциями, которые лишь анализируют это состояние.
  2. Совмещение имен (aliasing) запрещается. Например, нельзя передавать в процедуру глобальный объект при помощи out или in out параметр, если она обращается к нему напрямую. Это ограничение делает результат работы более прозрачным и позволяет убедиться, что компилятор волен выбрать любой способ передачи параметра (по значению или по ссылке).
  3. Инструкция goto запрещена. Это ограничение облегчает статический анализ.
  4. Использование контролируемых типов запрещено. Контролируемые типы приводят к неявным вызовам подпрограмм, генерируемых компилятором. Отсутствие исходного кода для этих конструкций затрудняет использование формальных методов.

Отсутствие рекурсии — необязательное требование? ( ADA )
Аналогично — сборка мусора? ( Active Oberon )

Итого: стоит добавить в список Modula-3
( да и Modula-2 стандарта ISO )
Всему виной дополнительным требования по загрузке компьютера на уровне 80% по мощности (хотя 100% загрузка бортового компьютера РН Ариан, в принципе тоже норма), из-за которых пришлось вводить ограничения на проверку параметров в коде. Плюс, грубая ошибка в использовании принципа «повторноиспользуемости кода», при отсутствии тестирования интеграции в условиях новых входных данных.


Да, согласен

P.S.

Оставлю здесь фрагмент с source code

According to a presentation by Jean-Jacques Levy (who was part of the
team who searched for the source of the problem), the actual source code
in Ada that caused the problem was as follows.
-- Vertical velocity bias as measured by sensor

L_M_BV_32 := TBD.T_ENTIER_32S ((1.0/C_M_LSB_BV) * G_M_INFO_DERIVE(T_ALG.E_BV));

-- Check, if measured vertical velocity bias ban be 
-- converted to a 16 bit int. If so, then convert

if L_M_BV_32 > 32767 then
    P_M_DERIVE(T_ALG.E_BV) := 16#7FFF#;
elsif L_M_BV_32 < -32768 then
    P_M_DERIVE(T_ALG.E_BV) := 16#8000#;
else
    P_M_DERIVE(T_ALG.E_BV) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BV_32));
end if;

-- Horizontal velocity bias as measured by sensor -- is converted to a 16 bit int without checking P_M_DERIVE

P_M_DERIVE(T_ALG.E_BH) := UC_16S_EN_16NS (TDB.T_ENTIER_16S ((1.0/C_M_LSB_BH) * G_M_INFO_DERIVE(T_ALG.E_BH)));

The last line (shown here as two lines of text) caused the overflow,
where the conversion from 64 bits to 16 bits unsigned is not protected.
The code before is protected by testing before the assignment if the
number is too big.

The correct code would have been:
L_M_BV_32 := TBD.T_ENTIER_32S ((1.0/C_M_LSB_BV) * G_M_INFO_DERIVE(T_ALG.E_BV));

if L_M_BV_32 > 32767 then
    P_M_DERIVE(T_ALG.E_BV) := 16#7FFF#;
elsif L_M_BV_32 < -32768 then
    P_M_DERIVE(T_ALG.E_BV) := 16#8000#;
else
    P_M_DERIVE(T_ALG.E_BV) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BV_32));
end if;

L_M_BH_32 := TBD.T_ENTIER_32S ((1.0/C_M_LSB_BH) * G_M_INFO_DERIVE(T_ALG.E_BH));

if L_M_BH_32 > 32767 then
    P_M_DERIVE(T_ALG.E_BH) := 16#7FFF#;
elsif L_M_BH_32 < -32768 then
    P_M_DERIVE(T_ALG.E_BH) := 16#8000#;
else
    P_M_DERIVE(T_ALG.E_BH) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BH_32));
end if;


in other words, the same overflow check should have been present for the horizontal part of the calculation (E_BH) as was already present for the vertical part of the calculation (E_BV).

See diff with correct code:

--- LIRE_DERIVE.ads 000	Tue Jun 04 12:00:00 1996
+++ LIRE_DERIVE.ads	Fri Jan 29 13:50:00 2010
@@ -3,10 +3,17 @@
 if L_M_BV_32 > 32767 then
     P_M_DERIVE(T_ALG.E_BV) := 16#7FFF#;
 elsif L_M_BV_32 < -32768 then
     P_M_DERIVE(T_ALG.E_BV) := 16#8000#;
 else
     P_M_DERIVE(T_ALG.E_BV) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BV_32));
 end if;
 
-P_M_DERIVE(T_ALG.E_BH) := 
-  UC_16S_EN_16NS (TDB.T_ENTIER_16S ((1.0/C_M_LSB_BH) * G_M_INFO_DERIVE(T_ALG.E_BH)));
+L_M_BH_32 := TBD.T_ENTIER_32S ((1.0/C_M_LSB_BH) * G_M_INFO_DERIVE(T_ALG.E_BH));
+
+if L_M_BH_32 > 32767 then
+    P_M_DERIVE(T_ALG.E_BH) := 16#7FFF#;
+elsif L_M_BH_32 < -32768 then
+    P_M_DERIVE(T_ALG.E_BH) := 16#8000#;
+else
+    P_M_DERIVE(T_ALG.E_BH) := UC_16S_EN_16NS(TDB.T_ENTIER_16S(L_M_BH_32));
+end if;

основной заслугой (Н.Вирта) так и останется то, что в далёкие 70-е он придал верный импульс Алголу-60, создав Паскаль.
Я бы поставил на первое место Modula-2:
решение проблемы блоков BEGIN END в IF ( ELSIF), циклах;
приход Алголов в системное программирование и т.д.

Уточню, что я имел в виду: Вирт всегда был и остаётся сторонником экстремальной простоты. Сравните два пути развития Паскаля. Первый — по Вирту: Паскаль — Модула-2 — Оберон. Второй — по Borland: Паскаль — Турбо-Паскаль — Дельфи. Первый путь — путь упрощения, второй — путь усложнения. Индустрия однозначно предпочла второй путь
Во-первых сложно подсчитать объективно: «допинг» применяли обе стороны — Н.Вирт «выкидывал» цикл FOR и беззнаковые целые, его ученики-коммерсанты придумывали вместо RECORD с указателями на процедуры новые ключевое слово OBJECT

Во-вторых владельцы Delphi не смогли ( скорее, решили съэкономить) и просто лицензировали(?) разработки комады FPC для x64.

Т.е. путь усложнения имеет и отрицательные стороны.

Ну и финальный аккорд:

Во времена холодной войны ( с этапами оттепелей а-яля «Союз-Апполон») обе стороны
очень внимательно отслеживали состояние дел «по ту сторону окена».

Не только аэродинамику советских мини-челноков 60-70x, но и системы управления.

В частности, Э.Дейкстра ( если читать оригнал) говорил не о запрете BASIC в средних школах. Речь шла о Сибирском отделении Академии Наук СССР.

Теперь внимание: Н.Вирт был зван и тепло принят в Новосибирске.
Его ученик бизнесмен-саксофонист «срубивший бабла» и ушедший на пенсион раньше своего технологичекского гуру — я как-то сомневаюсь

Не став развивать Borland Modula-2 ( был для CP/M) и предоставив бороться не компиляторам, а благим пожеланиям от MISRA, с «парными фигурными скобочками»
выше упомянутый бизнесмен de-facto соучастник Тойота скандала с анти-тормозами в легковых автомобилях.
Однако настоящая трудность, специфичная для Паскаля, подстерегала совсем в другом месте — в работе с вложенными процедурами.
Кстати, в Clarion изящно обошли Вашу проблему с необходимостью стека фреймов(?), работы с ним с помощью регистра BX(?) и т.п. Просто вложенные процедуры сделаны без параметров и без собственных локальных переменных.

А уж во чтобы превратилась структура программы без этих routines я просто боюсь представить: их штук 20-40 в темплайте для генерации исходного кода для процедур отображения на экране файла базы данных в виде таблицы и в другом template для построения reports их не меньше.

Дело в мультипликации: файлов БД при реляционной схеме даже для относительно простого ПО требуется несколько десятков, для каждого файла нужны минимум по одной процедуре указанных выше темплейтов ( а обычно не одной, а несколько) и ещё по одной процедуре основанной на темплайте Forms.
вложенные процедуры не слишком нужны.

Как известно, практика критерий истины.

Буквально на днях видел вложенные процедуры в исходном коде, если не самого компилятора Modula-3, то в коде стандартной библиотеки.
Выглядело органично даже в 20-тистрочной подпрограмме.

Настолько же естественным путём вложенные процедуры потребуются при доказательном программировании ( см. ADA SPARK, Frama-C) из практических соображений, так как выход из середины циклов становится недопустим.
вложенные процедуры не слишком нужны. Да и, откровенно говоря, они не самый лучший способ структурирования кода.
Есть и другая точка зрения: как ни странно, именно вложенные процедуры считают способом построения иерархической структуры программы. И наоборот, модули обеспечивают только плоскую структуру. Самое удивительное, что это преподносилось, как один из немногих плюсов наследников Pascal. Ещё более удивительно, что автор этого построения занимается «не Паскалем».
Имеется в виду, что написание системного ПО на чистом Паскале 70-х проблематично без ассемблерных вставок. См. здесь же на чём написан, например Turbo Pascal.

Начиная с Modula ( т.е. ещё до Modula-2 на котором была написана AS/400, первоначально ) был взят курс на создание модуля SYSTEM с функциями ADDRESS(), SIZE() и т.п.

Как итог, на Алголах стало возможно программировать и ОС, и прикладное ПО.
для вложения процедур у Вирта была и вполне прагматическая причина — сведение косвенной рекурсии к прямой
Охотно допускаю ( хотя и верится с трудом — уже на 1989 опережающие описания процедур были «всегда» т.е. в «древних» 70-х «уже были») что ради рекурсии.

Рекурсия — фирменная «фишка» Алголов и предмет законной гордости европейской школы.

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

( Перечитываю переводную классику издательства «Мир» )
У Oberon много диалектов(?). Мне рассказывали про отсутствие беззнаковых, как о «фирменной особенности».

Если, как и цикл FOR, вернули в современные Oberon-ы, то я только «за»
Оберон так и остался… академическим проектом.
На нём разрабатывают промышленное ПО. Вы, скорее всего, ещё не успели прочитать статьи от Kemet?

Если не нравятся спорные моменты, как то, отсутствие беззнаковых целых, то давайте посмотрим на современные Modula-2 ( их разработчики, кстати, называют их Modula-2(Oberon-2), так как синтаксис объекто-ориентированного программирования в стиле Н.Вирта).

Давайте возьмём Modula-3 ( проект, кстати, «скорее жив чем мёртв», сегодня было многообещающее, в практическом плане, сообщение в списке рассылки).
В тот день, когда я перешёл с 32-битной Windows XP на 64-битную Windows 7 без виртуальной машины DOS, я мысленно похоронил свой проект.

Реинкарнируйте в DosBOX
Однако настоящая трудность, специфичная для Паскаля, подстерегала совсем в другом месте — в работе с вложенными процедурами. Может возникнуть совершенно невинная надобность обратиться к локальной переменной внешней процедуры из внутренней. Однако во внутренней процедуре нет адреса стекового кадра внешней процедуры — внутренняя процедура не знает, от чего отсчитывать адрес искомой переменной. Этот адрес приходится всякий раз передавать во внутреннюю процедуру через дополнительный скрытый параметр. Подозреваю, что именно это осложнение заставило разработчиков C вовсе отказаться от вложения функций. Однако в Паскале они есть, и с этим приходится считаться.

Вот что получается: Н.Вирт ( и Вы) смогли осилить, а те кто якобы не «утратили всякую связь с реалиями ИТ» — как в анекдоте N13 «не смогли, или не захотели»

А потом «почему-то» новейшие автомобили при нажатии на педаль тормоза...

P.S. см. Глава 5. Компиляторы
в книге
Л. Бек Введение в системное программирование
Заголовок спойлера
System Software
An introduction to systems programming
Leland L. Beck
San Diego State University
Addison-Wesley Publishing Company Reading, Massachusetts Menlo Park, California Don Mills, Ontario Wokingham, England Amsterdam Sydney Singapore Tokyo Mexico City Bogota Santiago San Juan

Л. Бек
Введение в системное программирование
Перевод с английского Н.А. Богомолова, В.М. Вязовского и С.Е. Морковина под редакцией Л.Н. Королева
Москва «Мир» 1988

ББК 32.973
Б42
УДК 681.142

Бек Л. Введение в системное программирование: Перевод с английского. — М.: Мир, 1988. — 448 с., ил.
ISBN 5-03-000011-9
Монография учебного характера, написанная американским специалистом. В ней изложены все основные компоненты системного программного обеспечения. Особое внимание уделено их взаимосвязи с архитектурой вычислительных комплексов. Конкретные реализации компонентов обсуждаются на примере трех современных вычислительных систем: IBM/370, VAX, CYBER.
Для системных программистов, аспирантов, студентов вузов.

ББК 32.973

КРАТКОЕ ОГЛАВЛЕНИЕ:
От редактора перевода (5).
Предисловие (7).
Глава 1. Основные понятия (11).
Глава 2. Ассемблеры (38).
Глава 3. Загрузчики и программы связывания (122).
Глава 4. Макропроцессоры (178).
Глава 5. Компиляторы (222).
Глава 6. Операционные системы (312).
Глава 7. Другие компоненты системного программного обеспечения (399).
Приложения (430).
Литература (437).
Предметный указатель (440).

Редакция литературы по математическим наукам
Учебное издание
Леланд Л. Бек
ВВЕДЕНИЕ В СИСТЕМНОЕ ПРОГРАММИРОВАНИЕ

P.P.S. А лучше — полностью прочтите
P.P.P.S.
Я не профессиональный программист
Я понимаю, что не все учились по специальности 22.04, но и я книгу нашел в библиотеке Заводского района

( И критика автора языка Modula-2 — в статье про его ранний язык ...)
«Питон — это бейсик сегодня!» :)
И «в следующие 40 лет он» принесёт «столько же» пользы/вреда как и предтеча BASIC «в предыдущие 40»? или нет?

( Это полу-цитата переводной статьи-главы из бело-зеленой 6мм. книги
см. здесь же в комментариях «координаты»)
... ни pascal, ни... никого ничему интересному не учат.
Разве что один учит, что begin и end ходят парами
За выживший в «эволюционной борьбе» begin можете сказать спасибо вполне конкретному ( с какого-то момента) бизнесмену. Почти дословно: «И зачем нам Borland Modula-2, когда и то что есть продаётся?»

Так что учит, ещё как учит... Скорее, правда, учит «жизни, как она есть»
(
100 строк — это немало...
В 100 строк вмещается, например, расчет отпуска или больничного
Из них 25 встроенного языка,
правда, цикл расчета среднемесячного дохода(?) на Clarion
)

Кстати, об обучении тех кто ходит в 9-11 классы ( и всех желающих с 4 класса),
есть предложение обсудить бело-зеленую книгу 6мм. толщиной:

Простое и сложное в программировании
Серия: Кибернетика — неограниченные возможности и возможные ограничения
ISBN: 5-02-006595-1
Переплет: мягкий;

Простое и сложное в программировании [Текст] / Академия наук СССР; авт. предисл. Е. П. Велихов. — М.: Наука, 1988. — 169, [5] с.: ил. — ISBN 5-02-006595-1: Б. ц.

Вишняков, Юрий Саввич
канд. физ.-мат. наук
Грюнталь, Андрей Игоревич
канд. физ.-мат. наук
А. И. Грюнталь
Кольцова, Анастасия Андриановна
канд. техн. наук
А. А. Кольцова
Пачков, Степан Александрович
С. А. Пачков
Семенов, Алексей Львович
д-р физ.-мат. наук
А. Л. Семенов

Приведу часть оглавления вне спойлера ( по нему проще вспомнить книгу тем кто её читал, а остальным понять о чём она):
...
Глава 2. Коза, капуста и другие с точки зрения программиста
Глава 3. Путник снова в лабиринте
Глава 4. Доказательства в программировании
Глава 5. Алгоритм Евклида
Глава 6. Кто тяжелее, или Нижние и верхние оценки для задачи сортировки
Глава 7. Сколько веревочке ни виться, или Почему программы кончают работу
Глава 8. Снова о сортировке
Глава 9. Могут ли восемь ферзей не бить друг друга, или Обход дерева
Глава 10. Можно ли поднять себя за волосы, или Рекурсия
Глава 11. От рекурсивного определения к программе
Глава 12. Ханойские башни
...
Глава 14. Переборные задачи
Глава 15. Игры, игры, игры
Глава 16. Снова об играх
Глава 17. Гениальный режиссер и его жертва
...
Глава 20. Игра в животных, или Искусственный интеллект
Глава 21. Программистские басни
Глава 22. Компьютеры и общество
...
Начиная с 17 главы ( или чуть раньше) — «но и для их родителей» и(или) «про жизнь», рекомендую

Например, что из неё пригодится «и в дальнейшем в жизни — в университете, в работе»? Актуальность?
... то, что компиляция ловят какие-то ошибки, не так важно — все равно вы должны тщательно протестировать свою (небольшую) программу, и все равно вы такие ошибки выловите.
Не все с этим согласны, и даже развивают инструментарий формальной верификации (доказательства корректности работы ПО с помощью математических методов):

SPARK — подмножество языка Ада
Многозадачность, в ее полном варианте, имеет очень сложную семантику исполнения. Но при использовании Ravenscar профиля она все же подлежит формальному анализу.
...
Важной возможностью... анализа является обнаружение неинициализированных переменных.
...
Далее, существуют формальные процессы верификации, касающиеся доказательств:
•Формальная верификация свойств надежности (т.е. гарантия отсутствия возбуждения предопределенных исключений);
•Формальная верификация функциональных свойств, основанных на контрактах, таких как пред-условия и пост-условия.

В случае с функциональными свойствами, которые кроме пред- и пост-условий включают в себя инварианты циклов и утверждения, касающиеся типов, анализатор генерирует предположения, которые необходимо доказать для гарантирования корректности программы.
...
За последние годы произошел значительный прогресс в области автоматического доказательства теорем, благодаря чему GNATprove способен автоматически исполнять множество условий верификации.
Это всё прикольно до той поры пока не надо будет запустить VMWare
Уже было писал об этом:
VMware всё равно придётся решать проблему VMware Workstation in Hyper-V.

Обучение отключению Credential Guard/Device Guard ( Turn on Virtualization Based Security ) в Article 2146361 вызывает «сложные эмоции» у заботящихся о защите от «утечки паролей»

В качестве выхода из ситуации, было бы неплохо программистам VMWare освоить API WHPX ( Windows Hypervisor Platform )
VirtualBox 6.0 released
•Added support for using Hyper-V as the fallback execution core on Windows host, to avoid inability to run VMs at the price of reduced performance
Как изящно выразился rseiler на форуме VBox:
I've since seen the one new line there mentioning Hyper-V, but it's a bit cryptic.
В частности:
Аналогично как и в Android emulator ( точнее как в QEMU ) используется API WHPX ( Windows Hypervisor Platform )?
аптаймом по шесть-восемь месяцев
проводить эксперимент, отложив обновы на те самые полгода.
Надо сделать кластер и обновлять его ноды одну за другой.
А вот создавать питательный сиропчик для вирусов и хакеров «экспериментами» — ни к чему

P.S. Рекорды uptime — устаналиваем по времени непрерывной работы сервиса в целом
( Есть предложения отвлечься на ещё более высокие материи,
чем ITIL + PCI-DSS, инженерная культура и т.п.)
Не совсем понятно: вы за Шарикова? или за Преображенского?

Information

Rating
Does not participate
Registered
Activity