Question on type invariants

Question on type invariants

[reinkor]

This question may be a bit imprecise:

Assume a complex object A (for example a set of records stored in a Container or file). Let S (for example an array of records) represent a summary of A (derived 
from A).

I want to update S (call "Update_S") in an economical way. S may not be updated immediately each time A changes. And I would prefer not to update too much when S is up-to-date anyway (i.e. avoid redundant updating). I also want to keep things simple and avoid to combine updating S in any smart way when I change A (I may not have full control over the modifications of A anyway). The main thing is that S in "fresh"/updated when I use it (not necessary when A changes).

In principle I could mark A and S with a "last-modified-time-flag" so I can update S when I find it necessary. This has similarities to unix "make". Bad idea?

I can program the whole thing and keep the concepts in my head, but is it a natural "Ada way" to secure that S is up-to-date when used? Is "type invariants" of any help?

reinert

Re: Question on type invariants

[Randy Brukardt]

"reinkor" <reinkor@gmail.com> wrote in message 
news:65f79e53-a468-4b77-8ee1-440c26a09371@googlegroups.com...
...
> I can program the whole thing and keep the concepts in my head, but is it 
> a natural
>"Ada way" to secure that S is up-to-date when used? Is "type invariants" of 
>any help?

Perhaps, if you can only export up-to-date versions of S. Type invariants 
are (mostly) enforced at the package boundary, that is when objects are 
passed in and out of the package that implements S.

I generally find that type invariants are too limiting. It's usually easier 
to have a dynamic predicate on a subtype; you can then apply that subtype to 
each place where the property is required. Something like:

    type S is ...
    subtype Up_to_Date_S is S
       with Dynamic_Predicate => Is_Up_to_Date (Up_to_Date_S);

Then all of the operations that require up-to-date S values can have 
parameters of Up_to_Date_S; the compiler will insert a check that it is in 
fact up-to-date. (But be careful: if you use such subtypes in places where 
the object can become stale behind the scenes, Ada will not recheck the 
predicate - dynamic predicates are primarily checked when a subtype 
conversion occurs, and usually only when a subtype *change* happens.)

In either case, you have to be able to write a function which returns True 
or False as to whether an object of type S is up-to-date. (If you can't do 
that, you can't use any sort of contract for the obvious reason that a 
contract has to be able to tell if it is satisfied.)

                                   Randy.

Re: Question on type invariants

[reinkor]

Thanks. I try it it.

reinert

Re: Question on type invariants

[reinkor]

Thanks, I try it out.

Re: Question on type invariants

[Dmitry A. Kazakov]

On 25/01/2017 09:38, reinkor wrote:

> In principle I could mark A and S with a "last-modified-time-flag"
> so  I can update S when I find it necessary. This has similarities to unix
> "make". Bad idea?

It depends. There are many scenarios, e.g. transactions is to name one.

What you have described looks like a lazy evaluation scheme. You keep 
track of applied changes ("expressions") and apply these changes on 
demand ("evaluate"). So long keeping commands is cheaper than applying 
them, it works fine. This schema is widely used for graphic contexts. 
Graphic operations do not have immediate effect, but cached until final 
rendering occurs, then the cache of commands is flushed. A continuation 
of the schema is having the object completely stateless. No value is 
kept only the commands to produce it.

> I can program the whole thing and keep the concepts in my head, but
> is  t a natural "Ada way" to secure that S is up-to-date when used?

There is no specific Ada's way. These are common considerations.

> Is "type invariants" of any help?

No. Invariant is a different thing. The idea is that the invariant is 
always true outside public calls, as Randy said, at the type's interface 
border. Since both updating and getting value are *public* operations 
they both must maintain the invariant.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Question on type invariants

[Robert Eachus]

On Wednesday, January 25, 2017 at 3:38:53 AM UTC-5, reinkor wrote:
 
> In principle I could mark A and S with a "last-modified-time-flag" so I can update S when I find it necessary. This has similarities to unix "make". Bad idea?

Responding to this point only, there are two decent ways to maintain last modified values for A and S.  One way is to store timestamps. Update_S then compares the values of last_modified for A and S for equality.  If not equal, copy the timestamp from A to S, and do the update work, otherwise exit immediately.  The potential problem here is that the timestamps may not be of sufficient granularity.  The other approach is to use a counter, updated every time A is.  Again comparing for equality can be used to avoid the excess work.  In this case you need to worry about whether your counter is large enough.  My tendency would be just to use a 64-bit integer.  But you may not have atomic updates for 64-bit values, and S and A may be maintained by different tasks.

For this case, there is a neat trick.  Use a smaller integer type for the counter.  When the S counter value is smaller than the A counter value, set both counters to zero, and do the S update.  This can all be done with a protected object, but with careful coding, it can be done with the counters being marked atomic.  Notice that it is possible that an update to A can occur while processing S.  You may need to use protected objects to insure that S_Update sees a consistent view of A.  However, it doesn't really matter whether the update to A is reflected in the new S, you may just have an additional, unneeded update of S now or later.

Re: Question on type invariants

[reinkor]

>  The potential problem here is that the timestamps may not be of sufficient granularity.  

What about to use "wait" statements to ensure S is up-to-date?  I.e. make a request to wait for update of A. Then wait for confirmation that waiting time has started and then go ahead to update?  A (kind of) "collaborative approach" ? :-)

Re: Question on type invariants

[reinkor]

torsdag 26. januar 2017 17.18.43 UTC+1 skrev Robert Eachus følgende:

>   Notice that it is possible that an update to A can occur while processing S.  

Maybe a hack: what about using "wait" statements. Sending a request to pause updating A -> wait for confirmation -> then update S ?

Re: Question on type invariants

[reinkor]

On Thursday, January 26, 2017 at 9:38:21 AM UTC+1, Dmitry A. Kazakov wrote:

> What you have described looks like a lazy evaluation scheme. 

Exactly.

But no way to express this intention in a somehow explicite way in Ada?
The point is to produce updates only when you need it (i.e. when you read
from (use) S and A has changed since last update (of S).

Re: Question on type invariants

[Dmitry A. Kazakov]

On 27/01/2017 10:20, reinkor wrote:
> On Thursday, January 26, 2017 at 9:38:21 AM UTC+1, Dmitry A. Kazakov wrote:
>
>> What you have described looks like a lazy evaluation scheme.
>
> Exactly.
>
> But no way to express this intention in a somehow explicite way in Ada?
> The point is to produce updates only when you need it (i.e. when you read
> from (use) S and A has changed since last update (of S).

private
    type Lazy_Object is ... record
       Self : not null access Lazy_Object :=
              Lazy_Object'Unchecked_Access; -- Rosen's trick
       Cached : Value_Type; -- Last evaluated value
       Queue  : FIFO_Type;  -- Queue of update requests
    end record;

procedure Update (Value : in out Lazy_Object; Change : Request_Type) is
begin
    if Value.Queue.Is_Full then
       Value.Flush; -- Make space
    end if;
    Value.Queue.Put (Change);
end Update;

function Get (Value : Lazy_Object) return Value is
begin
    if not Value.Queue.Is_Empty then
       Value.Self.Flush; -- Collapse the queue
    end if;
    return Value.Cached;
end Get;

procedure Flush (Value : in out Lazy_Object) is
begin
    while not Value.Queue.Is_Empty loop
       Value.Cached := Execute (Value.Queue.Top, Value.Cached);
       Value.Queue.Delete;
    end loop;
end Flush;

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Question on type invariants

[reinkor]

Thanks a lot. Try it. Got a bit scared by Unchecked_Access :-)