ADA - условия до и после не работают? - PullRequest
Новая
       20

ADA - условия до и после не работают?

2 голосов
/ 24 марта 2020

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

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

-- Compilation with "gnat make  -gnata  prepost.adb"
-- If -gnata is ommitted, pre and post conditions will not
-- be checked

with Ada.Text_IO; use Ada.Text_IO;
with Ada.Integer_Text_IO; use Ada.Integer_Text_IO;

procedure Tp2q4 is

   -- FIXME-begin
   function changeValues(A, B: in out INTEGER) return Boolean is
   begin
        A := 2;
        B := 3;
        return true;
   end changeValues;
   -- FIXME-end


   function Sum_Of_Numbers(A, B : in out INTEGER) return INTEGER
     with
     -- Precondition must ensure that A should be negative, B positive
     -- Postcondition must ensure that the expected result is A+B

     -- *Warning*
     -- You must play with pre/post conditions so that:
     --     (1) the return value will be correctly checked
     --     (2) BUT the values of A and B are modifified by the pre/post-condition

     -- FIXME-begin
     Pre=>A < 0 and then B >= 0,
     Post=>Sum_Of_Numbers'Result = A + B and then changeValues(A, B)
     -- FIXME-end
   is
   begin
      -- Changing A+B to A*B must trigger an error
      return A + B;
   end Sum_Of_Numbers;

   A, B : INTEGER;
begin
   A := -1;
   B := 2;
   Put(Sum_Of_Numbers(A,B));
   Put(A);
   Put(B);
end Tp2q4;

Текущий выход: 

  1         -1          2

Ожидаемый результат: 

1
2
3

1 Ответ

4 голосов
/ 24 марта 2020

Если вы используете GNAT (который выглядит как jdoodle по умолчанию), вам нужно включить утверждения. Добавьте -gnata в качестве параметра командной строки.

РЕДАКТИРОВАТЬ: я не знаю много о jdoodle, но кажется, что он не может принимать аргументы компилятору, только при запуске вашей программы ...

Вместо этого вы можете добавить pragma Assertion_Policy в вашу программу, например: 

procedure Tp2q4 is
   pragma Assertion_Policy(Check);

   --...
...