Права доступа к переменным

Со времени предыдущих историй прошло всего-то лет пять, а как стал меняться компьютерный мир. В том числе, и в НПО. В отделах стали появляться персоналки: у кого IBM-PC/XT, у кого «Правец», у кого ЕС-1840. Число пользователей БЭСМ и даже ЕС и СМ-4 стало асимптотически приближаться к нулю. На фоне новых возможностей все их «фишки» сразу побледнели. Например, смешно, что ещё недавно какая-нибудь замена терминала VT-340 на VT-52100 c памятью на 5 страниц, позволяющей вводить текст ещё до включения БЭСМ, казалась важной.

            Расстаться со старыми заделами и навыками психологически мне было даже проще, чем многим, поскольку после двухлетнего отсутствия я вернулся на работу уже в другой отдел и, так сказать, сразу отрекся от старого мира и отряхнул его прах со своих ног. Впрочем, последние годы работа с БЭСМ через диалоговую программу «Пульт» (разработка МГУ) как раз очень напоминала работу за первыми персоналками и поэтому переход был несложным. А вот задачи стали другие. Отдел занимался разработкой ПО системы управления «Энергия-Буран». Точнее, отдел занимался комплексацией, верификацией, взаимодействием с наземным ПО и т.п., а собственно разработкой занималось сразу несколько отделов. Я впервые принимал участие в проекте, где были заняты десятки программистов. Язык программирования — ПРОЛ-2 разработки ИПМ АН СССР.

            Вообще-то, девичья фамилия этого языка была «Пролог-Ц» от ПРОграммирования ЛОГики. Но поскольку в то время на слуху был японский Пролог с его транспьютерами, вероятно разработчикам надоело отвечать на вопросы о применении транспьютеров в «Буране», поэтому вторая версия языка вышла под таким скромным и безликим именем.

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

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

            Сказано-сделано. Часть транслятора была написана на ассемблере и поэтому летал он ласточкой.

            В то время было модно извлекать из внутреннего динамика персоналки разные звуки. Ребята из моего бывшего отдела даже спаяли простой АЦП на параллельный разъем и через микрофон от древней «Яузы-5» мы записали ряд сигналов и фраз. Например, при отсутствии замечаний проверочный транслятор бесцветным голосом произносил половинку подходящего к случаю т.н. «заходеризма» (т.е. афоризма Б. Заходера): «если взглянуть формально, все обстоит нормально».

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

            Для повышения надежности в языке ПРОЛ-2 описание нелокальных переменных должно было включать и права доступа в виде списка имен процедур, которым разрешается к этой переменной обращаться.

            Так вот, проверочный транслятор выдал большое число сообщений, что идет обращение к переменным без права доступа. Отдельческое начальство поморщилось: дескать, уж такую несложную ветку в проверочном трансляторе можно было бы сделать с первого раза и без ляпов. Штатный транслятор давно отлажен и многократно проверен. Таких нарушений он бы просто не пропустил. Откуда в проверенных программах взялись сотни ошибок доступа?

            Но разбирательство показало, что таки-да, в штатном трансляторе помарка. Вероятно, она проникла в транслятор, когда выяснилось, что ресурсов одной БЦВМ не хватает и приняли решение поставить в «Буране» две машины, разделив ПО между ними. Транслятор подправили для двух ЭВМ, но он перестал проверять доступ переменной из процедуры на соседней БЦВМ (или, наоборот, на той же, я уже не помню). В общем, выключилась одна из проверок.

            После выяснения этого даже было совещание. Не столько на тему помарки в трансляторе, сколько на тему технологи разработки. Ведь рассчитывали на что? Что разработчики проанализируют сферу действия каждой переменной и явно и осмысленно укажут множество объектов, которые могут эту переменную читать/писать. А что получилось в реальности? Разработчики чихали на анализ и совали свои модули в транслятор. Ругнулся он по поводу прав — так и быть допишем список, не ругнулся — и так сойдет. В текстах даже нашли издевательские описания нелокальных переменных с пустыми списками, т.е. по правилам языка к ним вообще никто не мог обращаться. И при этом все работало нормально и казалось, что защита от порчи «чужих» данных хорошо обеспечена.

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

            А что, разве при отработке не было случаев, когда один процесс портил переменную другому процессу? Конечно, были. Только во всех этих случаях как раз с доступом все было хорошо.

            С тех пор прошло уже десятка три лет. Программирование и теоретически и практически ушло далеко вперед и добилось больших успехов.

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

Автор: Д.Ю.Караваев. 10.02.2017

Опубликовано: 2018.08.26, последняя правка: 2019.01.28    20:43

✅  2018/10/21 13:50, Comdiv          #0 

✅  2018/10/21 20:13, Автор сайта          #1 

✅  2018/10/22 15:13, Comdiv          #2 

✅  2018/12/18 18:33, Автор сайта          #3 

• Отладка. Дотошно проверяем каждый бит и байт. Работа и труд всё перетрут. Но при росте объёма и сложности программы трудоёмкость отладки растёт не в линейной прогрессии. Во-вторых, полная отладка марсохода возможна только на Марсе — имитация внешней среды не всегда возможна.
• Других альтернатив не вижу. Не кропить же написанный код святой водой?

✅  2018/12/18 20:28, Comdiv          #4 

✅  2018/12/19 18:34, Автор сайта          #5 

✅  2018/12/19 23:46, Comdiv          #6 

Но даже правильное задание и 100-процентное его выполнение могут столкнуться с неудачей.

✅  2018/12/20 13:58, Автор сайта          #7 

✅  2018/12/20 14:14, Бурановский дедушка          #8 

прочих, ежедневно отливаемых «серебряных пулях»

31 ноября

✅  2018/12/20 14:21, MihalNik          #9 

Да никому и в голову не могло прийти, что в ноябре 31 день. Любая академия наук утвердила бы ТЗ на тип данных «дата».

✅  2018/12/21 18:34, Автор сайта          #10 

✅  2018/12/22 02:20, MihalNik          #11 

✅  2018/12/22 20:36, Автор сайта          #12 

✅  2018/12/23 05:04, MihalNik          #13 

Как бы он помог в случае с 31 ноября? «Дракон» — это про алгоритмы. А тип «дата» — это про данные.

✅  2018/12/28 22:07, Автор сайта          #14 

Форматы данных не задают алгоритмы... Формат данных не определяет алгоритмы, а выбирается исходя из них.

31 ноября — проблема в АЛГОРИТМЕ обработки данных.

если (полномочия текущего пользователя && разрешена запись неправильных данных)
   дата рождения = поле ввода даты рождения;

Вам дали посчитать площадь круга. Допустимая погрешность 0,01%. Вам дали формулу S=Pi*R^2 и сказали считать число Pi строго равным 3.

S приблизительная = 3 * радиус * радиус
S точная = Пи * радиус * радиус
относительная погрешность = (S точная - S приблизительная) / S приблизительная
относительная погрешность = (Пи - 3) / 3
относительная погрешность = (3.14159 - 3) / 3
относительная погрешность = 0.072 или 7.2%

✅  2019/01/02 02:58, rst256          #15 

✅  2019/01/02 14:32, Автор сайта          #16 

✅  2019/01/09 10:14, utkin          #17 

31 декабря 2011 года из Ростова-на-Дону вышел поезд, когда часы на вокзале показывали 23 часа, 00 минут, 00 секунд. Когда он пришёл в Донецк 1 января 2012 года, то часы на донецком вокзале показывали 01 час, 00 минут, 00 секунд. Вопрос: сколько секунд был в пути этот поезд?

Не знаю, как была решена проблема с 31 ноября.

✅  2019/01/10 11:41, Автор сайта          #18 

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

Так вот: ФП позволяет смотреть на программу, как на теорему в математике. И математически доказывать её правильность. Конкретно это означает следующее. Вот код Паскале, который считает сумму элементов массива:

s:=0;
   for i:=1 to n do s:=s+X[i];

Попробуйте доказать, что код считает сумму n элементов любого массива. Это будет непросто. А вот тот же код на Haskell:

sum [] = 0
sum (x:sx)=x+sum(xs)

Здесь все готово для того, чтобы доказать по индукции, что функция sum вычислит сумму элементов любого списка s конечной длины.

sum [] = 0
sum (x:sx)=x+sum(xs)

✅  2019/01/10 12:45, utkin          #19 

Спорить я с Вами не буду, хотя логика Ваших рассуждений небезупречна.

Дело в том, что так уж сложилось, что никто не требует доказательства правильности программы. Обычно ограничиваются парой тестов. Работает? Ну так что же вам ещё? Хотя понятно, что даже 1000 верных тестов не доказывает, что 1001-й тест будет верным.

Так вот: ФП позволяет смотреть на программу, как на теорему в математике. И математически доказывать её правильность.

Попробуйте доказать, что код считает сумму n элементов любого массива. Это будет непросто. А вот тот же код на Haskell:

Многие люди из нашего круга общения хотят написать компилятор Oberon-2, Lisp, C (с вариациями, с доработками). Но что-то никто не горит желанием написать свой Haskell, свою систему доказательного программирования. Увы.

И снова можно верить в доказательства.

✅  2019/01/11 11:58, Автор сайта          #20 

верификация и валидация ... не свойственна нашим производственным предприятиям

Само функциональное программирование тоже не без греха — есть же всякие там монады и прочие извращения.

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

Потому что очень высокий порог вхождения

Первая проблема — значимость не показана. Ещё один подарок от Евклида: «Дай вопрошающему грош, если он ищет выгоды, а не математики». Авторы начинают вводить определения, доказывать теоремы и творить прочую математику без объяснения зачем оно вообще нужно. Пример: учебник по математическому анализу от Фихтенгольца. Почитайте первую главу: «из школьного курса вы знаете про рациональные числа, но потребности математики понуждают нас ввести вещественные...» и понеслась. Какие потребности, какой математики, чем не устраивают рациональные — да пёс его знает. «Очевидно».

✅  2019/01/12 07:22, utkin          #21 

Общество позволяет государство проводить беззубую экономическую политику, поэтому интересы потребителей не защищены от произвола «as is» («как есть»). Люди платят деньги за ПО, но никак не защищены. Вот появятся требования по качеству — тогда и будет внимание к доказательству правильности программ.

Это угрожает Вашей непорочности? :)

А зачем переводить на особый математический язык? Может, лучше сделать такой язык, чтобы он был удобен, понятен, общедоступен и при этом «математичен», чтобы проводить формальные проверки? «Два в одном»?

Так его надо понижать. Во-первых, отказаться и сказать «это слишком сложно» никогда не поздно. Во-вторых, сложность связана, зачастую, лишь с плохим изложением материала.

Первая проблема — значимость не показана. Ещё один подарок от Евклида: «Дай вопрошающему грош, если он ищет выгоды, а не математики». Авторы начинают вводить определения, доказывать теоремы и творить прочую математику без объяснения зачем оно вообще нужно. Пример: учебник по математическому анализу от Фихтенгольца. Почитайте первую главу: «из школьного курса вы знаете про рациональные числа, но потребности математики понуждают нас ввести вещественные...» и понеслась. Какие потребности, какой математики, чем не устраивают рациональные — да пёс его знает. «Очевидно».

✅  2019/01/12 11:23, Автор сайта          #22 

✅  2019/01/14 07:23, utkin          #23 

И всё-таки, я думаю, стоит побороться за снижения порога вхождения. А вдруг родятся витагенные технологии в доказательном программировании?

plus = λx. λy. λs. λz. x s (y s z)

✅  2019/01/15 15:40, Автор сайта          #24 

✅  2019/01/16 07:18, utkin          #25 

Императивный код сложнее анализировать.

Я что-то не слышал о конкуренции форм записи среди математиков.

Просто нужно думать и придумывать.

✅  2019/01/16 15:36, Автор сайта          #26 

например, римские цифры и арабские цифры.

И всё? А языков программирования что-то около восьми тысяч. Это цифра, где-то озвученная несколько лет назад. Восемь тысяч форм записи! На три порядка больше, чем в математике. Просто математика сосредоточена на содержании, а не на форме. Просто перенос математики в язык программирования надо попытаться сделать с большим уважением к форме. С большим дружелюбием.

эра одиночек в гаражах уже прошла

Мои порывы не связаны с тем, что я бензина нанюхался.

целые кафедры функциональных языков в уважаемых институтах, которые думают, думают и никак не придумают.

Я несколько лет ломал голову над тем, как возвратить из функции объект переменной длины. В итоге нашёл решение, которое очень просто в реализации. А ведь сколько кафедр и институтов 70 лет ходило мимо, его не замечая. А теперь некоторые сотрудники РАН, которые в курсе, отдают должное. А Вы поищите в литературе, какие модели памяти знает наука — и моего новшества там не найдёте.

Конечно, нет никаких гарантий, что мне удастся что-то найти. Но я ведь и не претендую на ваше личное время. От Вас ничего не убудет.

На практике их использование приводит к жестким проблемам, о которых стараются не говорить. И Вы их тоже избегаете. Я Вам дам простой вопрос — как описать мир с побочными эффектами языком без побочных эффектов?

Как раз над этим я и думаю. Проблема не в том, что мне непонятны какие-то отдельные детали. Проблема в том, что общая картина не столь непонятна, сколь противоречива. Одни определения противоречат другим. Задавал вопросы на форумах, но меня начали подозревать в холиварах. Надо все противоречия грамотно изложить и снова попробовать.

✅  2019/01/17 14:05, utkin          #27 

И всё? А языков программирования что-то около восьми тысяч. Это цифра, где-то озвученная несколько лет назад. Восемь тысяч форм записи! На три порядка больше, чем в математике. Просто математика сосредоточена на содержании, а не на форме.

Просто перенос математики в язык программирования надо попытаться сделать с большим уважением к форме. С большим дружелюбием.

Мои порывы не связаны с тем, что я бензина нанюхался.

А ведь сколько кафедр и институтов 70 лет ходило мимо, его не замечая.

Но я ведь и не претендую на ваше личное время. От Вас ничего не убудет.

Проблема в том, что общая картина не столь непонятна, сколь противоречива.

✅  2019/01/17 17:43, Автор сайта          #28 

Я имел ввиду более приятные ассоциации

Значит это не такая важная проблема на фоне других проблем.

Убывает время, которое я трачу, читая Ваши выкладки ... сделка честная.

программа должна быть либо самой операционной системой, либо её главной частью ... смотрите на проблему под другим углом зрения

✅  2019/01/18 08:54, utkin          #29 

Да, настолько неважная, что в Haskell объекты по сей день создаются в «куче», хотя есть способы побыстрее.

Ничего подобного. Моего времени убывает больше, так нечестно.

У Вас очень оригинальный угол.

✅  2019/01/18 13:53, Автор сайта          #30 

✅  2019/01/18 14:23, MihalNik          #31 

В Хаскелле есть проблемы по важней. Первая — высокий порог вхождения. Вторая — пляски вокруг побочных эффектов.

По сути программа должна быть либо самой операционной системой, либо её главной частью и все проблемы решены. Вопрос только какой ценой.

✅  2019/01/18 14:48, MihalNik          #32 

Пляски вокруг побочных эффектов есть — это как раз в императивных языках. В Haskell — другие пляски, вокруг кода

Попробуйте доказать, что код считает сумму n элементов любого массива. Это будет непросто. А вот тот же код на Haskell
sum [] = 0
sum (x:sx)=x+sum(xs)

с доказанной правильностью («функция sum вычислит сумму элементов любого списка s конечной длины») я укажу на ошибку, из-за которой функция sum не всегда вычислит сумму не любого списка. Просто в этом коде на Haskell опять «сломалось» ТЗ и его надо подправить. И снова можно верить в доказательства.

var
s: LongInt;
e: Word;
A: array[1..1000] of Word;
procedure CalculateSum;
begin
  s:= 0;
  for e in A do s+= e;  
end;

✅  2019/01/18 15:59, Автор сайта          #33 

Укажите на ошибку

✅  2019/01/18 19:21, utkin          #34 

Понимаете, это не я хочу математику. Это она заставит нас преодолевать повышенный порог вхождения.

Резервов в развитии программирования немного, и ФП — один из них.

Пляски вокруг побочных эффектов есть — это как раз в императивных языках.

Тыкнуть случайно в хромобраузере андроида на смартах из коробки куда-нибудь не туда и уже устанавливаются неизвестные приложения/иконки, соответственно, закладки/дыры/управляемость под вопросом.

Указываю. Вышеприведённый пример имеет недостаток: он с большим доверием относится ко входным данным и не предполагает, что при суммировании возникнет переполнение. А где обработка переполнения? А нет её.

А вы исправьте так, чтобы обоих случаях был одинаковый тип и вставьте в код проверку ошибок. Тогда будет ясно, как ваш язык обрабатывает ошибки.

✅  2019/01/19 00:52, MihalNik          #35 

А вы исправьте так, чтобы обоих случаях был одинаковый тип и вставьте в код проверку ошибок.

var a,b,c: Byte;
begin
a:= (b+c) mod 256;
end;

if (a=b) c+= 1;

✅  2019/01/19 07:29, utkin          #36 

Указываю. Вышеприведённый пример имеет недостаток: он с большим доверием относится ко входным данным и не предполагает, что при суммировании возникнет переполнение. А где обработка переполнения? А нет её.

✅  2019/01/20 18:12, Автор сайта          #37 

Одинаковый тип — это и есть ошибка.

int operator+=(int& a1, int a2)

int operator+=(int& a1, short a2)

A: array[1..1000] of Word;

✅  2019/01/20 19:04, utkin          #38 

Ошибка, говорите? Да она в стандартах языков зафиксирована! В C++, например, вот так:

легко сломать, увеличив количество элементов в массиве.

✅  2019/01/21 11:53, Автор сайта          #39 

✅  2019/01/21 13:11, utkin          #40 

Современность работает над как можно большим контролем кода.

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

✅  2019/07/20 19:42, Александр Коновалов aka Маздайщик          #41 

sum [] = 0
sum (x:sx)=x+sum(xs)

Указываю. Вышеприведённый пример имеет недостаток: он с большим доверием относится ко входным данным и не предполагает, что при суммировании возникнет переполнение. А где обработка переполнения? А нет её.

Добавить свой отзыв

Написать автору можно на электронную почту
mail(аt)compiler.su