Выбор языка программирования для высоких систем целостности
Какие языки программирования являются хорошим выбором для Высоких Систем Целостности?
Примером плохого выбора является Java, поскольку существует значительный объем кода, который недоступен программисту. Я ищу примеры языков блочно-структурированных, со строгим контролем типов, где программист ответственен за 100% кода, и существует как можно меньше интерференции от вещей как JVM.
Компиляторы, очевидно, будут проблемой. Язык должен иметь полное и однозначное определение.
Править: Высокие Системы Целостности являются обобщающим понятием для Безопасности Критические Системы и т.д., Защищенные системы, и т.д.
РЕДАКТИРОВАНИЕ РЕДАКТИРОВАНИЯ: Я хочу примеры языков, которые не являются под влиянием платформы, которая приведет к тому же результату независимо от компилятора и которая полностью определяется.
7 ответов
Подмножество SPARK в Ada было бы очень хорошей отправной точкой. SPARK наследует все хорошие функции Ada (строгая типизация, легкость чтения, ...) с дополнительным преимуществом отсутствия неопределенных функций, что означает, что все программы SPARK будут делать одно и то же, независимо от того, какой компилятор Ada использовался для скомпилируйте это.
SPARK можно использовать без среды выполнения. Аналогично для языка Ада (см. Прагму No_Runtime).
Конечно, с такими языками, как SPARK, вы жертвуете гибкостью в пользу безопасности (или безопасности).
Я не совсем понимаю, что это за «система высокого уровня целостности». Предполагая, что вы имеете в виду «систему, которая оставляет меньше места для ошибок», я предлагаю вам взглянуть на ML и его производную от ООП, O'CaML . ML был разработан для минимизации ошибок типов. В ML нет ошибок приведения или нулевых указателей - вы просто не можете их закодировать. Ему также не хватает динамических функций, что делает его менее крутым, но более безопасным.
Сказав это, ML далеко не доставляет удовольствие хакерам; Это несколько громоздкий язык. Но если вы предпочитаете работать на час больше и получать на одно исключение меньше, это правильный выбор.
Насколько высокий уровень интеграции вы ищете?
Галуа в Портленде, штат Орегон построили очень успешный бизнес на системах с высокой степенью целостности, написанных на Haskell . Я считаю, что они делают упор на целостность и безопасность данных. Несколько удивительно выполнять такого рода работу на таком сложном языке, с очень сложной системой времени выполнения, но система типов Haskell обеспечивает очень надежные гарантии, а семантика языка обеспечивает гораздо более строгие принципы рассуждения, чем большинство языков. Кроме того, вы склонны писать гораздо меньше кода для каждого приложения, поэтому его легко показать правильно.
Если вам нужны еще более строгие гарантии, SPARK Ada (или просто SPARK в наши дни) - это относительно простой традиционный императивный язык, который поставляется с полной формальной семантикой и инструментами для полной формальной проверки. Вы получаете более надежные гарантии, чем с Haskell, но по гораздо более высокой цене, как в капитале, так и в рабочей силе.
Вы можете думать в терминах Eiffel , где более строгое соблюдение предварительных и последующих условий делает системы с высокой степенью целостности Полегче.
Это противоречие в терминах. Сильно типизированные, блочно-структурированные языки почти всегда компилируются компилятором, создавая машинный код, за который программист не отвечает. Если вы хотите на 100% отвечать за код, вам нужно использовать язык ассемблера.
Вы можете искать то, что хотите, но вы выиграли не понимаю.
Ваши требования несовместимы друг с другом. Они в основном полностью исключают любую библиотеку. Вы можете сказать, что можете использовать C / C ++, но БЕЗ КАКИХ-ЛИБО ФАЙЛОВ И СТАНДАРТНЫХ БИБЛИОТЕК (за которые программист, очевидно, не несет ответственности).
Это оставляет вас в значительной степени на суше - требование нереалистично. Даже в большой команде никто не захочет перепрограммировать большинство библиотек.
Java на самом деле довольно хороша, если у вас есть подходящие методы программирования - и достаточно интересно, что ваше требование (система с высокой степенью целостности) в большей степени является проблемой методологии программирования (модульные тесты, тонны внутренних тестов, несколько экземпляров в параллельном сравнении результаты - например, управляющие компьютеры космического челнока - в случае отказа одного из них) чем то, что решает язык.