From: Simon Wright <simon@pushface.org>
Subject: Re: My bug or else regarding Visibility Rules
Date: Tue, 02 Apr 2013 21:16:34 +0100
Date: 2013-04-02T21:16:34+01:00 [thread overview]
Message-ID: <lysj38hen1.fsf@pushface.org> (raw)
In-Reply-To: e703d782-2e4c-4fe9-bcae-218abcc170f1@googlegroups.com
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:
>> This is (partly) why we now have expression functions; specify the
>> function in the public part, use it in a pre/postcondition, complete it
>> with an expression function in the private part when Buffer etc. are
>> visible.
>
> 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). If you made
Queue a data type
type Queue is private;
...
private
...
type Queue is record
Buffer : Element_Array;
In_Index : Index := 1;
Out_Index : Index := 1;
Count: Natural range 0 .. Length := 0;
end record;
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);
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)));
Notes:
I commented out the comparison, because this is a *circular* buffer, so
the first valid element isn't at Buffer(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!
next prev parent reply other threads:[~2013-04-02 20:16 UTC|newest]
Thread overview: 15+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-03-28 19:54 My bug or else regarding Visibility Rules Anh Vo
2013-03-28 20:58 ` Adam Beneschan
2013-03-28 22:03 ` Randy Brukardt
2013-03-30 6:05 ` Anh Vo
2013-04-02 0:56 ` Randy Brukardt
2013-04-02 1:52 ` Anh Vo
2013-04-02 8:26 ` Simon Wright
2013-04-02 18:17 ` Anh Vo
2013-04-02 20:16 ` Simon Wright [this message]
2013-04-03 23:21 ` Anh Vo
2013-04-04 8:19 ` Simon Wright
2013-04-04 19:21 ` Anh Vo
2013-04-04 19:47 ` Simon Wright
2013-04-02 22:04 ` Randy Brukardt
2013-03-28 22:06 ` Anh Vo
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox