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;