Почему Ада является «критически важным для безопасности» языком?
Я пробовал поискать в Google и прочитал несколько фрагментов в Интернете. Почему язык Ada является «критически важным для безопасности»? Я заметил некоторые вещи:
- Нет указателей
- Укажите диапазон (этот тип является целым числом, но может быть только 1-12)
- Явно укажите, если параметр функции отсутствует или вводится / выводится
- Диапазон- на основе циклов (чтобы избежать связанных ошибок или проверки привязки)
Остальной синтаксис я либо не понимал, либо не видел, как он помогает быть «критичным для безопасности». Это некоторые моменты, но я не вижу общей картины. Есть ли у него контракт на проектирование, которого я не вижу? Есть ли в нем правила, которые затрудняют компиляцию кода (и если да, то какие?) Почему это «критически важный для безопасности» язык?
1 ответ
Все это хорошо для критически важного применения; но учтите также возможность назначать макет (вплоть до битов) и возможность [опционально] указывать, что такая запись может быть ТОЛЬКО в определенном месте (полезно для таких вещей, как отображения видеопамяти).
Учтите, что многие критически важные для безопасности приложения также не имеют стандартных (в смысле как «широко распространенного», так и прямого сопоставления) интерфейсов; Например: ядерные реакторы, ракетные двигатели (сама техника отличается от поколения к поколению *), модели самолетов.
Будущий стандарт Ada 2012 ДОЛЖЕН иметь действующие контракты в форме предварительных и последующих условий; пример (взят из http://www2.adacore.com/wp-content/uploads/2006/03/Ada2012_Rational_Introducion.pdf ):
generic
type Item is private;
package Stacks is
type Stack is private;
function Is_Empty(S: Stack) return Boolean;
function Is_Full(S: Stack) return Boolean;
procedure Push(S: in out Stack; X: in Item)
with
Pre => not Is_Full(S),
Post => not Is_Empty(S);
procedure Pop(S: in out Stack; X: out Item)
with
Pre => not Is_Empty(S),
Post => not Is_Full(S);
Stack_Error: exception;
private
-- Private portion.
end Stacks;
Кроме того, еще одна вещь, которая получает замаскировано, это возможность исключить Null из ваших Access / типов указателей; это полезно тем, что вы можете а) указать это исключение в параметрах вашей подпрограммы и б) упростить свой алгоритм [так как вам не нужно проверять нулевое значение в каждом случае использования], и в) разрешить ваше исключение Обработчик обрабатывает (я предполагаю) исключительное обстоятельство из Null.
* The Arianne 5 disaster occurred precisely because the management disregarded this fact and had the programmers use the incorrect specifications: that of the Arianne 4.