DRAKON.SU

Текущее время: Вторник, 19 Март, 2024 06:09

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




Начать новую тему Ответить на тему  [ Сообщений: 81 ]  На страницу Пред.  1, 2, 3, 4, 5  След.
Автор Сообщение
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Пятница, 10 Август, 2012 08:16 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Alexey_Donskoy писал(а):
...
Выводы:
1) если редактор не поддерживает транзакции редактирования, которые не могут быть завершены с нарушением синтаксиса - это плохой редактор;
2) если редактор поддерживает транзакции редактирования, которые обеспечивают прозрачное для пользователя сохранение (преобразование) семантики, это очень хороший редактор.

Вашу среду пока можно дисквалифицировать по п.1 - нарушить синтаксис легко простым перетаскиванием элементов.
Среда Тышова удовлетворяет п.1, но не п.2.

Может показаться, что п.1 среда Тышова тоже не выполняет, поскольку часто бывают глюки при перетаскивании линий - сбоит автоматическая разводка, приходится исправлять вручную. Однако синтаксис при этих глюках не нарушается!

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

Вопрос, поднятый Эдуардом (о переносе петли цикла), вообще говоря, относится к п.2.
Человек, желающий перенести петлю, может сделать это тремя путями:
а) внести куски кода в тело цикла (и/или вынести оттуда);
б) переместить петлю;
в) всё разобрать и собрать заново (как в Вашей среде со свободным рисованием) :wink:
...
Думаю, не совсем так - а) (с моими уточнениями) при свободном построении оказывается частным случаем б)... Впрочем, и при детерминированном можно "всё разобрать" - хотя бы раскидав по схемам-времянкам... или в многоместный карман, если таковой поддерживается...

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Пятница, 10 Август, 2012 11:04 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
Илья Ермаков писал(а):
Владимир Паронджанов писал(а):
Практическая ценность состоит в том, что управляющие операторы алгоритма, представленные в виде шампур-схемы оказываются безошибочными, гарантированно правильными.

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

А, например, методы Дейкстры или формальной верификации типа model-checking позволяют убедиться в том, что поведение программы соответствует спецификации требований.

Уважаемый Илья Евгеньевич!

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

Анализ метода Дейкстры, его оценка и перспективы.
Метод Дейкстры и язык ДРАКОН


План моего ответа.

Сначала я приведу большой отрывок из статьи о Дейкстре в журнале "Системный администратор". (Это ПУНКТ ПЕРВЫЙ).

Затем выделю из этого отрывка два-три абзаца, отчасти созвучные моим мыслям. (Это ПУНКТ ВТОРОЙ).

Затем дам оценку метода Дейкстры и его перспективам. (Это ПУНКТ ТРЕТИЙ).

Затем буду излагать преимущества языка ДРАКОН. (Это ПУНКТ ЧЕТВЕРТЫЙ и последующие).


Последний раз редактировалось Владимир Паронджанов Воскресенье, 12 Август, 2012 12:17, всего редактировалось 1 раз.

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Пятница, 10 Август, 2012 11:19 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
ПУНКТ ПЕРВЫЙ

http://samag.ru/uart/more/16

Эдсгер Вибе Дейкстра. Смиренный гений программирования

Автор: Алексей Вторников

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

В информатике мы все – дети Дейкстры
К. Апт «Портрет гения»

Цитата:
Эдсгер Вибе Дейкстра родился в Роттердаме (Нидерланды) в мае 1930 года в семье научных работников: отец будущего лауреата Тьюринговской премии был химиком, мать – математиком что, видимо, и предопределило выбор Дейкстры поступить на отделение математики и теоретической физики Лейденского университета. Еще учась в университете Дейкстра познакомился с первыми компьютерами и увлекся их программированием. Этому немало способствовало и то, что будучи еще студентом Дейкстра с 1952 года работал программистом в Математическом центре Амстердама. За год до окончания университета Дейкстра оказался перед дилеммой: продолжить научную карьеру по основной специальности – теоретической физике или все-таки продолжать заниматься программированием. Вот что рассказывал об этом он сам:
Цитата:
«... мне надо было сделать выбор – либо прекратить программировать и стать настоящим респектабельным теоретическим физиком, либо как-то формально завершить мое обучение теоретической физике с минимальными усилиями и стать ... кем же? Программистом? Но разве это респектабельная профессия? В конце-концов, что такое программирование? В чем должен был состоять тот солидный объем знаний, который позволил бы считать программирование научной дисциплиной?»

По счастью Дейкстра обратился со своими сомнениями к своему научному руководителю Адриану ван Вейнгаардену у которого хватило житейской мудрости и научной проницательности чтобы убедить молодого физика стать профессиональным программистом.

Трудно сказать – много ли потеряла теоретическая физика оставшись без Дейкстры; учитывая его уникальную интеллектуальную мощь, которая очень вскоре проявилась в полную силу, рискну предположить, что физика потеряла немало. Но случилось то, что случилось и начиная с этого времени талант и энергия Э.Дейкстры принадлежали новой дисциплине – информатике.

Надо сказать, что Дейкстра действительно рисковал выбирая столь экзотическую в те времена профессию. Программистов было мало, а компьютеры и вовсе исчислялись двумя-тремя десятками. Будущее информатики как науки было туманным – многие рассматривали (и надо признать не без оснований) информатику как ветвь прикладной математики.

......................................................................

Заканчивая этот раздел, я не могу не удержаться, чтобы не процитировать самое, пожалуй, знаменитое высказывание Эдсгера Дейкстры: «Тестирование программ может служить для доказательства наличия ошибок, но никогда не докажет их отсутствия». И тут самое время перейти к главному труду Эдсгера Дейкстры – его книге «Дисциплина программирования».

Книга

Если бы в русском языке существовала категория артиклей, то я непременно поставил перед названием этого раздела определенный артикль (ср. англ. «The Book»), чтобы подчеркнуть уникальное значение книги Э.Дейкстры «Дисциплина программирования». Книга появилась в 1976 году и через два года была переведена и опубликована на русском языке в серии «Математическое обеспечение ЭВМ». Аналогов «Дисциплине программирования» нет – эта книга уникальна как по замыслу, так и по стилю. «Дисциплина программирования» относится к тем немногим (исчисляющимся двумя-тремя десятками) книгам, определившим столбовые направления и продолжающим оказывать влияние на информатику.

Книги по точным наукам, вообще говоря, не балуют своих читателей философскими размышлениями. Книга Дейкстры – счастливое исключение: это одновременно и математический текст, и сборник рецептов, и интеллектуальное откровение пророка.

В известном смысле «Дисциплина программирования» - это продолжение исследований Э.Дейкстры по структурному программированию, построению алгоритмов и развитию методов программирования. Книге, как и другим работам Дейкстры, присущ тонкий юмор, глубина проникновения в проблемы и искусство воплощения идей в алгоритмы и программы. Дейкстра как бы говорит: «Посмотрите, как можно рассуждать о программах, как можно их проектировать так, чтобы на любом этапе разработки вы не теряли уверенности в правильности – логической, семантической, математической – того, что вы делаете».

Формально книга представляет собой описание решений примерно двух десятков задач, начиная от самых простых (алгоритм Евклида нахождения наибольшего общего делителя), до весьма сложных (построение выпуклой оболочки по заданным точкам в 3-х мерном пространстве). Если бы книга ограничивалась только этим, то, безусловно, она была бы интересна, познавательна, но не более.

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

Программирование – не набор пассов и заклинаний, не шаманство, не танцы с бубном, а математическая дисциплина. А всякая дисциплина, если она претендует на нечто большее, чем на внешний эффект, должна строиться на прочном фундаменте. Таким фундаментом для Дейкстры является математическая логика, а точнее – исчисление предикатов. Сейчас это не кажется чем-то необычным, но в те годы это прозвучало как откровение. Дейкстра понял и убедительно показал, как теория может и должна помочь практике.

В конце 60-х годов XX века американцем Р.Флойдом и англичанином Ч.Хоаром - оба, кстати, Тьюринговские лауреаты - было начато исследование формальных свойств программ. Нельзя сказать, что до них этими вопросами никто не занимался, но предыдущие исследования (за исключением, пожалуй, передовых статей создателя языка LISP Дж.Мак-Карти) носили довольно фрагментарный характер. Самые проницательные исследователи понимали, что назревал кризис, обусловленный сложностью и объемом программного обеспечения: индустрии грозила опасность захлебнуться в миллионах строк кода. Ч.Хоар, используя идеи Р.Флойда, предложил формализм для обозначения частичной корректности программ. Этот формализм выражался формулой вида:

{Q} S {R}

имевший следующий смысл: если команда S начинается в начальном состоянии, удовлетворяющем предикату (т.е. условию) Q, то имеется гарантия , что выполнение S заканчивается через конечное время в состояниии удовлетворяющему предикату (т.е. условию) R.

Это все, конечно, очень и очень абстрактно; сейчас я, в качестве примера, рассмотрю реализацию на языке программирования Java алгоритма определения наибольшего общего делителя (НОД) пары целых чисел по алгоритму Евклида:

Void gcd (int x, int y) {

while (x != y) {

if (x > y) x = x – y;

if (x < y) y = y – x;

}

System.out.println (x);

}

Теперь проверим как работает эта реализация при различных значениях аргументов:

................................................................................................


Вызов gcd (0, 257), очевидно, работает не так как надо: правильный результат 257. Для пары (0, 0) результат вообще не определен: любое число исключая 0 служит решением. Последние два варианта (когда один или оба аргумента метода отрицательны) не позволяют определить правильный результат (он, кстати, равен по-прежнему 37). Одним словом – либо неполна реализация (в ней не обрабатываются особые случаи), либо я передаю недопустимые значения входных аргументов.

Кто в этом виноват? Конечно, программист – он обязан был это предусмотреть какие значения аргументов допустимы, а какие нет. Причем еще на этапе написания программы. Можно ли предотвратить подобные ситуации? Можно. Как именно? Ответ и его обоснование и находятся в книге Дейкстры.

Цель программирования – написание программ, выполняющих поставленные задачи. Возвращаясь к примеру очевидно, что в нем такой задачей является нахождение НОД пары чисел и легко видеть, что правильный ответ зависит от области значений аргументов. С точки зрения математики алгоритм нахождения НОД отвечает тому, что требуется (сам Евклид тому порукой); но раз есть ошибки выполнения, то их источник кроется в реализации этого алгоритма.

Вспоминая школьную алгебру мы вспомним, что многие изучаемые в ней функции определены не для всех значений аргументов. Скажем, квадратный корень определен только для неотрицательных аргументов (комплексные числа я не рассматриваю); деление определено только в том случае, когда делитель не равен 0. Все это – примеры частичных функций. А вот, к примеру, сложение и умножение определены всегда. Следовательно, приведенная выше реализация алгоритма Евклида определена не для всех значений аргументов, т.е. является примером частичной (не всюду определенной) функции. Иными словами, начальные условия при данной реализации должны удовлетворять некоторым условиям, а именно – это должны быть только положительные целые числа.

Вот что пишет Дейкстра:
Цитата:
«Условие, характеризующее множество всех начальных состояний, при которых запуск обязательно приведет к событию правильного завершения, причем система останется в конечном состоянии, удовлетворяющем заданному постусловию, называется «слабейшим предусловием, соответствующим этому постусловию». (Мы называем его «слабейшим», поскольку, чем слабее условие, тем больше состояний удовлетворяют ему, а мы стремимся здесь охарактеризовать все возможные начальные состояния, которые неизбежно приведут к желаемому конечному состоянию.)

Если система (машина, конструкция) обозначается через S, а желаемое постусловие - через R, то соответствующее слабейшее предусловие мы обозначим wp (S, R)»

(здесь «wp» – это аббревиатура от «weakest precondition»).

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

Таким образом методика построения программ по Дейкстре носит характер поиска начальных условий при которых программа S будет правильно завершена (т.е. окажется в состоянии, удовлетворяющем R). Очень важно сделать такой поиск систематическим; поиск вслепую, как это продемонстрировано выше, не подходит. Для этого Дейкстра привлекает аппарат исчисления предикатов из математической логики; начальные условия не просто ищутся - они выводятся: убедительны не голословные утверждения и не результаты тестовых прогонов, а исключительно математически доказуемые факты. При этом доказательство программы строится параллельно ее написанию. Выгоды этого очевидны – мы получаем более или менее убедительные (в зависимости от глубины анализа) свидетельства того, что программа делает то, что от нее ожидается.

Этот подход – вдохновленный работами Р.Флойда и Ч.Хоара и убедительно развитый Эдсгером Дейкстрой – получил имя «формальной верфикации» программ. Для демонстрации разработки программ посредством логического вывода Дейкстра в своей книге описывает очень простой язык программирования, напоминающий в своих основных чертах ALGOL-60, язык настолько простой, что в нем даже нет процедур. В обоснование синтаксиса и семантики этого языка, Дейкстра, следуя своей же методике, дает строгие доказательства поведения основных конструкций – прежде всего, оператора выбора и оператора цикла. Для этого он вводит понятие охраняемых команд, выполнение которых зависит от состояния т.н. предохранителей. Одним словом, Дейкстра стремится обеспечить полную уверенность в том, что его инструментарий свободен от подводных камней и неожиданных особенностей.

Нельзя сказать, что методика Дейкстры получила полное и безоговорочное признание: многое в ней отпугивало и казалось чересчур сложным. Вот слова самого Дейкстры из его введения к книге Д.Гриса «Наука программирования»:
Цитата:
«Разница между «старой программой» и «новой программой» столь же глубока, сколь глубока разница между гипотезой и доказанной теоремой или между математическим наблюдением и утверждением, строго выведенным из свода постулатов...

Новые формализмы всегда страшат, и требуются значительные и тщательные педагогические усилия, чтобы убедить новичка в том, что формализм не только полезен, но и необходим»

Мне кажется, основной причиной того, что методика Э.Дейкстры так и не стала mainstream-ом заключалась в определенных требованиях к математической культуре программистов (хотя ничего сверх самого элементарного курса математической логики и скромных способностей к абстрактному мышлению не требуется). Кроме того, радикальное снижение стоимости программного обеспечения и стремительное проникновение компьютеров во все области науки, производства и быта требовало все большего объема программного обеспечения и увеличения скорости его разработки. Стоимость труда программиста стала определяющим экономическим фактором. Но за все надо платить. Если цена ошибки программного обеспечения космической ракеты или медицинского томографа очень высока и тут необходимо обеспечить более строгий подход (хотя именно эти области как раз и «отличились» катастрофическими ошибками), то ошибка в игровой программе, броузере или редакторе текста стали зачастую восприниматься как «недокументированная возможность».

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

Было бы глупо и смешно пересказывать «Дисциплину программирования» - ее надо прочесть. То, о чем я рассказал – лишь малая часть того интеллектуального богатства щедро рассыпанного автором на страницах его книги.

Афоризмы

На этом мой небольшой рассказ об Эдсгере В.Дейкстре подошел к концу. Но рассказ о нем будет не полон без упоминания о еще одной стороне творчества великого программиста – его афоризмах, ставших поистине «народным» программистским фольклором. Некоторые из них весьма резки, например: «Студентов, ранее изучавших Бейсик, практически невозможно обучить хорошему программированию. Как потенциальные программисты они подверглись необратимой умственной деградации». Другие более сдержанны: «Средства не виноваты в том, что их безграмотно используют» или «Если отладка - процесс удаления ошибок, то программирование должно быть процессом их внесения». Сами афоризмы отнюдь не тщеславное желание их автора прослыть остроумным человеком; они - концентрированное выражение опыта, интуиции и тонкого аналитического мастерства Эдсгера Вибе Дейкстры – смиренного гения программирования.

Список литературы

Список литературы я условно разделил на две части: прежде всего - работы самого Э.В.Дейкстры, а затем - книги других авторов, вплотную примыкающие к темам, затронутым в статье.

E.W.Dijkstra Archive http://www.cs.utexas.edu/users/EWD/

Электронный архив трудов и рукописей Эдсгера В.Дейкстры

Э.Дейкстра «Взаимодействие последовательных процессов» (сборник статей «Языки программирования») – М.:, Мир, 1972

Э.Дейкстра «Заметки по структурному программированию» (сборник статей «Структурное программирование») – М.: Мир, 1975

Э.Дейкстра «Дисциплина программирования» - М.: Мир, 1978

Д.Грис «Наука программирования» - М.: Мир, 1984

Адаптированный вариант «Дисциплины программирования», написанный как учебник программирования для университетов. Изложение весьма строгое, но доступное (вся необходимая математика излагается в книге). По словам редактора книги академика А.П.Ершова «... книга Д.Гриса – апостольское деяние, направленное на то, чтобы превратить учение одиночки в мировую религию»

С.Алагич и М.Арбиб «Проектирование корректных структурированных программ» - М.: Радио и Связь, 1984

Более простая книга, нежели работа Д.Гриса. Математики заметно меньше, зато много практических примеров и упражнений. Основной язык программирования - PASCAL

Ч.Хоар «Взаимодействующие последовательные процессы» - М.: Мир, 1989

Прекрасное изложение теории взаимодействующих процессов и параллелизма. Детальное обсуждение множества вопросов затронутых в статье Дейкстры. Чтение книги предполагает знакомство читателя с основами математической логики и теории множеств

C.A.R.Hoare «An axiomatic basis of computer programming». Communications ACM, v.2 (October 1969), p.576-580, 583

Пионерская работа Ч.Хоара о построении формального базиса программирования

В.Аджиев «Мифы о безопасном ПО: уроки знаменитых катастроф» – журнал «Открытые Системы», июнь 1998 (http://www.osp.ru/os/1998/06/179592/)

Среди программистов всегда бытовали байки об ошибках программного обеспечения. Трудно сказать – насколько они правдивы. Почти наверняка, что-то подобное происходило: как у каждого хорошего врача есть свое кладбище, так и у каждого хорошего программиста есть своя подборка ошибок и провалов. Эта статья посвящена описанию нескольких ошибок программного обеспечения имевших катастрофические последствия.


Последний раз редактировалось Владимир Паронджанов Пятница, 10 Август, 2012 11:37, всего редактировалось 2 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Пятница, 10 Август, 2012 11:20 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
ПУНКТ ВТОРОЙ

Цитата из статьи Алексея Вторникова.

Алексей Вторников пишет:
Цитата:
Мне кажется, основной причиной того, что методика Э.Дейкстры так и не стала mainstream-ом заключалась в определенных требованиях к математической культуре программистов (хотя ничего сверх самого элементарного курса математической логики и скромных способностей к абстрактному мышлению не требуется).

Кроме того, радикальное снижение стоимости программного обеспечения и стремительное проникновение компьютеров во все области науки, производства и быта требовало все большего объема программного обеспечения и увеличения скорости его разработки. Стоимость труда программиста стала определяющим экономическим фактором. Но за все надо платить.

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

В связи со сказанным в статье Алексея Вторникова у меня возникают вопросы.

Вопрос первый. Стала ли методика Э. Дейкстры, описанная в книге "Дисциплина программирования", повсеместно распространенной в мировой практике программирования? То есть, как выражается Вторников, "стала ли она mainstream-ом"?

На этот вопрос Алексей Вторников недвусмысленно отвечает: Нет, она "так и не стала mainstream-ом".

Вопрос второй. Почему? Что явилось основной причиной неудачи?

Алексей Вторников отвечает: Мне кажется, основной причиной того, что методика Э.Дейкстры так и не стала mainstream-ом заключалась в определенных требованиях к математической культуре программистов (хотя ничего сверх самого элементарного курса математической логики и скромных способностей к абстрактному мышлению не требуется).

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

Вопрос третий. Может быть, эти требования слишком высокие, чрезмерные?

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

ПУНКТ ТРЕТИЙ

МИСТИЧЕСКАЯ ТАЙНА СОВРЕМЕННОГО ПРОГРАММИРОВАНИЯ,
или Загадка, которая не имеет ответа.
Ой ли, неужели действительно не имеет?


Автор статьи, Алексей Вторников сам себе противоречит.
Противоречие состоит в следующем.

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

Но по какой-то загадочной причине это не произошло.

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

Но! Реальные, живые программисты (в своей основной массе) по каким-то непонятным причинам то ли не могут, то ли не хотят пользоваться прекрасным методом, описанным в замечательной книге Эдсгера Дейкстры "Дисциплина программирования".

В чем разгадка этой Великой Тайны?


Последний раз редактировалось Владимир Паронджанов Пятница, 10 Август, 2012 12:47, всего редактировалось 7 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Пятница, 10 Август, 2012 11:37 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Итак, цитированное подразумевает некоторые уточнения:

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

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

А, например, методы Дейкстры или формальной верификации типа model-checking позволяют убедиться в том, что поведение программы соответствует спецификации требований.

Уважаемый Илья Евгеньевич!

Отвечу на Ваш последний абзац, который я выделил жирным.
...
- то следует, видимо, говорить о методе Хоара - что обсуждалось уже: viewtopic.php?p=72529#p72529. Это не метод Дейкстры в описании из "Как улучшить..." (т.е. не видеоструктурный). В цитированной выдержке Кауфман объясняет суть. И по тому, какой предмет обсуждения называет Илья как "доказательное программирование" и с чем рядополагает то, что называет "методом Дейкстры" (проверка моделей), видно, о чём он говорит... а из плана, данного Вами, можно предположить, что Вы хотите отвечать по видеоструктурам - т.е. на иной вопрос?..

2) Что сделал Дейкстра для предмета, обсуждаемого Ильёй - говорилось чуть раньше: viewtopic.php?p=72517#p72517. Карпов, кстати, описывает, как Вы можете помнить, ту самую проверку моделей...

3) Ну и вытекающий отсюда вопрос - как из шампур-"слепыша" м.б. получена структура Крипке для проверки модели программы в целом?.. и как сформулированы утверждения по семантике "аннотированной по Дейкстре" программы?..


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Пятница, 10 Август, 2012 17:32 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
Продолжаю отвечать на сообщение Ильи Ермакова
Илья Ермаков в сообщении viewtopic.php?p=73786#p73786 , в частности, писал(а):
... методы Дейкстры или формальной верификации типа model-checking позволяют убедиться в том, что поведение программы соответствует спецификации требований.


ПУНКТ ЧЕТВЕРТЫЙ

О книге Эдсгера Дейкстры "Дисциплина программирования"

Это выдающаяся книга, сыгравшая важную роль в истории программирования.

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

Многие программисты (но отнюдь не все) освоили метод математического доказательства правильности программ по Дейкстре. И с успехом применяют этот метод на практике.

В Википедии развитие этого метода отражено в статьях:

Цитата:
Формальная верификация (Раздел "Доказательное программирование")
http://ru.wikipedia.org/wiki/%D0%A4%D0% ... 0%B8%D1%8F

Formal verification
http://en.wikipedia.org/wiki/Formal_ver ... r_software

Цитата:


Последний раз редактировалось Владимир Паронджанов Пятница, 10 Август, 2012 18:08, всего редактировалось 4 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Пятница, 10 Август, 2012 17:45 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
ПУНКТ ПЯТЫЙ

Вернемся к статье Алексея Вторникова, опубликованной в журнале "Системный администратор". И повторим вытекающие из нее вопросы.

Вопрос первый. Стала ли методика Э. Дейкстры, описанная в книге "Дисциплина программирования", повсеместно распространенной в мировой практике программирования? То есть, как выражается Вторников, "стала ли она mainstream-ом"?

Ответ. Нет, не стала.

Вопрос второй. Почему? Что явилось причиной неудачи?

Алексей Вторников отвечает: Мне кажется, основной причиной того, что методика Э.Дейкстры так и не стала mainstream-ом заключалась в определенных требованиях к математической культуре программистов (хотя ничего сверх самого элементарного курса математической логики и скромных способностей к абстрактному мышлению не требуется).

А теперь уберем лишние слова и дадим краткий ответ.

Причина неудачи в том, что метод Дейкстры слишком сложен.

Большинство программистов не пользуются им потому, что для большинства программистов время и усилия, затраченные на освоение этого (безусловно, очень хорошего метода) слишком велики и не оправдывают полученный результат.


Люди не дураки. Их не обманешь. Все решает критерий "затраты — результат".

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

А для большинства программистов метод Дейкстры по критерию "затраты — результат" оказывается неэффективным.


Так что дело вовсе не в том, что метод хорош, а большинство программистов плохие. Мол, не доросли они до этого замечательного метода.

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

Это неверно. Вторников ошибся.

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

ПУНКТ ШЕСТОЙ

В чем разгадка Великой Тайны?

В том, что метод Дейкстры (метод доказательного программирования) в одиночку не справляется с серьезными проблемами, возникающими в ходе развития науки и практики (сomputer science и практики программирования).

Этот метод следует дополнить другими методами.
Какими?

В частности, методами когнитивной эргономики, используемыми в языке ДРАКОН.

Поскольку важной проблемой является СЛОЖНОСТЬ, то желательно уменьшить сложность с помощью когнитивно-эргономических методов.


Последний раз редактировалось Владимир Паронджанов Пятница, 10 Август, 2012 19:12, всего редактировалось 8 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Пятница, 10 Август, 2012 17:59 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Ну вот, из многаждого редактирования постов стало ясно, что будем обсуждать действительно доказательность... :)

Итак:
Владимир Паронджанов писал(а):
...
ПУНКТ ТРЕТИЙ

МИСТИЧЕСКАЯ ТАЙНА СОВРЕМЕННОГО ПРОГРАММИРОВАНИЯ,
или Загадка, которая не имеет ответа.
Ой ли, неужели действительно не имеет?


Автор статьи, Алексей Вторников сам себе противоречит.
Противоречие состоит в следующем.
...
В чем основная причина неудачи? Согласно Вторникову, секрет в том, что требования к математической культуре какие-то не такие. С одной стороны, они не чрезмерные, а самые обыкновенные.

Но! Реальные, живые программисты (в своей основной массе) по каким-то непонятным причинам то ли не могут, то ли не хотят пользоваться прекрасным методом, описанным в замечательной книге Эдсгера Дейкстры "Дисциплина программирования".

В чем разгадка этой Великой Тайны?
Дык ведь он сам же и отвечает... здесь:
Владимир Паронджанов писал(а):
...
ПУНКТ ВТОРОЙ
...
Алексей Вторников пишет:
Цитата:
...
Если цена ошибки программного обеспечения космической ракеты или медицинского томографа очень высока и тут необходимо обеспечить более строгий подход ..., то ошибка в игровой программе, броузере или редакторе текста стали зачастую восприниматься как «недокументированная возможность».
О том же писал и Громов... обсуждалось в п.3 этого поста... вместе с условиями применимости...

Вот уж действительно:
Владимир Паронджанов писал(а):
...
ПУНКТ ТРЕТИЙ

МИСТИЧЕСКАЯ ТАЙНА СОВРЕМЕННОГО ПРОГРАММИРОВАНИЯ,
или Загадка, которая не имеет ответа.
Ой ли, неужели действительно не имеет?
:)
Ответ по существу же лежит не в плоскости подготовленности, а в психологической... во-первых, если можно не делать - то зачем делать?.. :wink: Во-вторых, если можно делать иначе - то тот, кому удобнее, будет делать иначе.
Как? Возможный вариант намечал ещё Дж. Вейценбаум - "заклинать" машину программой, объяснять ей, "пока не поймёт". Кстати, это цитировал Илья в своём докладе об инженерии ПО... В немалой степени - применяя брейки/континуи, ретурны... а то и произвольные БП...

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

И если не потребуется полная ответственность разработчика за результаты (юридически м.б. его нанимателя - но он всё равно переложит :wink:) - то не будет он этим заниматься. Даже если уровень культуры позволяет... но комбинировать проще... :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Суббота, 11 Август, 2012 09:52 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
Продолжаю отвечать на сообщение Ильи Ермакова
Илья Ермаков в сообщении viewtopic.php?p=73786#p73786 , в частности, писал(а):
... методы Дейкстры или формальной верификации типа model-checking позволяют убедиться в том, что поведение программы соответствует спецификации требований.


ПУНКТ СЕДЬМОЙ

Статья Валерия Аджиева Часть 1
http://www.osp.ru/os/1998/06/179592/

опубликована в журнале «Открытые системы», № 06, 1998 5051

Мифы о безопасном ПО: уроки знаменитых катастроф

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

Валерий Аджиев



Цитата:
"Если бы строители строили здания так же, как программисты пишут программы, первый залетевший дятел разрушил бы цивилизацию", - второй закон Вейлера.

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

Слово "безопасность" не сходит со страниц компьютерной прессы. Однако, употребляется оно обычно в контексте поддержания целостности данных и - особенно - обеспечения их конфиденциальности. Что ж, тема интересная: Internet, банки, спецслужбы, хакеры ... - все, к чему приложимо вошедшее в повседневный обиход слово "seсurity". Есть, однако, у "безопасности" и другое измерение, чаще обозначаемое не столь популярным термином "safety", про которое говорят меньше, но важность его - применительно к компьютерным системам - поистине нельзя переоценить.

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

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

Катастрофа Ariane 5

4 июня 1996 года был произведен первый запуск ракеты-носителя Ariane 5 - детища и гордости Европейского Сообщества. Уже через неполные 40 сек. все закончилось взрывом. Автоподрыв 50-метровой ракеты произошел в районе ее запуска с космодрома во Французской Гвиане. За предшествующие годы ракеты серии Ariane семь раз терпели аварии, но эта побила все рекорды по вызванным ею убыткам. Только находившееся на борту научное оборудование потянуло на пол-миллиарда долларов, не говоря о прочих разноообразных издержках; а астрономические цифры "упущенной выгоды" от несостоявшихся коммерческих запусков и потеря репутации надежного перевозчика в очень конкурентном секторе мировой экономики ("стоимость рынка" к 2000 г. должна превысить 60 млрд. долл.) с трудом поддаются оценке. Небезынтересно отметить, что предыдущая модель - ракета Ariane 4 - успешно запускалась более 100 раз.

Буквально на следующий день Генеральный директор Европейского Космического Агенства (ESA) и Председатель Правления Французского Национального Центра по изучению Космоса (CNES) издали распоряжение об образовании независимой Комиссии по Расследованию обстоятельств и причин этого чрезвычайного происшествия, в которую вошли известные специалисты и ученые изо всех заинтересованных европейских стран. Возглавил Комиссию представитель Французской Академии Наук профессор Жак-Луи Лион (Jacques-Louis Lions). Кроме того, был сформирован специальный Технический Комитет из представителей заказчиков и подрядчиков, ответственных за производство и эксплуатацию ракеты, в чью обязанность было вменено незамедлительно предоставлять Комиссии всю необходимую информацию.

13 июня 1996 г. Комиссия приступила к работе, а уже 19 июля был обнародован ее исчерпывающий доклад, который сразу же стал доступен в Сети [1]. Что же касается информации, которую - при участии нескольких институтов - осмысляла Комиссия, то она состояла из телеметрии, траекторных данных, а также оптических наблюдений за ходом полета. Были собраны (что само по себе было непросто, так как взрыв произошел на высоте приблизительно 4 км, и осколки были рассеяны на площади около 12 кв. км. в саванне и болотах) и изучены части ракеты и оборудования. Кроме того, были заслушаны показания многочисленных специалистов и изучены горы производственной и эксплуатационной документации.

Технические подробности аварии

Положение и ориентация ракеты-носителя в пространстве измеряются Навигационной Системой (Inertial Reference Systems - IRS), составной частью которой является встроенный компьютер, вычисляющий углы и скорости на основе информации от бортовой Инерциальной Платформы, оборудованной лазерными гироскопами и акселерометрами. Данные от IRS передаются по специальной шине на Бортовой Компьютер (On-Board Computer - OBC), который обеспечивает необходимую для реализации программы полета информацию и непосредственно - через гидравлические и сервоприводы - управляет твердотопливными ускорителями и криогенным двигателем типа Вулкан (Vulkain).

Как обычно, для обеспечения надежности Системы Управления Полетом используется дублирование оборудования. Поэтому две системы IRS (одна - активная, другая - ее горячий резерв) с идентичным аппаратным и программным обеспечением функционируют параллельно. Как только бортовой компьютер OBC обнаруживает, что "активная" IRS вышла из штатного режима, он сразу же переключается на другую. Впрочем, и бортовых компьютеров тоже два.

Теперь, следуя Докладу Комиссии [1], проследим все значимые фазы развития процесса, оказавшегося в конце концов аварийным. Момент старта обозначим H0 - это и будет точка отсчета для всех событий, хотя отслеживать их мы будем в обратном - начиная с момента саморазрушения системы - порядке. Для полноты картины упомянем, что предшествующие старту операции происходили в нормальном режиме вплоть до момента H0-7 минут, когда было зафиксировано нарушение "критерия видимости". Поэтому старт был перенесен на час; в H0 = 9 час. 33 мин. 59 сек. местного времени "окно запуска" было вновь "поймано" и был, наконец, осуществлен сам запуск, который и происходил штатно вплоть до момента H0+37 сек. В последующие секунды произошло резкое отклонение ракеты от заданной траектории, что и закончилось взрывом. Итак:

      в момент H0+39 сек. из-за высокой аэродинамической нагрузки вследствие превышения "углом атаки" критической величины на 20 градусов произошло отделение стартовых ускорителей ракеты от основной ее ступени, что и послужило основанием для включения Системы Автоподрыва ракеты;
      изменение угла атаки произошло по причине нештатного вращения сопел твердотопливных ускорителей;

      такое отклонение сопел ускорителей от правильной ориентации вызвала в момент H0 + 37 сек. команда, выданная Бортовым Компьютером на основе информации от активной Навигационной Системы (IRS 2). Часть этой информации была в принципе некорректной: то, что интерпретировалось как полетные данные, на самом деле являлось диагностической информацией встроенного компьютера системы IRS 2;

      встроенный компьютер IRS 2 передал некорректные данные, потому что диагностировал нештатную ситуацию, "поймав" исключение (exception), выброшенное одним из модулей программного обеспечения;

      при этом Бортовой Компьютер не мог переключиться на резервную систему IRS 1, так как она уже прекратила функционировать в течение предшествующего цикла (занявшего 72 мсек.) - по той же причине, что и IRS 2;

      исключение, "выброшенное" одной из программ IRS, явилось следствием выполнения преобразования данных из 64-разрядного формата с плавающей точкой в 16-разрядное целое со знаком, что привело к "Operand Error";

      ошибка произошла в компоненте ПО, предназначенном исключительно для выполнения "регулировки" Инерциальной Платформы. Причем - что звучит парадоксально, если не абсурдно - этот программный модуль выдает значимые результаты только до момента H0 + 7 сек. отрыва ракеты со стартовой площадки. После того, как ракета взлетела, никакого влияния на полет функционирование данного модуля оказать не могло;

      однако, "функция регулировки" действительно должна была (в соответствии с установленными для нее требованиями) действовать еще 50 сек. после инициации "полетного режима" на шине Навигационной Системы (момент H0-3 сек.), что она с усердием дурака, которого заставили богу молиться, и делала;

      ошибка "Operand Error" произошла из-за неожиданно большой величины BH (Horizontal Bias - горизонтальный наклон), посчитанной внутренней функцией на основании величины "горизонтальной скорости", измеренной находящимися на Платформе датчиками. Величина BH служила индикатором точности позиционирования Платформы;

      величина BH оказалась много больше, чем ожидалось потому, что траектория полета Ariane 5 на ранней стадии существенно отличалась от траектории полета Ariane 4 (где этот программный модуль использовался ранее), что и привело к значительно более высокой "горизонтальной скорости".


Финальным же действием, имевшим фатальные последствия, стало прекращение работы процессора; соответственно, вся Навигационная Система перестала функционировать. Возобновить же ее действия оказалось технически невозможно.

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

Причины и истоки аварии

Прежде всего проследим, откуда взялось первоначальное требование на продолжение выполнения операции регулировки после взлета ракеты. Оказывается, оно было заложено более чем за 10 лет до рокового события, когда проектировались еще ранние модели серии Ariane. При некотором (весьма маловероятном!) развитии событий взлет мог быть отменен буквально за несколько секунд до старта, например в промежутке H0-9 сек., когда на IRS запускался "полетный режим", и H0-5 сек., когда выдавалась команда на выполнение некоторых операций с ракетным оборудованием. В случае неожиданной отмены взлета необходимо было быстро вернуться в режим "обратного отсчета" (countdown) - и при этом не повторять сначала все установочные операции, в том числе приведение к исходному положения Инерциальной Платформы (операция, требующая 45 мин. - время, за которое можно потерять "окно запуска").

Было обосновано, что в случае события отмены старта период в 50 сек. после H0-9 будет достаточным для того, чтобы наземное оборудование смогло восстановить полный контроль за Инерциальной Платформой без потери информации - за это время Платформа прекратит начавшееся было перемещение, а соответствующий программный модуль всю информацию о ее состоянии зафиксирует, что поможет оперативно возвратить ее в исходное положение (напомним, что все это в случае, когда ракета продолжает находиться на месте старта). И действительно, однажды, в 1989 году, при старте под номером 33 ракеты Ariane 4, эта особенность была с успехом задействована.

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

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

Расследование показало, что в данном программном модуле присутствовало целых семь переменных, вовлеченных в операции преобразования типов. Оказалось, что разработчики проводили анализ всех операций, способных потенциально генерировать исключение, на уязвимость. И это было их вполне сознательным решением добавить надлежащую защиту к четырем переменным, а три - включая BH - оставить незащищенными. Основанием для такого решения была уверенность в том, что для этих трех переменных возникновение ситуации переполнения невозможно в принципе. Уверенность эта была подкреплена расчетами, показывающими, что ожидаемый диапазон физических полетных параметров, на основании которых определяются величины упомянутых переменных, таков, что к нежелательной ситуации привести не может. И это было верно - но для траектории, рассчитанной для модели Ariane 4. А ракета нового поколения Ariane 5 стартовала по совсем другой траектории, для которой никаких оценок не выполнялось. Между тем она (вкупе с высоким начальным ускорением) была такова, что "горизонтальная скорость" превзошла расчетную (для Ariane 4) более чем в пять раз.

Но почему же не была (пусть в порядке перестраховки) обеспечена защита для всех семи, включая BH, переменных? Оказывается, для компьютера IRS была продекларирована максимальная величина рабочей нагрузки в 80%, и поэтому разработчики должны были искать пути снижения излишних вычислительных издержек. Вот они и ослабили защиту там, где теоретически нежелательной ситуации возникнуть не могло. Когда же она возникла, то вступил в действие такой механизм обработки исключительной ситуации, который оказался совершенно неадекватным.

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

Осмысление

Произошедшая с Ariane 5 катастрофа имела исключительно большой резонанс - и по причине беспрецедентных материальных потерь, и вследствие очень оперативного расследования, характеризовавшегося к тому же открытостью результатов (впервые такая практика публичности была опробована при расследовании причин аварии космического корабля Challenger в 1986 году). Сразу стало очевидным, что данному событию суждено войти в историю не только космонавтики, но и программной инженерии. Поэтому неудивительно, что авария послужила поводом для оживленной дискуссии, в которой приняли участие многие известные специалисты.

Ж.-М. Жезекель (J.-M. Jezequel) и Бертран Мейер (B.Meyer) [2] пришли к совершенно однозначному выводу: допущенная (и так и не выявленная) программная ошибка носит, по их мнению, чисто технический характер и коренится в некорректной практике повторного использования ПО. Более точная формулировка: роковую роль сыграло отсутствие точной спецификации повторно-используемого модуля. Расследование показало, что обнаружить требование, устанавливающее максимальную величину BH (вмещающуюся в 16 битов), можно было с большим трудом: оно затерялось в приложениях к основному спецификационному документу. Мало того, в самом коде на этот счет не было никаких комментариев, не говоря уже о ссылке на документ с обоснованием этого требования.

В качестве панацеи в такого рода ситуациях авторы предложили задействовать принцип "Контрактного Проектирования" (что и неудивительно, ибо его разработчиком как раз и является Мейер [3]). Именно "контракт" в духе языка Eiffel, явным образом (с помощью пред- и пост-условий) устанавливающий для любого программного компонента ограничения на входные и выходные параметры, и мог бы предотратить катастрофическое развитие событий. Был приведен и набросок такого контракта:

      convert (horizontal_bias:INTEGER): INTEGER is require horizontal_bias <= Maximum_bias do ... ensure ... end


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

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

Авторы с сожалением заключают, что контрактные механизмы никак не получат должного распространения в современной практике. Более того, положение только усугубляется: например, в Java даже исчезла присутствовавшая в языке Cи скромная по возможностям инструкция "assert". В составной части CORBA - языке IDL (Interface Definition Language), предназначенном обеспечить полномасштабное повторное использование компонентов в распределенной среде, отсутствует какой-либо механизм спецификации семантики. То же относится и к ActiveX. Авторы заключают: без полной и точной спецификации, основанной на пред- и пост-условиях и инвариантах, "повторное использование программных компонентов - совершенное безрассудство".

Эта точка зрения вызвала многочисленные отклики. Хотя полезность использования контрактных механизмов никто не оспаривал, все же взгляд авторов многим показался упрощенным. Наиболее обстоятельный критический разбор их статьи выполнил сотрудник Locheed Martin Tactical AirCraft Systems, известный специалист в области разработки ответственных систем Кен Гарлингтон (Ken Garlington) [4]. Он начал с того, что указал на ошибку в приведенном наброске контракта, где предполагается, что BH преобразуется не из вещественного (как то было в реальности) числа, а из целого.

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

Вывод Гарлингтона вполне отвечает здравому смыслу: проблема носит комплексный характер и обусловлена прежде всего объективной сложностью систем типа Ariane. Соответственно, одним лекарством болезнь, приводящая к появлению ошибок в ПО, вылечена быть не может. Хотя то, что процесс мониторинга спецификаций, кода и документов с обоснованием проектных решений при разработке ПО для Ariane 5, оказался неадекватен, отметила и Комиссия по расследованию аварии. В частности, подчеркнуто, что к процессу контроля не привлекались специалисты из организаций, независимых как от заказчика, так и от подрядчика системы, что нарушило принцип разделения исполнительных и контрольных функций.

Большие претензии были предъявлены не только к процессу тестирования как таковому, но и к самой его стратегии. На этапе тестирования и отладки системы было технически возможно в рамках интегрального моделирования процесса полета исследовать все аспекты работы IRS, что позволило бы почти гарантированно выявить ошибку, приведшую к аварии. Однако, вместо этого при моделировании работы всего комплекса IRS рассматривалась как черный ящик, заведомо выдающий то, что ожидается. Почему? А зачем тестировать то, что успешно работало в течение многих лет?!

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

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

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

В контексте данной статьи интересно мнение главного редактора журнала "Automated Software Engineering" Башара Нузейбеха (Bashar Nuseibeh) [5], который, дав обзор разных точек зрения на причины аварии и придя к выводу, что "все правы", связал все-таки катастрофу Ariane 5 с более общими проблемами разработки программных систем. Он отметил, в частности, что современные тенденции в программной инженерии, связанные с разделением интересов вовлеченных в разработку независимо работающих персонажей (что связано с широким внедрением таких подходов, как объектно-ориентированные и компонентные технологии) не получают надлежащего балансирующего противовеса в виде менеджмента, способного координировать всю работу на должном уровне. Эта тема заслуживает дальнейшего обсуждения, но сначала обратимся к еще одной печально знаменитой истории.


Последний раз редактировалось Владимир Паронджанов Суббота, 11 Август, 2012 10:21, всего редактировалось 2 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Суббота, 11 Август, 2012 09:56 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
ПУНКТ ВОСЬМОЙ

Цитата:
Статья Валерия Аджиева Часть 2
http://www.osp.ru/os/1998/06/179592/

опубликована в журнале «Открытые системы», № 06, 1998

Мифы о безопасном ПО: уроки знаменитых катастроф

Цитата:
Инциденты с Therac-25

Вспомним более давнюю историю, почти во всем отличную от ситуации с Ariane 5, а сходную только в том, что она также была подробно задокументирована [6] и получила в свое время большой резонанс как повлекшая наиболее тяжкие последствия за всю не столь долгую историю использования медицинских комплексов, управляемых компьютерами. Правда в этом случае полномасштабного официального расследования проведено не было; источниками информации послужили, в основном, протоколы встреч пользователей системы с производителем и материалы многочисленных судебных разбирательств.

Технические подробности инцидентов

В 1985-87 гг. 6 человек получили смертельную дозу облучения во время сеансов радиационной терапии с применением медицинского ускорителя Therac-25 (количество пациентов, также подвергшихся переоблучению, но выживших, точно не известно). Производителем установки являлось одно из подразделений Канадского Агентства Атомной Энергии (Atomic Energy of Canada Limited - AECL). Модель Therac-25, законченная в виде прототипа в 1976 г. и поступившая в промышленную эксплуатацию в 1982 г. (пять установок в США и шесть - в Канаде) была развитием ранних моделей Therac-6 и Therac-20. При этом некоторые программные модули, разработанные для ранних моделей, использовались повторно (в том числе - поставленные партнером, французской фирмой CGR, сотрудничество AECL с которой прекратилось к моменту начала работ над Therac-25).

Следующий инцидент, случившийся в июле того же года в Онкологическом Центре Онтарио как раз был задокументирован хорошо, но производитель не смог воспроизвести ситуацию, и ее отнесли на счет случайного сбоя аппаратуры; в ПО сомнений по-прежнему просто не было. И трагические инциденты продолжились.

Очередной из них произошел в Онкологическом Центре Восточного Техаса в марте 1986 года. В данном случае процессом управляла опытный оператор, проведшая уже более 500 подобных сеансов. Она быстро ввела предписанные параметры, после чего заметила, что вместо режима облучения электронными лучами заказала лучи рентгеновские (которыми пользовали большинство пациентов). Коррекция требовала исправления всего одной буквы; нажав кнопку, она вошла в режим редактирования, скорректировала в нужном месте "x" на "e", затем несколькими нажатиями клавиши "Return" (благо, все остальные параметры были введены правильно) достигла нижней (командной) строки экрана, убедилась, что против каждого введенного параметра горит "VERIFIED", а статус системы - ожидаемый ("BEAM READY"), и выдала команду начать процесс облучения. Однако, неожиданно система встала, на консоли высветилось сообщение "MALFUNCTION 54", а статус системы изменился на "TREATMENT PAUSE", что свидетельствовало о проблеме невысокой степени серьезности. Висевшая тут же бумага с кодами ошибок "исчерпывающе" поясняла, что "MALFUNCTION 54" означает "dose input 2". Забегая вперед, укажем, что много позже, во внутренней документации производителя было обнаружено, что это сообщение выдавалось в случае "ненадлежащей дозы облучения" - причем, как для слишком большой, так и для слишком малой, что само по себе странно (да и просто недопустимо - ведь ситуации принципиально разные). Озадаченная операторша взглянула на высветившееся количество отпущенной дозы и увидела, что оно - пренебрежимо мало. Поэтому она без долгих раздумий выдала команду на продолжение процесса, после чего вся описанная выше ситуация повторилась.

Тем временем пациент, который возлежал на столе в изолированном от оператора помещении, испытал некое подобие электрического шока. Он тоже был опытным (для него это был девятый сеанс), поэтому понял, что творится что-то неладное. Однако, дать сразу же знать об этом оператору через специально для того предназначенные видео и аудио средства он не смог: как выяснилось, видео было по непонятным причинам отключено, а аудиоканал - просто неисправен. После повторного шокового удара пациент вскочил и нимало шокировал уже операторшу, начав ломиться в стеклянные двери ее помещения. Поначалу его и лечили от электрошока (он умер через пять месяцев). Позднейшее моделирование ситуации показало, что пациент получил менее чем за 1 сек. на участок позвоночника в 1 кв. см. дозу в диапазоне от 16500 до 25000 рад (в то время, как ему было предписано принять в этом сеансе 180 рад, а всего - 6000 рад за шесть с половиной недель).

Прибывший из AECL инженер, несмотря на все усилия, оказался не в состоянии воспроизвести ситуацию, хотя заверил, что переоблучение в принципе невозможно. Были успешно прогнаны все тесты, система снова вступила в эксплуатацию, и через три недели инцидент повторился во всех деталях - с тем же трагическим результатом. Только после этого установка была выведена из эксплуатации, и началось углубленное расследование, шедшее, кстати, очень трудно. Опуская множество деталей, приведем его итоги, интересные с программистской точки зрения.

Особенности ПО как предпосылки для инцидентов

В комплексе не использовалась какая-либо стандартная операционная система: была разработана специальная мультизадачная ОС реального времени, для компьютера PDP-11/23 с 32Kбайт и написанная на языке ассемблера. Специальный планировщик координировал деятельность всех одновременно исполняющихся процессов. Задачи, запускавшиеся каждые 0,1 сек., разделялись на "критические", исполнявшиеся первыми, и "некритические". К критическим отнесены три приоритетных задачи (рис. 1):

      "Servo", ответственная за все операции, связанные с эмиссией радиационных пучков и доставкой их к месту назначения;

      "Housekeeper", выполнявшая верификацию всех параметров и ответственная за блокировку работы в случае возникновения нештатной ситуации, а также за сообщения о таких ситуациях;

      "Treat", управлявшая самим процессом лечения, который был разделен на 8 операционных фаз. В зависимости от значения переменной Tphase вызывалась одна из восьми подпрограмм, по окончании работы которой Treat - в зависимости от значений нескольких разделяемых с другими критическими и некритическими задачами переменных, вырабатывала план на новый цикл.


......................................................
Рис. 1. Взаимодействие задач и подпрограмм в ПО для Therac-25

Одна из вызываемых Treat подпрограмм - Datent (Data entry) через разделяемую "флаговую" переменную Data_entry_complete взаимодействует с "некритической" задачей Keyboard Handler, которая управляет вводом информации с клавиатуры, исполняясь параллельно с Treat. Keyboard Handler распознает момент окончания ввода и сигнализирует об этом, изменяя значение Data_entry_complete. В свою очередь, Datent проверяет значение этой переменной. Если оно не изменилось, то значение Tphase остается равным "1", и на следующем цикле Treat опять запустит Datent; если же значение Data_entry_complete изменилось, то Datent меняет значение Tphase с "1" на "3"; в результате после окончания работы Datent монитор Treat вызовет подпрограмму Set Up Test, выполняющую проверку считающихся уже установленными параметров.

Необходимо упомянуть еще одну переменную MEOS ( Mode/Energy Offset), разделяемую между Datent, Keyboard Handler и еще одной некритической задачей Hand. Старшие байты MEOS используются подпрограммой Datent для установки одного из двух режимов облучения и величины энергии испускаемого потока, в то время как младшие используются параллельно работающей задачей Hand для установки коллиматора в положение, соответствующее выбранному режиму и энергии.

Оператор мог после ввода параметров режима и энергии редактировать эти величины по отдельности. Однако, здесь присутствовал тонкий момент - разработчики установили: об окончании процесса ввода (и редактирования!) параметров свидетельствует то, что все параметры заданы и курсор находится в командной строке, на предмет чего каждые 8 сек. (величина выбрана, исходя из некоторых технических соображений, связанных с инерционностью приборов) производится опрос переменной Data_entry_complete. Если в пределах этих 8 сек. курсор покидает командную строку и - после быстрого редактирования параметров - успевает вернуться на нее, то Keyboard Handler этого события просто не заметит, и соответственно, никак переменную Data_entry_ complete не изменит. Иными словами, потенциально существует возможность для следующей последовательности действий:

      Keyboard Handler отследил местонахождение курсора на командной строке и установил флаг Data_entry_complete;

      затем оператор изменил данные в MEOS;

      не заметив этого (если к моменту опроса курсор оказался вновь на командной строке), Keyboard Handler не переустанавливает флаг Data_entry_complete;

      тогда Datent уже не способна обнаружить изменение MEOS - она свою работу закончивает, установив Tphase=3 (а не Tphase=1, чтобы отработать еще один цикл и учесть изменения);

      тем временем, параллельно работающая Hand устанавливает коллиматор в положение, соответствующее младшим байтам MEOS (их установила ранее Datent), которые могли находиться в противоречии со старшими байтами этой разделяемой переменной (как раз и подвергшимся редактированию!). Специальных проверок для обнаружения такой несовместимости предусмотрено не было.


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

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

Программная блокировка и ее последствия

Рассмотрим еще один инцидент с Therac-25, которому суждено было стать последним. Он произошел в Yakima Valley Memorial Hospital (штат Вашингтон) в январе 1987 г. Пациенту было предписано сначало проделать два рентгеновских снимка с дозой в 4 и 3 рад соответственно, а затем произвести в фотонном режиме облучение в 86 рад. Все это и было выполнено, однако, как потом было установлено, пациент получил переоблучение фотонной дозой до 10000 рад. (Установлено было "потом", а не сразу - оператор, сделав снимки, забыл вынуть рентгеновскую пленку из-под пациента, из-за чего у него на консоли горели все те же 7 рад; однако, и правильная индикация уже выданной дозы была бы здесь как - в буквальном смысле слова - мертвому припарки).

Что же произошло? Выявленная в итоге расследования проблема выходит далеко за пределы частного случая еще одной программистской ошибки. В данном случае не сработала блокировка, реализованная программно позволившая прибору действовать (испускать поток фотонов) при ошибочной установке параметров. Ситуация возникла в момент, когда введенные параметры уже верифицированы подпрограммой Datent и монитор Treat в соответствии со значением переменной Tphase = 3 вызвал подпрограмму Set Up Test.

Во время установки и подгонки параметров подпрограмма Set Up Test вызывается несколько сотен раз - пока все параметры не будут установлены и верифицированы, о чем эта подпрограмма судит по нулевому значению разделяемой переменной F$mal. Если же значение ненулевое - цикл повторяется. F$mal, в свою очередь, устанавливается подпрограммой Chkcol (Check Collimator) из критической задачи Housekeeper, проверяющей, все ли с коллиматором нормально; а вызывает Chkcol другая подпрограмма задачи Housekeeper под названием Lmtchk (analog-to-digital limit checking), и вызов этот происходит, только если значение разделяемой переменной Class3 ненулевое. А ненулевым его делает как раз сама Set Up Test, которая (пока F$mal=0) каждый раз выполняет над Class3 операцию инкремента.

Эта переменная - однобайтовая, следовательно каждый 256-й проход заставляет ее сбрасываться в ноль. А ведь этот ноль - свидетельство, что все параметры, наконец, установлены. Если повезет, что именно в этот момент оператор нажмет клавишу "set" для запуска установки коллиматора в надлежащую позицию (а он это может сделать в любой момент, так как уверен, что система позволит коллиматору начать позиционироваться, только если все параметры заданы и верифицированы), то основываясь на случайно возникшем нулевом значении Class3, подпрограмма Lmtchk уже не станет вызывать Chkcol, а значит установить ненулевое значение F$mal будет некому. Иными словами, в ситуации, когда параметры не установлены должным образом (в данном конкретном случае "челюсти" коллиматора были еще раскрыты слишком широко), программная блокировка не сработала: Set Test Up установила Tphase = 2, что позволило монитору Treat прекратить цикл вызова Set Up Test, а инициализировать подпрограмму Set Up Done, по существу запускающую процесс излучения, который и потек бурным потоком, а не узеньким ручейком, как предполагалось.

Коррекция этой ошибки также выполняется просто - вместо выполнения инкремента переменной Class3 следует просто присваивать фиксированное ненулевое значение. Вот от каких, казалось бы, мелких и чисто технических ляпсусов программиста может зависеть жизнь человека!

Некоторые итоги

История с Therac-25 показательна, прежде всего, своей комплексностью: если в случае с Ariane 5 авария случилась один раз и из-за единственной ошибки, то катастрофические последствия с Therac-25 проявлялись неоднократно в течение длительного времени, и были следствием целого спектра причин, среди которых не только вполне конкретные программистские "баги", но и дефекты в самой постановке выполнявшегося многие годы проекта.

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

Что же до системной "глобальной особенности", то к ней можно отнести принципиальную переусложненность построения мультизадачной управляющей системы. С чисто программистской точки зрения можно отметить, что для реализации тонкой синхронизации параллельных процессов был выбран механизм разделения переменных, требующий очень внимательной проработки (это именно та область, где необходимо выполнять формальное доказательство правильности алгоритма, благо соответствующие методы разработаны и могут считаться рутинными - для тех, кто ими владеет); получилось же так, что потенциально опасные в плане возникновения "race conditions" операции типа "set" и "test" не были сделаны "неделимыми" (indivisible), что и привело к наложению друг на друга их "критических секций" и - соответственно - к печальным последствиям.

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

Мифы о безопасности ПО

Катастрофы с Ariane 5 и Therac-25, сами по себе беспрецедентные, конечно же не являются уникальными. Можно привести длинный список больших и малых инцидентов в системах, относящихся к классу mission-critical, произошедших по причине дефектов в программном обеспечении и проявившихся только в режиме эксплуатации. Конечно, большинство инцидентов так или иначе расследовалось и осмыслялось. К сожалению, специфика "ответственных" систем часто такова, что это осмысление не становилось достоянием всего программистского сообщества - поэтому, неудивительно, что в разное время и в разных местах повторялись сходные ошибки. Соответственно, слишком многие приобретают специфические знания и опыт на практике, методом проб и ошибок, которые - как лишний раз показывает разобранные инциденты - обходятся дорого.

Что же может предложить в этом отношении наука? Только недавно общесистемные и общеинженерные дисциплины "Безопасность Систем" (System Safety) и "Управление Рисками" (Risk Management) начали настраиваться на ту выраженную специфику, которую имеют программно-аппаратные комплексы в контексте их разработки, эксплуатации и сопровождения. Крупнейший специалист в данной области профессор Вашингтонского Университета Нэнси Левесон (Nancy Leveson) ввела даже специальный термин Safeware, который вынесла в название своей книги [7] - пока единственной в мировой литературе, где систематически рассматриваются вопросы безопасности и рисков в компьютерных системах. В частности, в этой книге разбираются некоторые распространенные мифологические представления о ПО и связанных с ним безопасности и рисках, бытующие на фоне все более широкого использования сложных систем в потенциально опасных приложениях. Остановимся на некоторых из них.

О "дешевом и технологичном" ПО

Бытует мнение, что стоимость программно-аппаратных систем обычно меньше, чем аналоговых или электромеханических, выполняющих ту же задачу. Однако, это миф, если, конечно, не говорить о "голом" hardware и однажды оплаченном ПО, сработанном "на коленке". Стоимость написания и сертификации действительно надежного ПО очень высока; к тому же необходимо принимать во внимание затраты на сопровождение - опять же такое, которое не подрывает надежности и безопасности. Показательный пример: только сопровождение относительно простого и не очень большого по объему (около 400 тыс. слов) программного обеспечения для бортового компьютера, установленного на американском космическом корабле типа Shuttle, стоит NASA 100 млн. долл. год.

Следующий миф заключается в том, что ПО при необходимости достаточно просто модифицировать. Однако, и это верно только на поверхностный взгляд. Изменения в программных модулях легко выполнить технически, однако трудно сделать это без внесения новых ошибок. Необходимые для гарантий безопасности верификация и сертификация означают новые большие затраты. К тому же, чем длиннее время жизни программы, тем более возрастает опасность вместе с изменениями внести ошибки - например, потому, что некоторые разработчики с течением времени перестают быть таковыми, а документация редко является исчерпывающей. Оба примера - что с Ariane 5, что с Therac-25 вполне подтверждают эту точку зрения. Между тем, масштабы изменений в ПО могут быть весьма велики. Например, ПО для космических кораблей типа Shuttle [8] за 10 лет сопровождения, начиная с 1980 г., подверглось 14-ти модификациям, приведшим к изменению 152 тысяч слов кода (полный объем ПО - 400 тысяч слов). Необходимость модернизации ПО диктовалась периодическим обновлением аппаратной базы, добавлением функциональности, а также происходило по причине необходимости исправления выявленных дефектов. По оценке независимых экспертов, эти модификации поначалу не сопровождались должными процедурами по поддержке безопасности, однако, случившаяся в 1986 г. авария с кораблем Challenger, которая хотя и произошла по причинам, не связанным с ПО, послужила толчком к пересмотру всей политики NASA в области безопасности, затронув и область ПО.

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

Мысль о том, что использование имеющего длительную историю и уже зарекомендовавшего себя с положительной стороны модуля, равно как и "коробочного" продукта, дает гарантии отсутствия в нем ошибок, весьма естественна с точки зрения "здравого смысла" и способна притупить бдительность. На самом деле повторное использование программных модулей может и понизить безопасность по той простой причине, что данные модули изначально разрабатывались и отлаживались для использования в ином контексте, а спецификация обычно не дает исчерпывающего отчета о всех видах возможного поведения модуля (произошедшая с Ariane 5 авария имеет основной причиной именно повторное использование модуля с некорректной для изменившегося контекста спецификацией).

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

Можно привести еще несколько любопытных иллюстраций к проблемам, связанным с повторным использованием. Так, попытка внедрить в Англии программную систему управления воздушным движением, которая до того несколько лет успешно эксплуатировалась в США, оказалась сопряжена с большими трудностями - ряд модулей весьма оригинальным образом обращались с информацией о географической долготе: карта Англия уподоблялась листу бумаги, согнутому и сложенному вдоль Гринвичского меридиана, и получалось, что симметрично расположенные относительно этого нулевого меридиана населенные пункты накладывались друг на друга. В Америке, через которую нулевой меридиан не проходит, эти проблемы никак не проявлялись. Аналогично, успешно функционировавшее авиационное ПО, изначально написанное с неявным прицелом на эксплуатацию в северном полушарии, создавало проблемы, когда его стали использовать при полетах по другую сторону экватора. Наконец, ПО, написанное для американских истребителей F-16, явилось причиной нескольких инцидентов, будучи использованным израильской авиацией при полетах над Мертвым морем, которое, как известно, находится ниже уровня моря. Это лишний раз подтверждает мысль, что безопасность ПО нельзя оценивать в отрыве от среды, в контексте которой эксплуатируется вся система.

О "корректном" ПО

Заветная мечта (не столько программистов, сколько потребителей), чтобы в ПО не было ошибок, увы, никак не исполняется. И иллюзий на этот счет уже не осталось. Соответственно, утверждение, что тестирование ПО и/или "доказательство" его корректности позволяют выявить и исправить все ошибки, можно признать тем мифом, в который мало кто верит.

Причина очевидна. Прежде всего, исчерпывающее тестирование сложных программных систем невозможно в принципе: реально проверить только небольшую часть из всего пространства возможных состояний программы. В результате, тестирование может продемонстрировать наличие ошибок, но не может дать гарантию, что их нет. Как ядовито замечают Жезекель и Мейер [2], собственно, сам запуск Ariane 5 и явился весьма качественно выполненным тестом; правда, не каждый согласится платить полмиллиарда долларов за обнаружение ошибки переполнения.

Что же касается использования математических методов для верификации ПО в плане его соответствия спецификации, то оно (несмотря на оптимизм, особенно явный в 70-х г.) пока не вошло в практику в сколько-нибудь значительном масштабе, хотя и сейчас некоторые влиятельные специалисты продолжают утверждать, что это непременно случится в будущем. Вопрос, реалистично ли ожидать, что для систем масштаба Ariane 5 возможно выполнить полный цикл доказательства правильности всего ПО, остается открытым. Нет сомнений, однако, что для отдельных подсистем такая задача может и должна ставиться - уже приводились аргументы о полезности использования формальных методов при разработке механизмов синхронизации в Therac-25.

Формальные методы разработки - это тема специального большого разговора. Здесь же в качестве примера формального подхода, имеющего промышленные перспективы, упомянем только "B-Method" [9], получивший недавно широкое паблисити в связи с созданием ПО для автоматического управления движением на одной из линий парижского метро. Разработчик метода - Жан-Раймон Абриал (J.-R. Abrial), до того известный как создатель формального метода Z (вошедшего в учебные программы всех уважающих себя университетов), использовал идеи таких классиков, как Эдсгар Дийкстра (E.W.Dijkstra) и Тони Хоар (C.A.R.Hoare). Важно, что основанная на формализмах методология поддержана практической инструментальной средой разработки Atelie B (которая, кстати, не единственная).

Эта среда включает в себя инструменты для статической верификации написанных на B-коде компонентов и для автоматического выполнения доказательств, автоматические трансляторы из B-кода в Си и Ада, повторно-используемые библиотеки B-компонентов, средства графического представления проектов и генерации документации, гипертекстовый навигатор и аниматор, позволяющий в интерактивном режиме моделировать исполнение проекта из спецификации, и, наконец, средства по управлению проектом. При разработке ПО для метро, включавшего около 100 тысяч строк B-кода (что эквивалентно 87 тыс. строк на Ада) пришлось доказать около 28 тысяч лемм. Насколько этот подход (и аналогичные ему) будет востребован практикой, покажет будущее.

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

О "надежном" ПО

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

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

В конце 80-х гг. такая влиятельная в оборонных кругах организация как British Royal Signals and Radar Establishment сделала попытку оценки распространенности дефектов в ПО, написанном для ряда очень ответственных систем. Оказалось, что "до 10% программных модулей и отдельных функций не соответствуют спецификациям в одном или нескольких режимах работы" [7]. Такого рода отклонения были обнаружены даже в ПО, прошедшем полный цикл всестороннего тестирования. Хотя большинство обнаруженных ошибок были признаны слишком незначительными, чтобы вызвать сколь-либо серьезные последствия, все же 5% функций могли оказывать разного рода значимое негативное воздействие на поведение всей системы. Примечательно, что среди прочего авторы исследования особо упомянули выявленную в одном из модулей неназванной системы потенциальную возможность переполнения в целой арифметике, что могло привести к выдаче команды приводу повернуть некую установку не направо (как следовало), а налево. Достаточно предположить, что речь в ПО шла об управлении ориентацией пусковой ракетной установки, чтобы представить возможные последствия.

Коварство программных ошибок и в том, что они могут проявиться далеко не сразу, иногда после сотен тысяч часов нормальной эксплуатации - как реакция на вдруг возникшую специфическую комбинацию многочисленных факторов. Так, установка Therac-25 вполне корректно работала в течение нескольких лет до первого переоблучения; и последующие зафиксированные инциденты происходили спорадически в течение 2.5 лет на общем "нормальном" фоне. NASA инвестировала огромные средства и ресурсы в верификацию и сопровождение программного обеспечения для космических кораблей Shuttle. Несмотря на это, за 10-летие с 1980 г. - времени начала использования ПО - выявлено 16 ошибок "первой степени серьезности" (способных привести к "потере корабля и/или экипажа"). Восемь из этих ошибок не были обнаружены своевременно и присутствовали в коде во время полетов, хотя, к счастью, без последствий. Зато во время полетов были задокументированы проблемы, возникшие от проявившихся 12 значимых ошибок, из которых три относились ко "второй степени серьезности" ("препятствуют выполнению критически важных задач полета"). А ведь NASA имеет, может быть, самую совершенную и дорогостоящую комплексную систему процессов разработки и верификации ПО.

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

Наконец, как ни парадоксально это звучит, даже если бы компьютерные системы действительно были надежнее "традиционных", то это вовсе не обязательно означает, что они обеспечивают большую безопасность. Дело в том, что надежность ПО традиционно определяется степенью его соответствия зафиксированным в спецификациях требованиям; однако, часто бывает так, что ПО делает именно то, что ему и было предписано, и авария Ariane 5 - классический тому пример: и злополучное вычисление посторонней для полета величины горизонтального отклонения Инерциальной Платформы, и реакция на него вплоть до выведения из строя всех навигационных систем и бортовых компьютеров - все это случилось в полном соответствии с Требованиями, которые были частично унаследованы от Ariane 4 и не отражали новых реальностей. Более того, по сравнению с ошибками в коде именно спецификационные ошибки обычно ведут к более тяжелым последствиям - компетенции разработчиков ПО недостаточно для обнаружения таких ошибок. Программный комплекс - сложная система, однако реальный мир, отражаемый в спецификационных требованиях - еще более сложен и требует специальных экспертных знаний. Так что надежность ПО и его безопасность - понятия, хотя и перекрывающиеся, но не идентичные.

Фактически любая сложная программная система при определенных обстоятельствах способна вести себя неожиданно для разработчиков и/или пользователей. Вероятность такого поведения, особенно если оно может привести к тяжелым последствиям, следует реалистически оценивать и предусматривать специальные средства защиты, в том числе - уже не на уровне самого ПО, а на уровне всей системы. Собственно, авария с Ariane 5 продемонстрировала это в полной мере: реагируй система на выброшенное исключение не столь радикально, аварии бы не произошло - ведь сам полет проходил нормально, но этот "глобальный контекст" просто не принимался во внимание!

Аналогично, катастрофические последствия при использовании Therac-25 наступили не столько из-за ошибок, допущенных в ПО, сколько вследствие того, что на аппаратном уровне не было предусмотрено защиты против этих ошибок. Шлейф программных ошибок тянулся к Therac-25 от ранних версий этого сложного программно-аппаратного комплекса, но в предыдущей модели Therac-20 надлежащие аппаратные защитные механизмы были задействованы - от них отказались по соображениям достижения большей производительности. К тому же программных ошибок оказалось много: в каждом конкретном инциденте проявлялась одна из них, ее исправляли - затем следующий инцидент (уже со смертельным исходом) показывал, что исправлено не все. Безопасность - это свойство всей системы, а не только ее программного компонента.

Эпитафия

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

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

Между тем, сегодня на массовом рынке программных продуктов стандарты качества сознательно занижены (о чем мне уже доводилось писать применительно к производственной культуре Microsoft [11]). Торжествует "good enough software", когда критерии качества не имеют столь высокого приоритета, как удобство пользования, простота освоения и дешевизна - и все это в сочетании с избыточной функциональностью, пожирающей компьютерные ресурсы, и отсутствием у производителя стимула выбрасывать на рынок действительно отлаженный продукт. Весьма взрывчатая смесь. В обозримом будущем мы можем оказаться свидетелями катастрофических ситуаций, в которые попадут пользователи массовых продуктов, и, похоже, что только это способно сдвинуть ситуацию с ее нынешнего печального положения.

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

Небезынтересно в этом контексте упомянуть, что та же Microsoft пытается проникнуть на рынок "ответственных" систем; во всяком случае, она не прочь получить подряд на поставку большой партии Window NT для федеральных организаций, чья работа завязана на "обеспечение национальной безопасности". А для этого надо сертифицировать эту ОС на соответсвие одному из базовых уровней безопасности компьютерных систем С2 (в соответствии с критериями, определенными в "Оранжевой книге" Агенства Национальной Безопасности США). Хотелось бы, конечно, надеяться, что осваивая сегмент рынка с принципиально иными требованиями к продуктам, производители массового ПО поднимут планку качества и в своей традиционной вотчине. А ну как окажется наоборот?

И последнее. Все примеры в данной статье относятся к зарубежным системам. В России всегда была очень мощная отрасль mission-critical систем, выглядевшая вполне конкурентоспособно на общем мировом фоне. Отрадно, что и в нынешние турбулентные времена еще сохранились работоспособные коллективы. Однако с авариями самых разных видов и масштабов в России недостатка тоже никогда не было. Например, можно вспомнить о нескольких не столь давних авариях при пусках ракет - носителей, внешне очень похожих на катастрофу Ariane 5, да и произошедших примерно в то же время. Что нам известно об их причинах?

Эпилог

Что касается Therac-25, то после выполненной-таки в 1988 году капитальной ревизии комплекса и коррекции ряда проектных и реализационных решений, ни о каких новых инцидентах не сообщалось.

Первый после аварии запуск Ariane 5 несколько раз откладывался и состоялся 30 октября 1997 г. Между тем, летопись катастроф при запусках ракет продолжала пополняться. Так, в августе 1998 г. взорвались при старте ракета Titan-4 (производства Lockheed Martin), выводившая на орбиту американский шпионский спутник (стоимость аварии оценена в 1.2 млрд. долл.), а неделей позже - ракета Delta-3 (производитель - Boeing), убытки - "всего" 225 млн. долл. В начале сентября та же судьба постигла украинскую ракету Зенит, стартовавшую с Байконура. Виновато ли в этих авариях ПО? Может быть, может быть?

Литература
1.Jacques-Louis Lions, Доклад комиссии, ESA, CNES.

2. J.-M. Jezequel, B. Meyer "Put It in the Contract: The Lessons of Ariane", // Computer, Vol.30, No.2, January 1997, pp.129-130.

3.Бертран Мейер, "Построение надежного объектно-ориентированного ПО. Введение в Контрактное Проектирование", //Открытые системы, №6, 1998.

4. K. Garlington, "Critique of "Put it in the Contract: The Lessons of Ariane", March 1998

5. B. Nuseibeh, "Ariane 5: Who Dunnit?", //IEEE Software, Vol.14, No.3, 1997, pp.15-16.

6. N. Leveson, C. Turner "An Investigation of the Therac-25 Accidents", - Computer, Vol.26, N.7, July 1993, p. 18-41.

7. N. Leveson, "Safeware: System Safety and Computers", - Addison-Wesley, 1995

8. "An Assessment of Space Shuttle Flight Software Development processes", - Committee for Review of Ovеrsight Mechanisms for Space Shuttle Flight Software Development Processes, National Research Council, 1993

9. J.-R. Abrial, "The B-Book: Assigning Programs to Meanings", //Cambridge University Press, 1996

10.Карло Пешио, "Никлаус Вирт о Культуре Разработки ПО", //Открытые системы, №1, 1998, сc.41-44,

11.Валерий Аджиев, "MS: Корпоративная Культура Разработки ПО", //Открытые системы, №1, 1998, с.45-51.


Валерий Аджиев (valchess@gmail.com).


Последний раз редактировалось Владимир Паронджанов Воскресенье, 12 Август, 2012 12:56, всего редактировалось 2 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Суббота, 11 Август, 2012 10:27 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
ПУНКТ ДЕВЯТЫЙ

Анализ статьи Валерия Гаджиева

Цитата:
Мифы о безопасном ПО: уроки знаменитых катастроф
опубликована в журнале «Открытые системы», № 06, 1998


Ниже я привожу наиболее важные цитаты из этой статьи

Когда нужно формальное доказателство?

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

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

Получилось же так, что потенциально опасные в плане возникновения "race conditions" операции типа "set" и "test" не были сделаны "неделимыми" (indivisible), что и привело к наложению друг на друга их "критических секций" и - соответственно - к печальным последствиям.


Что может предложить наука?
Что такое Safeware?


Цитата:
Что же может предложить в этом отношении наука?

Только недавно общесистемные и общеинженерные дисциплины "Безопасность Систем" (System Safety) и "Управление Рисками" (Risk Management) начали настраиваться на ту выраженную специфику, которую имеют программно-аппаратные комплексы в контексте их разработки, эксплуатации и сопровождения.

Крупнейший специалист в данной области профессор Вашингтонского Университета Нэнси Левесон (Nancy Leveson) ввела даже специальный термин Safeware, который вынесла в название своей книги [7] - пока единственной в мировой литературе, где систематически рассматриваются вопросы безопасности и рисков в компьютерных системах.

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


Доказательство правильности ПО

Цитата:
Что же касается использования математических методов для верификации ПО в плане его соответствия спецификации, то оно (несмотря на оптимизм, особенно явный в 70-х г.) пока не вошло в практику в сколько-нибудь значительном масштабе.

Хотя и сейчас некоторые влиятельные специалисты продолжают утверждать, что это непременно случится в будущем.

Вопрос, реалистично ли ожидать, что для систем масштаба Ariane 5 возможно выполнить полный цикл доказательства правильности всего ПО, остается открытым.

Нет сомнений, однако, что для отдельных подсистем такая задача может и должна ставиться - уже приводились аргументы о полезности использования формальных методов при разработке механизмов синхронизации в Therac-25.


Формальные методы разработки и B-Method

Цитата:
Формальные методы разработки - это тема специального большого разговора.

Здесь же в качестве примера формального подхода, имеющего промышленные перспективы, упомянем только "B-Method" [9], получивший недавно широкое паблисити в связи с созданием ПО для автоматического управления движением на одной из линий парижского метро.

Разработчик метода - Жан-Раймон Абриал (J.-R. Abrial), до того известный как создатель формального метода Z (вошедшего в учебные программы всех уважающих себя университетов), использовал идеи таких классиков, как Эдсгар Дийкстра (E.W.Dijkstra) и Тони Хоар (C.A.R.Hoare).

Важно, что основанная на формализмах методология поддержана практической инструментальной средой разработки Atelie B (которая, кстати, не единственная).


Нужно доказать 28 тысяч лемм

Цитата:
Эта среда включает в себя инструменты для статической верификации написанных на B-коде компонентов и для автоматического выполнения доказательств, автоматические трансляторы из B-кода в Си и Ада, повторно-используемые библиотеки B-компонентов, средства графического представления проектов и генерации документации, гипертекстовый навигатор и аниматор, позволяющий в интерактивном режиме моделировать исполнение проекта из спецификации, и, наконец, средства по управлению проектом.

При разработке ПО для метро, включавшего около 100 тысяч строк B-кода (что эквивалентно 87 тыс. строк на Ада) пришлось доказать около 28 тысяч лемм.

Насколько этот подход (и аналогичные ему) будет востребован практикой, покажет будущее.


Безошибочное ПО (zero-defect software)

Цитата:
В то время как надежность аппаратуры может быть увеличена за счет ее дублирования, что резко нивелирует опасности от случайных сбоев, эквивалентного способа защиты от систематических программных ошибок не найдено (даже если некоторые вендоры, с подачи оторванных от практики исследователей, рекламируют методики и инструментарий, позволяющие разрабатывать "zero-defect software").

Впрочем, если бы методы производства идеального ПО существовали, то резонно предположить, что следование им потребовало бы нереалистично большого количества ресурсов и времени.

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


Ошибки в спецификациях — серьезная проблема

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

Дело в том, что надежность ПО традиционно определяется степенью его соответствия зафиксированным в спецификациях требованиям; однако, часто бывает так, что ПО делает именно то, что ему и было предписано, и авария Ariane 5 - классический тому пример.

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

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

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

Так что надежность ПО и его безопасность - понятия, хотя и перекрывающиеся, но не идентичные.


ВЫВОДЫ

1. Доказательство правильности программ — чрезвычайно важный и полезный метод.

2. Но это трудоемкий метод, требующий значительных затрат труда, времени и финансовых ресурсов.

3. По причине дороговизны метода, доказательство правильности программ, по-видимому, будет проводиться не во всех случаях, а только в наиболее ответственных (critical) системах. Там, где это обосновано либо экономически, либо вопросами безопасности.

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


Последний раз редактировалось Владимир Паронджанов Воскресенье, 12 Август, 2012 13:02, всего редактировалось 5 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Суббота, 11 Август, 2012 11:10 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Ну, и так понятно, что внимание привлечено правильно... спасибо за полные версии статей! :)
Именно на эти вещи указывал в связи с оценкой эргономики редакторов, в частности, здесь:
Владислав Жаринов в viewtopic.php?p=57746#p57746 писал(а):
...
А главное - что никаких "отклонений от маршрута" схема не предполагает. Изучи Ты-среду - и ты в порядке :) А поможет ли она, скажем, уйти от "наивно-отладочного" подхода - если человек готов принять "убедительный"? Большой вопрос с учётом замечаний, сделанных во всех упомянутых постах... И позиция самого Тышова известна:
Геннадий Тышов в viewtopic.php?p=46802#p46802 писал(а):
...
На форуме преподавателей много, но как то пишут о программировании, игнорируя этапы постановки задачи, декомпозиции и создания алгоритма, о Драконе молчат, посылают читать Дейкстру, успешно борются с партизанами и ополченцами, навязывают доказательное программирование, с отечественными языками 1С не знакомы...
А как Вам, Геннадий Николаевич, примеры из Карпова (с. 16-17) - когда пациентов посылали под прибор Therac-25, который мог дать им дозу радиации в 100 раз больше лечебной? или когда снаряжённый боевой робот "вдруг" ожил? И "бездоказательные" отладка с тестированием избежать этого не помогли? И как с тем, чтобы на этапах постановки и спецификации задачи дать возможность удобно работать с документом не только тем, кто будет "бороться за освоение"?.. И визуализировать своё знание не только в части, покрываемой ДРАКОНом (создания алгоритма)?

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

Аджиев пишет про всё то же самое - и поощрение опасных инноваций. Здесь:
Цитата:
..., когда критерии качества не имеют столь высокого приоритета, как удобство пользования, простота освоения и дешевизна - и все это в сочетании с избыточной функциональностью, пожирающей компьютерные ресурсы, и отсутствием у производителя стимула выбрасывать на рынок действительно отлаженный продукт. Весьма взрывчатая смесь. В обозримом будущем мы можем оказаться свидетелями катастрофических ситуаций, в которые попадут пользователи массовых продуктов, и, похоже, что только это способно сдвинуть ситуацию с ее нынешнего печального положения.
...
Как сдвинуть? А это уже к Голубицкому: viewtopic.php?p=71257#p71257. Вот вам и предпосылки к луддизму и обскурантизму... создаваемые самими ИТ-шниками...
И пренебрежение целостным пониманием задачи:
Цитата:
... по сравнению с ошибками в коде именно спецификационные ошибки обычно ведут к более тяжелым последствиям - компетенции разработчиков ПО недостаточно для обнаружения таких ошибок. Программный комплекс - сложная система, однако реальный мир, отражаемый в спецификационных требованиях - еще более сложен и требует специальных экспертных знаний. Так что надежность ПО и его безопасность - понятия, хотя и перекрывающиеся, но не идентичные.

Фактически любая сложная программная система при определенных обстоятельствах способна вести себя неожиданно для разработчиков и/или пользователей. Вероятность такого поведения, особенно если оно может привести к тяжелым последствиям, следует реалистически оценивать и предусматривать специальные средства защиты, в том числе - уже не на уровне самого ПО, а на уровне всей системы. Собственно, авария с Ariane 5 продемонстрировала это в полной мере: реагируй система на выброшенное исключение не столь радикально, аварии бы не произошло - ведь сам полет проходил нормально, но этот "глобальный контекст" просто не принимался во внимание!
...
И ведь сколько тот же Усов напоминал об этом... вот хотя бы сейчас:
<...> речь только о том, что не поняв сути задачи браться за решение чего-то там... не стоит.
Но ведь очень часто мы просто не понимаем сути задачи, пока не возьмёмся её решать. Постоянно возникают изменения задачи, и вчерашнее её понимание оказывается неполным, а то и вовсе не верным...
Что же делать в этом случае?
Думать над задачей, над тем, откуда она взялась, почему сформулирована именно так. Но слово "решение" здесь имеет два смысловых оттенка. Можно решать задачу без понимания сути, но решить её таким образом нельзя. (Я говорил о втором, то есть, о том, что не поняв сути задачи, браться за решение не стоит, потому что решить задачу не получится).
Но моё высказывание не говорит о том, что думать над задачей не надо. Надо. Это вопрос "частного" и "общего". Частные решения можно получить, не понимая сути, но общего решения так получить нельзя.
И у Лаврова можно видеть аналогичные мысли - обсуждалось здесь: viewtopic.php?p=72973#p72973. Кстати, он тоже это в связи с тем, что возможности верификации ограничены - но тем не менее верифицировать надо...

И о тех же контрактах Мейера Вы (словами Аджиева) напомнили своевременно - только вот надо реализовать их граф-запись... А чтобы было что записывать - опять же думать над задачей...

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Суббота, 11 Август, 2012 12:28 

Зарегистрирован: Понедельник, 09 Ноябрь, 2009 17:29
Сообщения: 904
Откуда: Россия, Питер
Не могу понять, к чему весь этот массив информации?

Да, всё плохо, ракеты падают, а мэйнстримгеры делают опасные поделки и не хотят : ) доказательно программировать.

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

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

P.S. Со своей стороны, я мог бы иллюстрировать такой пример дракон-схемами : ) (если они потребуются)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Суббота, 11 Август, 2012 12:42 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Дык вот об чём и речь... :wink:

Во-первых - что эта формулировка:
Владимир Паронджанов писал(а):
... метод Дейкстры (метод доказательного программирования) в одиночку не справляется с серьезными проблемами, возникающими в ходе развития науки и практики (сomputer science и практики программирования).

Этот метод следует дополнить другими методами.
Какими?

В частности, методами когнитивной эргономики, используемыми в языке ДРАКОН.

Поскольку важной проблемой является СЛОЖНОСТЬ, то желательно уменьшить сложность с помощью когнитивно-эргономических методов.
- в таком виде не проясняет суть дела. Точнее будет:
Цитата:
Традиционно принятую текстовую форму изложения/представления/записи этого метода <Дейкстры[-Хоара etc]> следует дополнить другими формами.

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

В частности, формой схем, строго упорядоченных - например, по шампур-методу. Такие схемы используются в языке ДРАКОН.


Почему так (примерно)? Да потому, что ведь не развитие (усовершенствование, дополнение) методов доказательного программирования предлагается. Т.е. не собственно то, что Эдуард назвал "простые способы доказательства программ" и/или "культура доказательного программирования". А именно "способы проще разбираться в доказательствах программ" и/или "легче прививать себе (и другим) культуру доказательного программирования"...

А если формулировать столь расплывчато - то возникнет ситуация аналогичная этой:
Возможно, grosborn решил, что ВП говорил о применении ГРАФИТ-ФЛОКСа на самом космодроме в Куру? Там действительно использовалась другая система разработки — можно узнать из этой статьи.
...
Нет, мои претензии были другого плана.
...
... имеет право приписывать себе эту заслугу и неоднократное участие в разных космических программах?
А, понял. Т.е., что непосредственно в критикуемом посте вот это:

ВП> ПРИМЕНЕНИЕ ЯЗЫКА ДРАКОН В РАКЕТНО-КОСМИЧЕСКОЙ ОТРАСЛИ

ВП>Язык ДРАКОН успешно используется во многих космических программах:

ВП>{• <имя-изделия>[(имя-проекта)]}

ВП>Космодромы:

ВП>{название-космодрома}

— следовало бы изложить более развёрнуто — как в этом посте:

ВП>Мои слова «Технология разработки алгоритмов и программ Графит-Флокс» успешно применяется при разработке системы управления разгонным блоком Фрегат (который запускается, в частности, с космодрома Kuru во Французской Гвиане) полностью соответствуют действительности.

Т.е. что с таких-то площадок по таким-то проектам запускаются изделия, где применяется ГРАФИТ-ФЛОКС либо в целом (как можно понять — из уже эксплуатируемых это "Протон"), либо в таком-то субизделии (в данном случае — РБ как части носителя). А изложенное так, как выше, Вы считаете, можно понимать так, что ГРАФИТ-ФЛОКС применяется в целом на проекте и/или площадке? Возможно, Вы и правы...

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

Заметим, что уже в последующем Вы уточнили это:
VladimirParondzhanov в http://forum.ru-board.com/topic.cgi?for ... ic=13309#9 писал(а):
...
Космодромы (с которых запускаются перечисленные ракеты и разгонные блоки) :
{- название-космодрома}
...
- а тут снова такого же рода "ловушка"...


Последний раз редактировалось Владислав Жаринов Суббота, 11 Август, 2012 13:32, всего редактировалось 1 раз.

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Суббота, 11 Август, 2012 12:54 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
Эдуард Ильченко писал(а):
Не могу понять, к чему весь этот массив информации?

Уважаемый Эдуард!

Этот массив информации (состоящий из 8 пунктов и озаглавленных как ПУНКТ ПЕРВЫЙ ... ПУНКТ ВОСЬМОЙ) является ответом на следующее замечание Ильи Ермакова.

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


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

А, например, методы Дейкстры или формальной верификации типа model-checking позволяют убедиться в том, что поведение программы соответствует спецификации требований.
По моему мнению, замечание Ермакова является интересным и очень глубоким. Поэтому я решил дать Илье Евгеньевичу ответ в развернутой и очень подробной форме.

Мой ответ (который, кстати, еще не закончен) Вы обозначили как "массив информации".


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Суббота, 11 Август, 2012 14:01 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Ну, собственно Ваш ответ, видимо, здесь (понятно, что выводы м.б. изменены):
Владимир Паронджанов писал(а):
ПУНКТ ВОСЕМЬ
Анализ статьи Валерия Гаджиева
Цитата:
Мифы о безопасном ПО: уроки знаменитых катастроф
опубликована в журнале «Открытые системы», № 06, 1998

Ниже я привожу наиболее важные цитаты из этой статьи
...
ВЫВОДЫ
1. Доказательство правильности программ — чрезвычайно важный и полезный метод.
2. Но это трудоемкий метод, требующий значительных затрат труда, времени и финансовых ресурсов.
3. По причине дороговизны метода, доказательство правильности программ, по-видимому, будет проводиться не во всех случаях, а только в наиболее ответственных (critical) системах. Там, где это обосновано либо экономически, либо вопросами безопасности.
4. Решение о применении доказательного программирования, как правило, принимается не на индивидуальном уровне, а на уровне топ-менеджеров корпораций, которые отдают себе отчет о размере предстоящих расходов. Топ-менеджеров, которые одновременно принимают решение о выделения для этой работы значительных дополнительных финансовых средств.

А Эдуард, как можно понять, прежде всего хотел узнать:
Ильченко Эдуард писал(а):
Это предложение к поиску простых способов доказательства программ? Похоже, это дело не простое : ) Или это предложение прививать себе (и другим) культуру доказательного программирования? Но тогда нужна некоторая методика и средства.
- что и другим, думаю, интересно...

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Суббота, 11 Август, 2012 14:31 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Ну и теперь - что во-вторых вытекает из слов Эдуарда:
Ильченко Эдуард в viewtopic.php?p=73808#p73808 писал(а):
...
Или это предложение прививать себе (и другим) культуру доказательного программирования? Но тогда нужна некоторая методика и средства.

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

P.S. Со своей стороны, я мог бы иллюстрировать такой пример дракон-схемами : ) (если они потребуются)
- если их связывать с объективными потребностями тех или иных работающих в сфере ИТ.
Например, один из вполне нейтрально и интересно обсуждающих техноязык и шампур-метод на РСДН по другому поводу сказал (курсив мой):
...
Буквально единицы лет назад в академических кругах научились делать "суперкомпиляторный анализ" императивного кода, до этого вообще был детский сад, представляющий из себя чуть продвинутую бета-редукцию над ФП.
Почему так медленно идёт движение в этой области? Любое ветвление в программе — это лишний множитель комбинаторного кол-ва вариантов исполнения, то бишь сложность анализа от сложности алгоритма — степенная. Современные компиляторы проводят анализ в самых простейших случаях до 10 уровней глубины, в сложных — дай бог 2-3. Исходники gcc открыты, можно посмотреть самому.
Понимаешь, из-за степенной природы происходящего, наблюдаемая вроде бы неплохая геометрическая прогрессия в росте мощщи железа ничего кроме пессимизма не вызывает. Ни ты, ни я не увидим "золотого века IT". Например, gcc в последних версиях медленно но верно догоняет MS VC по эффективности конечного образа. Именно поэтому gcc таки относительно скоро нагонит MSVC, что он его настигнет прямо в точке насыщения возможностей, выжимаемых из машин разработчиков.
Это я всё к тому, что в течении ближайших 10-20 лет никакое самое вылизанное ФП по эффективности не догонит аналогично вылизанный императив даже близко.
На плюсах я сижу неплотно лет 20, плотно более 15 лет. Все их достоинства и недостатки собственной задницей ощущал не раз, так же как знаю как с ними бороться. Я могу выжимать из машины максимум, умею это и люблю. Помимо выжимания, есть определенные способности находить нетривиальные ошибки даже в чужом коде. Считай, у меня в сформировалась некая статистика по причинам всех этих ошибок.
Самые популярные, ес-но, не те ярлыки, которые навешивают на плюсы — типа выхода за границы диапазонов. Самые популярные сегодня — это неверное представление о работе собственных многопоточных программ, иногда откровенные гонки. Причем, эти гонки не из-за непоходимости разработчиков, ес-но, а из-за всего здесь обсуждаемого, из-за скрытого неявного поведения/зависимостей, которое в реальном коде образуется немыслимыми сочетаниями сценариев. Обычный разработчик уже на глубину более 3-х уровней зависимостей смотрят с ооочень большим трудом и не часто. В идеале хотелось бы 1 уровень. И мне/нам обсуждаемые языковые ср-ва помогут заметно сэкономить на отладке. А если брать предлагаемую банальную иммутабельность — наоборот, добавит работы и снизит эффективность решения.
Теперь сравните с подходом проверки моделей... и с другими родами методов верификации...
Что мы видим? Что как предмет "доказательного программирования конкретной реальной задачи" рассматривается прежде всего верификация взаимодействия совместно протекающих алгопроцессов. Т.е. доалгоритмической модели деятельности. И то же самое как первоочередная потребность видно из обсуждения Оберона на РСДН... и не только там...
Надо напоминать, в какой ветке мы обсуждали соответствующие шампур-средства? и к чему пришли на данный момент?.. :)

А для чего в первую очередь были созданы средства проверки моделей? Правильно - для того же (например, Spin, UPPAAL, Kronos)...

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

Но есть человек, который постарался исследовать различные средства граф-записи систем алгопроцессов на практике (пусть эмпирически). Это PSV100. Совсем недавно он опубликовал свои очередные результаты: http://www.rsdn.ru/forum/philosophy/485 ... ?tree=tree. Как видим, он ставит в ряд вместе с мультишампур-схемами также модифицированные Р-схемы...

Реальная же задача давно находится здесь: viewtopic.php?p=66824#p66824. Можно описывать - но надо понимать - в расчёте на какой род методов верификации?..


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Воскресенье, 12 Август, 2012 13:11 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
Подытожу сказанное выше в моих сообщениях.
И дам заключительный ответ на критическое замечание Ильи Ермакова
Илья Ермаков в сообщении viewtopic.php?p=73786#p73786 писал(а):
Владимир Паронджанов писал(а):
Практическая ценность состоит в том, что управляющие операторы алгоритма, представленные в виде шампур-схемы оказываются безошибочными, гарантированно правильными.

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


Уважаемый Илья Евгеньевич!

Это не совсем так.

1. Дракон-конструктор обеспечивает НЕ то же самое, что синтаксический анализатор обычных языков.

2. Дракон-конструктор делает БОЛЬШЕ, чем синтаксический анализатор обычных языков. Может быть, ненамного, но все таки БОЛЬШЕ.

3. Разница состоит в следующем:

      — Синтаксический анализатор глуп. Он позволяет обнаружить синтаксическую ошибку. Но он не может ее исправить. Единственное, что он может, это сообщить ЧЕЛОВЕКУ: есть ошибка и указать место ее локализации.

      — После этого человек должен прочитать листинг компилятора и понять этот листинг. Для этого он должен быть программистом, то есть человеком, имеющим квалификацию и умеющим читать такие сложные вещи, как листинг компилятора.

      — После этого человек (программист) должен вызвать исходный текст своей программы и найти в исходном тексте место с ошибкой. Затем внести исправление в исходный текст.

      — После этого человек должен еще раз скомпилировать программу и убедиться, что ошибок нет.

      (Если я что-то неправильно сказал, просьба меня поправить).

В случае дракон-конструктора НИЧЕГО ЭТОГО ДЕЛАТЬ НЕ НУЖНО. Потому что дракон-конструктор, в отличие от синтаксического анализатора, «умен». И не позволяет делать ошибки визуального синтаксиса.

Он умен потому, что в его внутренних алгоритмах использован метод доказательного программирования — исчисление икон.

Я полностью согласен со словами Степана Борисовича Митькина:

Цитата:
Разница между идеальным ДРАКОН-конструктором и компилятором обычного текстового языка вот в чём:

      — В случае с текстовой программой человек может написать всё, что угодно. А синтаксический анализатор потом проверит текст и укажет на ошибки.

      — В случае с конструктором человек не может нарисовать неправильную схему. Конструктор не даст.

      — Поэтому и проверять потом ничего не надо.

Концепция ДРАКОН-конструктора такова:

      1) В каждый момент времени на листе находится правильная ДРАКОН схема.

      2) Действия, разрешённые конструктором, приводят к изменённой, но тоже правильной ДРАКОН-схеме.

      3) То есть мы как бы едем по рельсам и можем переключать стрелки.

      4) Это даёт гарантию, что мы никогда не окажемся в чистом поле без дороги. Всегда будем на какой-нибудь станции.
Вопрос. Почему дракон-конструктор умнее, чем синтаксический анализатор?
Ответ. Потому что использован метод доказательного пограммирования.

В заключение повторю сказанное здесь:
viewtopic.php?p=73747#p73747

Цитата:
1. Главной задачей дракон-конструктура является содействие безошибочному проектированию алгоритмов.

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

3. Но! Дракон-конструктор может и должен предотвращать и исключать ошибки в графике алгоритмов (ошибки графического синтаксиса). Эти ошибки должны быть исключены на 100%. Исключены автоматически. Не человеком, а автоматом, то есть дракон-конструктором.

4. Автомат должен немедленно пресекать попытку пользователя сделать ошибку. Давить ее в зародыше. Это означает, что дракон-конструктор не должен потакать пользователю, который по неразумению пытается совершить ошибочные действия. Автомат должен запрещать такие действия.

5. Существующие дракон-конструкторы не в полной мере решают свою главную задачу.

6. Главная задача должна рассматриваться как стратегическая цель.
Эта цель вполне достижима. И к ней следует настойчиво двигаться.

7. Пользователям нужен дракон-конструктор, который гарантирует безошибочную графику дракон-схем. Графику, безошибочную на 100%.

8. Требование удобства (то есть требование эргономичности) само собой. Для многих оно на первом месте. И об этом тоже нельзя забывать.


И еще добавлю сказанное здесь:
viewtopic.php?p=73789#p73789

Цитата:
ВЫВОДЫ

1. Для уменьшения вероятности ошибок в управляющих операторах в языке ДРАКОН используются синтаксические и семантические средства.

2. Синтаксические средства реализованы в дракон-конструкторе, который гарантирует невозможность ошибок визуального синтаксиса.

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

4. Таким образом, имеет место разумное сочетание метода доказательного программирования (исчисление икон) и специальных методов повышения надежности алгоритмов, реализованных в языке ДРАКОН.


Но это не все. Кроме того, Илья Ермаков в том же сообщении viewtopic.php?p=73786#p73786 в последнем абзаце на писал(а):

А, например, методы Дейкстры или формальной верификации типа model-checking позволяют убедиться в том, что поведение программы соответствует спецификации требований.


Уважаемый Илья Евгеньевич!

Ответ я дал в девяти пунктах, обозначенных как ПУНКТ ПЕРВЫЙ — ПУНКТ ДЕВЯТЫЙ. Начало см. здесь:
viewtopic.php?p=73793#p73793

ПУНКТ ПЕРВЫЙ
viewtopic.php?p=73794#p73794
Эдсгер Вибе Дейкстра. Смиренный гений программирования Автор: Алексей Вторников

ПУНКТ ВТОРОЙ
viewtopic.php?p=73795#p73795
Цитата из статьи Алексея Вторникова.

ПУНКТ ТРЕТИЙ
там же
Мистическая тайна современного программирования

ПУНКТ ЧЕТВЕРТЫЙ viewtopic.php?p=73799#p73799
О книге Эдсгера Дейкстры "Дисциплина программирования"

ПУНКТ ПЯТЫЙ
viewtopic.php?p=73800#p73800
Вернемся к статье Алексея Вторникова, опубликованной в журнале "Системный администратор". И повторим вытекающие из нее вопросы.

ПУНКТ ШЕСТОЙ
Там же
В чем разгадка Великой Тайны? В том, что метод Дейкстры (метод доказательного программирования) в одиночку не справляется с серьезными проблемами

ПУНКТ СЕДЬМОЙ
viewtopic.php?p=73802#p73802
Статья Валерия Аджиева Часть 1
Мифы о безопасном ПО: уроки знаменитых катастроф

ПУНКТ ВОСЬМОЙ
viewtopic.php?p=73803#p73803
Статья Валерия Аджиева Часть 2
Мифы о безопасном ПО: уроки знаменитых катастроф

ПУНКТ ДЕВЯТЫЙ
viewtopic.php?p=73805#p73805
Анализ статьи Валерия Гаджиева
Наиболее важные цитаты

Из этих девяти пунктов следуют Выводы, указанные здесь:
viewtopic.php?p=73805#p73805

Цитата:
ВЫВОДЫ

1. Доказательство правильности программ — чрезвычайно важный и полезный метод.

2. Но это трудоемкий метод, требующий значительных затрат труда, времени и финансовых ресурсов.

3. По причине дороговизны метода, доказательство правильности программ, по-видимому, будет проводиться не во всех случаях, а только в наиболее ответственных (critical) системах. Там, где это обосновано либо экономически, либо вопросами безопасности.

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


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

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

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


Последний раз редактировалось Владимир Паронджанов Воскресенье, 12 Август, 2012 15:52, всего редактировалось 7 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Воскресенье, 12 Август, 2012 13:27 

Зарегистрирован: Понедельник, 09 Ноябрь, 2009 17:29
Сообщения: 904
Откуда: Россия, Питер
Владислав Жаринов писал(а):
Реальная же задача давно находится здесь: viewtopic.php?p=66824#p66824. Можно описывать - но надо понимать - в расчёте на какой род методов верификации?..

Об этой задаче я помню : )
Покопаться в ней было бы интересно. См. здесь.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Воскресенье, 12 Август, 2012 16:06 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Да уж покопались... было интересно посмотреть Вашу форум записи... на данный момент - бегло. Тем не менее уже есть вопросы в контексте топика этой ветки (потому здесь):

1. Предполагается, что в Вашем синтаксисе модели можно отделить вещи, связанные с множественностью "рабочих точек" (сеть работ) от вещей, требующих их единственности (алгоритмы работ)? В таком кратком эскизе это не ясно...

2. Т.к. мы о верификации - есть мысли о проверочных утверждениях (требованиях "формального ТЗ")? Уточню - в зависимости от рода верификации это д.б. для:
    * дедуктивной - правила "преодоления языковых конструктов" - сиречь, суждения (силлогизмы) об операторах (как у Кауфмана и Лаврова);
    * проверочной - утверждения о желательных свойствах модели - *TL-формулы, сводимые к never-алгопроцессам (стало быть, записываемым также в форме визуалов) - как у Карпова.


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

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


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

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


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

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