Заменяют ли предварительные и последующие условия проверку в функции?

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


ada formal-verification formal-methods spark-ada
person Lee Robinson    schedule 24.04.2021    source источник
comment
С помощью SPARK вы можете доказать для всей программы, что никакая автоматическая проверка не может быть нарушена, и в этом случае проверки во время выполнения можно безопасно отключить. При отсутствии таких доказательств необходимы проверки правильности во время выполнения.   -  person Jeffrey R. Carter    schedule 25.04.2021

Ответы (3)


arrow_upward
4
arrow_downward

Первый: если вы используете компилятор GNAT, вы должны добавить флаг -gnata к флагам компилятора или использовать файл конфигурации для GNAT с pragma Assertion_Policy(Check);, чтобы включить проверку для Pre- и Post-условий. Без одной из этих опций все проверки игнорируются. Вот почему вам позволено нарушать их.

Предварительные условия имеют место непосредственно перед выполнением выбранной подпрограммы. Например, функция, объявленная как:

function Add(A, B: Positive) return Positive is (A + B) with
   Pre => A < 10;

Это предварительное условие будет проверено перед выполнением функции. Например:

I := Add(2, 2);
Put_Line(Positive'Image(I)); -- prints 4 as expected
begin
   I := Add(10, 2); -- Crash, exception on violation of precondition
exception
   when ASSERT_FAILURE =>
      Put_Line(Positive'Image(I)); -- prints 4
end;

Постусловия проверяются на подпрограммах после их выполнения. Другой пример:

procedure Increment(A: in out Positive) with
   Post => A < 20 is
begin
   A := A + 1;
end Increment;

И использование:

I := 2;
Increment(I);
Put_Line(Positive'Image(I)); -- prints 3
I := 19;
begin
   I := Increment(I); -- Crash, exception on violation of postcondition
exception
   when ASSERT_FAILURE =>
      Put_Line(Positive'Image(I)); -- prints 19
end;
person thindil    schedule 24.04.2021
comment
спасибо, кажется, мне нужно добавить флаг --gnata при компиляции. как бы я сделал это в студии gnat? - person Lee Robinson; 24.04.2021
comment
@ LeeRobinson Я вижу, ты сам ответил. :) Другой способ: если я правильно помню, в настройках проекта есть возможность установить флаги компиляции. - person thindil; 24.04.2021
comment
Я нашел его в документации после прочтения вашего ответа, а затем понял, что ответ был упомянут вами, но я искал файл конфигурации, а не вставлял его в спецификацию! - person Lee Robinson; 24.04.2021

arrow_upward
3
arrow_downward

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

person Jim Rogers    schedule 24.04.2021
comment
Спасибо за все ваши ответы! Как узнать, когда это необходимо? Кажется, что ни одно из правил не соблюдается, поэтому все условия кажутся совершенно излишними, но я знаю, что это не так. - person Lee Robinson; 24.04.2021

arrow_upward
2
arrow_downward

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

pragma Assertion_Policy (Check);

к моему файлу спецификации.

person Lee Robinson    schedule 24.04.2021