Re: My bug or else regarding Visibility Rules

[Anh Vo <anhvofrcaus@gmail.com>]

On Tuesday, April 2, 2013 1:16:34 PM UTC-7, Simon Wright wrote:
> Anh Vo <anhvofrcaus@gmail.com> writes: > On Tuesday, April 2, 2013 1:26:12 AM UTC-7, Simon Wright wrote: > Other recipients: > Anh Vo <anhvo...@gmail.com> writes: 

>> It is dangerous make internal data visible in this case. after careful 
>> consideration, I decided to take away part of the post-conditions 
>> rather than exposing them. Following the philosophy of Ada, I would 
>> not leave any possibilities for the clients to accidently mess it up 
>> (not allowing clients to shoot themselve in the foot) 

> I think that part of your difficulty is that your Queue is implemented 
> using(effectively) global objects (Buffer, In_Index etc). 

Actually, it is my intention to design this way. I believe it is called singleton form. I could have designed Queue type as well, as you suggested. 

> then you could say something like 
>
>   procedure Put (Q : in out Queue; Item : Element) 
>     with Pre => not Queue_Full (Q'Old), 
>          Post => Item_Added (Q'Old, Q, Item); 

I believe that attribute 'Old is allowed in post-conditions only. 

> with public 
>
>   function Item_Added (Old, Current : Queue; Item : Element) return Boolean; 
>
>and private 
>
>   function Item_Added 
>     (Old, Current : Queue; Item : Element) return Boolean is 
>      ((Current.In_Index = (Old.In_Index + 1) mod Length) and 
>         (Current.Buffer (Old.In_Index) = Item) and 
> --         (for all I in 1 .. Queue_Length'Old => 
> --            Buffer(I) = Buffer'Old (I)) and 
>         (not Queue_Empty (Current))); 

This way does not look simpler. I rather go with simple way even I decide to use Queue type instead of Singleton Queue.

> I commented out the comparison, because this is a *circular* buffer, so 
> the first valid element isn't at Buffer(1).

I do not understand this. Why isn't Buffer(1) valid if my index starts at 1? 

> I think it will all work better if you say 
>   subtype Index is Natural range 0 .. Length - 1; 
> so that mod works as you require. 
>
> You need to add 1 to the current index and then do mod length! 

This is another array index option.

A. Vo