Communicating between in and out contracts

Denis Koroskin 2korden at gmail.com
Fri Oct 16 14:22:51 PDT 2009


On Sat, 17 Oct 2009 00:54:51 +0400, Denis Koroskin <2korden at gmail.com>  
wrote:

> On Sat, 17 Oct 2009 00:28:55 +0400, Denis Koroskin <2korden at gmail.com>  
> wrote:
>
>> On Sat, 17 Oct 2009 00:22:54 +0400, Andrei Alexandrescu  
>> <SeeWebsiteForEmail at erdani.org> wrote:
>>
>>> Jason House wrote:
>>>> if fun or gun is impure, then they should not be callable by the
>>>> contracts. Because of that, order is irrelevant.
>>>
>>> 1. Restricting calls to pure functions is sensible, but was deemed too  
>>> restrictive.
>>>
>>> 2. Even so, there's difficulty on what to cache. The amount cached may  
>>> depend on both the old and new object (in my example it only depends  
>>> on the old object).
>>>
>>> 3. There's too much hidden work and too much smarts involved. I just  
>>> don't think that's a feasible solution with what we know and have  
>>> right now.
>>>
>>>
>>> Andrei
>>
>> When not just let users one variable of type Variant per contract to  
>> store whatever they want?
>
> I mean, not a Variant, but a Dynamic* object so that the following would  
> be possible:
>
> void push(T)(T val)
> in(storage)
> {
>      storage.oldSize = this.size; // store
>      //storage.anyDynamicProperty = anyDynamicValue; in general case
> }
> out(storage)
> {
>      assert(storage.oldSize + 1 == this.size); // access
> }
> body
> {
>      // impl
> }
>
> *do you recall the Dynamic class discussion (a class that allows any  
> arbitrary methods and properties access, similar to JavaScript objects  
> or dynamic objects in C#)

On second thought Dynamic objects need run-time reflection that D  
currently lacks.

Alternatively users may be given a Variant[string] assoc.array as a  
poor-man's replacement for a full-fledged Dynamic object:

void push(T)(T val)
in(storage)
{
     storage["oldSize"] = this.size();
}
out(storage)
{
     assert(*storage["oldSize"].peek!(int) == this.size - 1);
}
body
{
     // impl
}

The contracts userdata would be stored in a stack alongside with monitor,  
classinfo etc for classes, and past the data fields for structs.



More information about the Digitalmars-d mailing list