ADA problem with value by reference or post conditions

Question

I have a problem with a 'simple' ADA program. This exercise aim at learning value by reference and post condition in ADA.

Here I want to build a simple function that sum two Integers where the first one is negative and the second one positive. The returned value must be the sum, and the postcondition must check it. This situation is only possible when the language integrates orthogonal concepts such as passing-by-reference and contracts.

In this code:

procedure Tp2q4 is

   function Set_Values(A : in out INTEGER; B : in out INTEGER) return BOOLEAN is
   begin
      A := 2;
      B := 3;
      return TRUE;
   end Set_Values;

   function Sum_Of_Numbers(A, B : in out INTEGER) return INTEGER
     with
       Pre => A < 0 and B > 0,
       Post => (Sum_Of_Numbers'Result = A + B and then Set_Values(A'Access, B'Access))
   is
   begin
      return A + B;
   end Sum_Of_Numbers;

With this test:

   A := -1;
   B := 2;
   Put(Sum_Of_Numbers(A,B));
   Put(A);
   Put(B);

I am suppose to get the result of the addition, the modification of A and the modification of B, so: -1 2 3

But i get : -1 1 2

So obviously the problem is either the value by reference or the post condition ... Any ideas how I could fix this?

Answer 1

You didn't give an actual compiling example, so I checked, and best I can see is that you didn't turn on Assertions to enable the post condition to fire. Note that based on the code you posted, the result should be 1 2 3, not -1 2 3. I tried to interpret what your actual code is and the following example works (though I would not recommend using post conditions like this at all. It is a very bad idea...you need to rethink your design).

with Ada.Text_IO; use Ada.Text_IO;

procedure jdoodle is

    pragma Assertion_Policy(Check);

    function Set_Values(A : in out INTEGER; B : in out INTEGER) return BOOLEAN is
    begin
      A := 2;
      B := 3;
      return TRUE;
    end Set_Values;
    
    function Sum_Of_Numbers(A, B : in out INTEGER) return INTEGER
     with
       Pre => A < 0 and B > 0,
       Post => (Sum_Of_Numbers'Result = A + B and then Set_Values(A, B))
    is
    begin
      return A + B;
    end Sum_Of_Numbers;
    
    A, B : Integer;
begin
    A := -1;
    B := 2;
    Put_Line(Sum_Of_Numbers(A,B)'Image);
    Put_Line(A'Image);
    Put_Line(B'Image);
end jdoodle;

Result:

 1
 2
 3

gcc -c jdoodle.adb
gnatbind -x jdoodle.ali
gnatlink jdoodle.ali -o jdoodle