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