# 'Old for limited types that are not limited in private view
**URL:** https://forum.ada-lang.io/t/old-for-limited-types-that-are-not-limited-in-private-view/1325
**Category:** General
**Created:** [October 13, 2024, 8:32pm UTC](https://forum.ada-lang.io/t/old-for-limited-types-that-are-not-limited-in-private-view/1325 "2024-10-13T20:32:01Z")
**Posts on this page:** 2
**Page:** 1
### Author:  [@evanescente-ondine](https://forum.ada-lang.io/u/evanescente-ondine)
#### Post date: [October 13, 2024, 8:32pm UTC](https://forum.ada-lang.io/t/old-for-limited-types-that-are-not-limited-in-private-view/1325/1 "2024-10-13T20:32:01Z")
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 ?
```ada
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;
```
---
### Author:  [@jcmoyer](https://forum.ada-lang.io/u/jcmoyer)
#### Post date: [October 14, 2024, 4:01pm UTC](https://forum.ada-lang.io/t/old-for-limited-types-that-are-not-limited-in-private-view/1325/2 "2024-10-14T16:01:15Z")
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:
```ada
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](https://www.adaic.org/resources/add_content/standards/22rm/html/RM-6-1-1.html#I3781)