'Old for limited types that are not limited in private view

Hi,
I made element limited private in the public view, but not in the private view. But then I understand now that contracts in the public view have to follow the public limitedness ?
This is annoying, how to prove different properties if I can’t use 'Old ?
The problem is that it makes a copy of the parameter, even though I only need one component… But of course I can’t mention a component of a private type there.
So how would you write

with  Post => Size(Q) = Size(Q'Old) + 1;

for instance, to express that the quantity increases after a subprogram call ?

pragma Ada_2022;
pragma Assertion_Policy (Check);
GENERIC

  TYPE Element IS PRIVATE;
  PriorityNumber: Positive := 3;
PACKAGE Queues_Generic with Spark_Mode is

  TYPE Queue (Capacity: Positive) is limited private;
  FUNCTION IsEmpty (Q : IN Queue) RETURN Boolean;
  FUNCTION IsFull  (Q : IN Queue) RETURN Boolean;
  subtype PriorityRange is Natural range 1..PriorityNumber;
  QueueFull  : EXCEPTION;
  QueueEmpty : EXCEPTION;

  FUNCTION Size (Q : IN Queue) RETURN Natural with Ghost;
  FUNCTION First (Q : IN Queue) RETURN Element
    with  Pre => (if IsEmpty (Q) then raise QueueEmpty);
  PROCEDURE MakeEmpty (Q : IN OUT Queue);
  PROCEDURE Enqueue (Q : IN OUT Queue;
		     E : IN Element; P: PriorityRange)  
    with  Pre => (if IsFull(Q) then raise QueueFull),
          Post => Size(Q) = Size(Q'Old) + 1;

  PROCEDURE Dequeue (Q : IN OUT Queue)
    with  Pre => (if IsEmpty(Q) then raise QueueEmpty),
          Post =>  Size(Q) = Size(Q'Old) - 1 and First (Q'Old) /= First (Q);


PRIVATE
  type TailList is array (PriorityRange) of Natural;
  TYPE List IS ARRAY (Positive RANGE <>) OF Element;
  TYPE Queue (Capacity: Positive) IS RECORD
    CurrentSize : Natural := 0;
    Tails: TailList := [others => 0]; 
    Head: Natural := 1;
    Store: List(1..Capacity);
  END RECORD with Type_Invariant => Queue.Head not in Tails(1).. Tails(PriorityRange'Last);
  
END Queues_Generic;

In this case you can just write Size(Q)'Old. When you use 'Old, the entire expression to the left of 'Old is captured at the start of your subprogram, so you can be specific about what state you want to copy. You can think of the compiler as generating code like:

procedure Enqueue(Q : ...) is
   Size_Q_Old : constant <> := Size(Q);
begin
   --  your code here

   --  compiler generated postcondition checks
   if not (Size(Q) = Size_Q_Old + 1) then
      --  raise contract failure
   end if;
end Enqueue;

You can read about the specifics in the RM: Preconditions and Postconditions

2 Likes