На чем пишется софт для КА?

Автор hudvin, 06.05.2009 15:28:09

« предыдущая - следующая »

0 Пользователей и 1 гость просматривают эту тему.

Васил Жеков

Цитата
ЦитатаНемного не в тему, но для Боингов ПО написано на С, процессор PowerPC.

А в МО США используется Ада. И что?  Ничего.. Вообще эти битвы стороников разных языков програмирования так умиляют... На мой взгляд идеальных языков нет и быть не может...
Вообще когда я изучал различные языки програмирования больше всего меня впечатлил Пролог.. Дейстительно вериться, что на его основе можно создать подобие искуственого интелекта.

Искуственой интелект можно на любом язике создать, в обшем-то Пролог ничего оссобенное не представляет - back-tracking и все.
Nula dies sine linea.

Александр Куприянов

Цитата
ЦитатаНемного не в тему, но для Боингов ПО написано на С, процессор PowerPC.

А в МО США используется Ада. И что?  Ничего.. Вообще эти битвы стороников разных языков програмирования так умиляют... На мой взгляд идеальных языков нет и быть не может...
Вообще когда я изучал различные языки програмирования больше всего меня впечатлил Пролог.. Дейстительно вериться, что на его основе можно создать подобие искуственого интелекта.

Судя по описанию, HAL сформирован из двух соображений:
1.Надежности, в том числе отсутствии двусмысленностей.
2.Понятности готового кода неспециалисту, что, между прочим, связано с п.1.

Ну и процедуры жизненного цикла ПО выстроены с банковской аккуратностью и требовательностью.

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

Вадим Семенов

Вообще языки программирования бывают более или менее уязвимые к производству багов. Но титаническим усилиями, многократной проверкой и каменной задницей можно сделать безошибочный код на любом языке.
Гипотеза о боге дает ни с чем не сравнимую возможность абсолютно все понять, абсолютно ничего не узнавая.
А. и Б. Стругацкие "Пикник на обочине".

bsdv

Цитата
Цитата
ЦитатаНемного не в тему, но для Боингов ПО написано на С, процессор PowerPC.

А в МО США используется Ада. И что?  Ничего.. Вообще эти битвы стороников разных языков програмирования так умиляют... На мой взгляд идеальных языков нет и быть не может...
Вообще когда я изучал различные языки програмирования больше всего меня впечатлил Пролог.. Дейстительно вериться, что на его основе можно создать подобие искуственого интелекта.

Судя по описанию, HAL сформирован из двух соображений:
1.Надежности, в том числе отсутствии двусмысленностей.
2.Понятности готового кода неспециалисту, что, между прочим, связано с п.1.

Ну и процедуры жизненного цикла ПО выстроены с банковской аккуратностью и требовательностью.

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

Мне трудно понять, зачем надо было выдумывать специальный язык. Наверное, это было модно в 70-е. Также мне кажется, что надежность ПО, написанного на стандартном С для того же B787 или A380, на порядок выше шаттла (не в обиду будет сказано, просто риски несоизмеримы). А вот насчет процедур ЖЦ ПО согласен на 100%, бюрократия страшенная :D . По другому сертификацию не пройдешь.

Александр Куприянов

Цитатаbsdv пишет:
 
ЦитатаAllex пишет:
 
Цитата
ЦитатаНемного не в тему, но для Боингов ПО написано на С, процессор PowerPC.

Мне трудно понять, зачем надо было выдумывать специальный язык. Наверное, это было модно в 70-е. Также мне кажется, что надежность ПО, написанного на стандартном С для того же B787 или A380, на порядок выше шаттла (не в обиду будет сказано, просто риски несоизмеримы). А вот насчет процедур ЖЦ ПО согласен на 100%, бюрократия страшенная :D . По другому сертификацию не пройдешь.

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

yos

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

yos

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

bsdv

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

Дык, потому языки и развиваются, охватывая новые предметные области. С++, С#, Matlab, Simulink, ObjectARX, MFC - что там еще программистская братия выдумает? В данном конкретном случае у С есть неоспоримое преимущество с названными выше языками, он известен многим :D . А из многих всегда легче выбрать лучших :D . А, собственно говоря, именно лучшие и задают безукоризненость кода, а не  язык сам по себе.

yos

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

hudvin

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

yos

Нее, тесты это фигня. Существуют формальные(!) методы проверки или даже построения программ из их спецификаций. Всякие там специальные логики, например. Самая известная, но одновременно и слишком простая -- логика (исчисление) Хоара.
Соответственно существуют программные системы для формального построения программ. Грубо говоря, инженер составляет спецификацию, манипулирует нею, а в конце, опять таки грубо, нажимает на кнопочку и получает программу на Модуле-2 или Аде. Но не путать с модельно-ориентированным программированием, где программы тоже генерируются!
Конечно, эти методы гарантируют не всё и применяются для изолированных но критичных вещей, алгоритмы там всякие и прочее.
Так вот, формализовать, например, указатели очень сложно. В результате, сложно создать систему (формальную, а также её программную реализацию), которая бы смотрела на программу с указателями и выдавала результат "нет проблем" или "тут указатель в ничто" и подобное. Такие системы есть, но они не формальные, то есть не всегда могут то, что должны делать и/или не всегда выдают правильные результаты.

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

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

hudvin

ясно, разница конечно коренная.  Я спутал с верификацией/тестированием в функциональном программмировании.

bsdv

Что-то мне кажется, что формальные методы не дадут оптимального кода - ни по быстродействию, ни по объемам памяти.

Not

ЦитатаЧто-то мне кажется...
перекреститесь немедленно!  :lol:

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

bsdv

Цитата
ЦитатаЧто-то мне кажется...
перекреститесь немедленно!  :lol:

 :D  :D  :D

yos

ЦитатаЧто-то мне кажется, что формальные методы не дадут оптимального кода - ни по быстродействию, ни по объемам памяти.
Е-е, как бы так сказать, одно не мешает другому. Формальные методы не генерируют за человека программы. Хотя для функционального программирования есть, действительно, метод основаный на лямбда исчислении, который позволяет извлечь программу из спецификации. Часто, такая программа будет действительно неоптимальной.

Но в большинстве своём, подчеркну, формальные методы дают возможность получить ответ на вопрос "делает ли моя программа то, что она должна делать?", а не каким-то чудесным способом дают готовую программу. Так что "оптимальность" тут ни при чём.

yos

Цитатанаписание оптимальных программ сродни решению задач мат. программирования...
Думаю, что под "оптимальностью" понимается, сложность алгоритма. Например, я говорю вам "найдите в словаре слово пионер". Вы просматриваете каждое слово по порядку: сложность алгоритма линейная. А кто-то другой смотрит в середину словаря, решает смотреть ли дальше и где, слева от середины или справа: сложность логарифмическая. Первый алгоритм менее "оптимальный" чем второй.

Вадим Семенов

ЦитатаТак вот, формализовать, например, указатели очень сложно. В результате, сложно создать систему (формальную, а также её программную реализацию), которая бы смотрела на программу с указателями и выдавала результат "нет проблем" или "тут указатель в ничто" и подобное.
Да нет, все решаемо. Другое дело, что ни в С++, ни в Джаве, ни в C# нет для этого необходимого инструментария. В результате в больших проектах (даже без "космических" требований по надежности!) приходится в начале каждой процедуры выполнять проверку всех указателей на ноль. Потому что даже если сейчас требованеие ненулевых указателей выполняется, то в дальнейшем где-то в другом месте программы другим человеком поменяется спецификация, на вход придет ноль и получится креш. А можно было бы иметь специальный тип указателей, котрые не могут быть рвны нулю. В этом стучае мы получим сообщение еще на стадии компиляции программы, что код стал некорректным. И так же по многом другим типовым источникам ошибок. К сожалениею, существующие языки программирования на безошибочное программирование совершенно не заточены. Если брать те же указатели, в распространенных языках специфицировать, что такой-то указатель не может быть нулем невозможно. И когда действительно требуется безошибочность приходится путем титанических усилий выверять код по спецификации. Вручную, очень трудоемко. Хотя это вполне мог бы делать компилятор при наличии специального языка программирования.
Гипотеза о боге дает ни с чем не сравнимую возможность абсолютно все понять, абсолютно ничего не узнавая.
А. и Б. Стругацкие "Пикник на обочине".

Not

Цитата
ЦитатаТак вот, формализовать, например, указатели очень сложно. В результате, сложно создать систему (формальную, а также её программную реализацию), которая бы смотрела на программу с указателями и выдавала результат "нет проблем" или "тут указатель в ничто" и подобное.
Да нет, все решаемо. Другое дело, что ни в С++, ни в Джаве, ни в C# нет для этого необходимого инструментария. В результате в больших проектах (даже без "космических" требований по надежности!) приходится в начале каждой процедуры выполнять проверку всех указателей на ноль. Потому что даже если сейчас требованеие ненулевых указателей выполняется, то в дальнейшем где-то в другом месте программы другим человеком поменяется спецификация, на вход придет ноль и получится креш. А можно было бы иметь специальный тип указателей, котрые не могут быть рвны нулю. В этом стучае мы получим сообщение еще на стадии компиляции программы, что код стал некорректным. И так же по многом другим типовым источникам ошибок. К сожалениею, существующие языки программирования на безошибочное программирование совершенно не заточены. Если брать те же указатели, в распространенных языках специфицировать, что такой-то указатель не может быть нулем невозможно. И когда действительно требуется безошибочность приходится путем титанических усилий выверять код по спецификации. Вручную, очень трудоемко. Хотя это вполне мог бы делать компилятор при наличии специального языка программирования.
А причем тут нулевые указатели? Это лишь частный случай проблемы. Не менее серьезная проблема состоит в слабой типизации и в адресной арифметике. Иначе говоря, возможность переместить указатель куда угодно и что угодно туда записать. Что делает верификацию принципиально неразрешимой (диапазон смещения указателя может зависеть от входных данных недоступных на момент верификации. Все что можно сделать в данной ситуации - построить упрощенную формальную модель программы, доказать что она в точности отображается в реальный код и вести анализ на этой модели. Что безусловно лучше, чем ничего, но не безгрешно, увы.

Not

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