immutability, static verification of assertions

[helmut.brandl]

In february we had a discussion on immutable strings on this mailing list.

I have reviewed the current status of the library and came to the
conclusion that the design with STRING, READABLE_STRING and
IMMUTABLE_STRING perfectly reflects the need for STRINGs which we
discussed in february.

The design for STRING can be used for any other type which needs
immutability. However if you use the pattern with more classes you end
up with 3 versions of each class (at least for the classes which needs
immutability).

Therefore I think that the problem needs a more general solution. I have
encountered a possible solution to express immutability without the
overhead of having 3 classes and wrote it down in a small white paper.

For those interested they can find it at
http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt
and discuss it in the forums at the origo site
http://ecma-eiffel.origo.ethz.ch/forum.

Immutability will be an important aspect to statically verify assertions
(i.e. proof them).

Regards

[dlebansais]

--- In [hidden email], Helmut Brandl <helmut.brandl@...> wrote:

>
> In february we had a discussion on immutable strings on this mailing list.
>
> I have reviewed the current status of the library and came to the
> conclusion that the design with STRING, READABLE_STRING and
> IMMUTABLE_STRING perfectly reflects the need for STRINGs which we
> discussed in february.
>
> The design for STRING can be used for any other type which needs
> immutability. However if you use the pattern with more classes you end
> up with 3 versions of each class (at least for the classes which needs
> immutability).
>
> Therefore I think that the problem needs a more general solution. I have
> encountered a possible solution to express immutability without the
> overhead of having 3 classes and wrote it down in a small white paper.
>
> For those interested they can find it at
> http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt
> and discuss it in the forums at the origo site
> http://ecma-eiffel.origo.ethz.ch/forum.
>
> Immutability will be an important aspect to statically verify assertions
> (i.e. proof them).
>
> Regards
>

Your link to the forums gives me error 404. And if I navigate to the forum manually, the most recent topic is 30 weeks ago.

Regards,
David Le Bansais

[helmut.brandl]

David wrote:
>
> Your link to the forums gives me error 404. And if I navigate to the forum manually, the most recent topic is 30 weeks ago.
>

I don't know what is wrong with the link. In my browser
http://ecma-eiffel.origo.ethz.ch/forum works fine.

There is not much discussion on the origo site. Unfortunately I don't
know of any other site to discuss the Eiffel language.

Helmut

[dlebansais]

I tried to create an account but failed the CAPTCHA test 3 times, so I'm giving up. (Good luck, Chinese users).

This forum sees more activity, anyway. I'll come back to the real discussion after I have compared your paper with my own work.

Regards,
David Le Bansais.

--- In [hidden email], Helmut Brandl <helmut.brandl@...> wrote:

>
> David wrote:
> >
> > Your link to the forums gives me error 404. And if I navigate to the forum manually, the most recent topic is 30 weeks ago.
> >
>
> I don't know what is wrong with the link. In my browser
> http://ecma-eiffel.origo.ethz.ch/forum works fine.
>
> There is not much discussion on the origo site. Unfortunately I don't
> know of any other site to discuss the Eiffel language.
>
> Helmut
>

[Bernd Schoeller-3]

Hi Helmut,

interesting thoughts. Just some small question: what do you do about the
fact that queries are allowed to have side-effects? How do you
unterstand the semantics of deep_twin?

Also, it needs to be discussed if the introduction of two new keywords
is necessary for something that can be nicely modeled using classes.

Bernd

--
Bernd Schoeller, PhD, CTO, Partner
Comerge AG, Bubenbergstrasse 11, CH-8045 Zurich, www.comerge.net

On 11/9/09 4:30 AM, Helmut Brandl wrote:

>  
>
> In february we had a discussion on immutable strings on this mailing list.
>
> I have reviewed the current status of the library and came to the
> conclusion that the design with STRING, READABLE_STRING and
> IMMUTABLE_STRING perfectly reflects the need for STRINGs which we
> discussed in february.
>
> The design for STRING can be used for any other type which needs
> immutability. However if you use the pattern with more classes you end
> up with 3 versions of each class (at least for the classes which needs
> immutability).
>
> Therefore I think that the problem needs a more general solution. I have
> encountered a possible solution to express immutability without the
> overhead of having 3 classes and wrote it down in a small white paper.
>
> For those interested they can find it at
> http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt
> <http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt>
> and discuss it in the forums at the origo site
> http://ecma-eiffel.origo.ethz.ch/forum.
> <http://ecma-eiffel.origo.ethz.ch/forum.>
>
> Immutability will be an important aspect to statically verify assertions
> (i.e. proof them).
>
> Regards
>
>

[Colin LeMahieu]

It would be interesting to see what could be done if CQS was compiler
enforced and queries were required to be referentially transparent; this
would be no where near backwards compatible, however, because you couldn't
do things like create a reference type and assign it to Result in the same
feature.

On Tue, Nov 10, 2009 at 2:35 AM, Bernd Schoeller <
[hidden email]> wrote:

>
>
> Hi Helmut,
>
> interesting thoughts. Just some small question: what do you do about the
> fact that queries are allowed to have side-effects? How do you
> unterstand the semantics of deep_twin?
>
> Also, it needs to be discussed if the introduction of two new keywords
> is necessary for something that can be nicely modeled using classes.
>
> Bernd
>
> --
> Bernd Schoeller, PhD, CTO, Partner
> Comerge AG, Bubenbergstrasse 11, CH-8045 Zurich, www.comerge.net
>
>
> On 11/9/09 4:30 AM, Helmut Brandl wrote:
> >
> >
> > In february we had a discussion on immutable strings on this mailing
> list.
> >
> > I have reviewed the current status of the library and came to the
> > conclusion that the design with STRING, READABLE_STRING and
> > IMMUTABLE_STRING perfectly reflects the need for STRINGs which we
> > discussed in february.
> >
> > The design for STRING can be used for any other type which needs
> > immutability. However if you use the pattern with more classes you end
> > up with 3 versions of each class (at least for the classes which needs
> > immutability).
> >
> > Therefore I think that the problem needs a more general solution. I have
> > encountered a possible solution to express immutability without the
> > overhead of having 3 classes and wrote it down in a small white paper.
> >
> > For those interested they can find it at
> >
> http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt
> > <
> http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt
> >
> > and discuss it in the forums at the origo site
> > http://ecma-eiffel.origo.ethz.ch/forum.
> > <http://ecma-eiffel.origo.ethz.ch/forum.>
> >
> > Immutability will be an important aspect to statically verify assertions
> > (i.e. proof them).
> >
> > Regards
> >
> >
>  
>

[Non-text portions of this message have been removed]



------------------------------------

Yahoo! Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/eiffel_software/

<*> Your email settings:
    Individual Email | Traditional

<*> To change settings online go to:
    http://groups.yahoo.com/group/eiffel_software/join
    (Yahoo! ID required)

<*> To change settings via email:
    [hidden email]
    [hidden email]

<*> To unsubscribe from this group, send an email to:
    [hidden email]

<*> Your use of Yahoo! Groups is subject to:
    http://docs.yahoo.com/info/terms/

[Bernd Schoeller-3]

On 11/10/09 10:36 AM, Colin LeMahieu wrote:
> It would be interesting to see what could be done if CQS was compiler
> enforced and queries were required to be referentially transparent; this
> would be no where near backwards compatible, however, because you couldn't
> do things like create a reference type and assign it to Result in the same
> feature.

(little advertisement for my thesis)

Dynamic Frame Contracts solve this problem in a nice and elegant way,
allowing queries to have modify and use specifications.

Bernd

>
> On Tue, Nov 10, 2009 at 2:35 AM, Bernd Schoeller <
> [hidden email]> wrote:
>
>>
>>
>> Hi Helmut,
>>
>> interesting thoughts. Just some small question: what do you do about the
>> fact that queries are allowed to have side-effects? How do you
>> unterstand the semantics of deep_twin?
>>
>> Also, it needs to be discussed if the introduction of two new keywords
>> is necessary for something that can be nicely modeled using classes.
>>
>> Bernd
>>
>> --
>> Bernd Schoeller, PhD, CTO, Partner
>> Comerge AG, Bubenbergstrasse 11, CH-8045 Zurich, www.comerge.net
>>
>>
>> On 11/9/09 4:30 AM, Helmut Brandl wrote:
>>>
>>>
>>> In february we had a discussion on immutable strings on this mailing
>> list.
>>>
>>> I have reviewed the current status of the library and came to the
>>> conclusion that the design with STRING, READABLE_STRING and
>>> IMMUTABLE_STRING perfectly reflects the need for STRINGs which we
>>> discussed in february.
>>>
>>> The design for STRING can be used for any other type which needs
>>> immutability. However if you use the pattern with more classes you end
>>> up with 3 versions of each class (at least for the classes which needs
>>> immutability).
>>>
>>> Therefore I think that the problem needs a more general solution. I have
>>> encountered a possible solution to express immutability without the
>>> overhead of having 3 classes and wrote it down in a small white paper.
>>>
>>> For those interested they can find it at
>>>
>> http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt
>>> <
>> http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt
>>>
>>> and discuss it in the forums at the origo site
>>> http://ecma-eiffel.origo.ethz.ch/forum.
>>> <http://ecma-eiffel.origo.ethz.ch/forum.>
>>>
>>> Immutability will be an important aspect to statically verify assertions
>>> (i.e. proof them).
>>>
>>> Regards
>>>
>>>
>>  
>>
>
>
> [Non-text portions of this message have been removed]
>
>
>
> ------------------------------------
>
> Yahoo! Groups Links
>
>
>

--
--
Bernd Schoeller, PhD, CTO, Partner
Comerge AG, Bubenbergstrasse 11, CH-8045 Zurich, www.comerge.net

[helmut.brandl]

Bernd Schoeller wrote:
> Hi Helmut,
>
> interesting thoughts. Just some small question: what do you do about the
> fact that queries are allowed to have side-effects?

Queries can have side effects. But the guideline is that they don't have
 visible side effects. The compiler is not yet able to enforce that. But
a verifying compiler shall be able to do that.

> How do you
> unterstand the semantics of deep_twin?

I don't understand the question. deep_twin is deep_twin. A complete
clone of the object and all reachable objects recursively. The frames of
an object and its deep_twin don't overlap.

>
> Also, it needs to be discussed if the introduction of two new keywords
> is necessary for something that can be nicely modeled using classes.

This is a side issue. But you are right. The introduction of new
keywords shall be made very carefully. Maybe there are more elegant ways
to express this syntactically. But let us concentrate on the concept.

I have tried to model immutability via classes. As the example in
EiffelStudio's base lib with STRING has proved, it is possible. But if
you want to rely on immutability a lot, you end up with a bunch of
classes which are necessary just to express that property. And if the
designer of a certain class has not implemented all 3 variants, objects
of that class cannot be used in a HASH_MAP as keys without the danger to
screw up the hash table i.e. violate the invariant of HASH_MAP.

Helmut

>
> Bernd
>
> --
> Bernd Schoeller, PhD, CTO, Partner
> Comerge AG, Bubenbergstrasse 11, CH-8045 Zurich, www.comerge.net
>
> On 11/9/09 4:30 AM, Helmut Brandl wrote:
>>  
>>
>> In february we had a discussion on immutable strings on this mailing list.
>>
>> I have reviewed the current status of the library and came to the
>> conclusion that the design with STRING, READABLE_STRING and
>> IMMUTABLE_STRING perfectly reflects the need for STRINGs which we
>> discussed in february.
>>
>> The design for STRING can be used for any other type which needs
>> immutability. However if you use the pattern with more classes you end
>> up with 3 versions of each class (at least for the classes which needs
>> immutability).
>>
>> Therefore I think that the problem needs a more general solution. I have
>> encountered a possible solution to express immutability without the
>> overhead of having 3 classes and wrote it down in a small white paper.
>>
>> For those interested they can find it at
>> http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt
>> <http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt>
>> and discuss it in the forums at the origo site
>> http://ecma-eiffel.origo.ethz.ch/forum.
>> <http://ecma-eiffel.origo.ethz.ch/forum.>
>>
>> Immutability will be an important aspect to statically verify assertions
>> (i.e. proof them).
>>
>> Regards
>>
>>
>
>
> ------------------------------------
>
> Yahoo! Groups Links
>
>
>

[Jonathan S. Ostroff]

Are there any working Eiffel packages for numerical calculations especially
roots of real-valued functions such as the IRR, e.g.


========================================================================
The IRR can be calculated by solving the expression below for r(T)...

MV(T) = MV(0)*{1+r(T)}^T + sum[C(t)*{1+r(T)}^{T-t}]

MV(T)... Ending market value portfolio
MV(0)... Beginning market value portfolio
T... Ending time T
r(T).... IRR at time T over time period {0,T}
C(t)...  Net contribution at time t

Note that the time period (0,T) is assumed to be divided in n equally spaced
time periods. Other formulas with different time conventions exist.
Unfortunately, there exists no "formula" for IRR. The above expression has
to be solved numerically (typically with the Newton-Raphson method).
======================================================================


Thanks

Jonathan

[Colin LeMahieu]

This paper is very interesting and could result in many compiler
optimizations, in addition to correctness around aliasing.  I enjoy that it
uses DbC style.

On Tue, Nov 10, 2009 at 6:24 AM, Bernd Schoeller <
[hidden email]> wrote:

>
>
> On 11/10/09 10:36 AM, Colin LeMahieu wrote:
> > It would be interesting to see what could be done if CQS was compiler
> > enforced and queries were required to be referentially transparent; this
> > would be no where near backwards compatible, however, because you
> couldn't
> > do things like create a reference type and assign it to Result in the
> same
> > feature.
>
> (little advertisement for my thesis)
>
> Dynamic Frame Contracts solve this problem in a nice and elegant way,
> allowing queries to have modify and use specifications.
>
> Bernd
>
>
> >
> > On Tue, Nov 10, 2009 at 2:35 AM, Bernd Schoeller <
> > [hidden email] <bernd.schoeller%40comerge.net>> wrote:
> >
> >>
> >>
> >> Hi Helmut,
> >>
> >> interesting thoughts. Just some small question: what do you do about the
> >> fact that queries are allowed to have side-effects? How do you
> >> unterstand the semantics of deep_twin?
> >>
> >> Also, it needs to be discussed if the introduction of two new keywords
> >> is necessary for something that can be nicely modeled using classes.
> >>
> >> Bernd
> >>
> >> --
> >> Bernd Schoeller, PhD, CTO, Partner
> >> Comerge AG, Bubenbergstrasse 11, CH-8045 Zurich, www.comerge.net
> >>
> >>
> >> On 11/9/09 4:30 AM, Helmut Brandl wrote:
> >>>
> >>>
> >>> In february we had a discussion on immutable strings on this mailing
> >> list.
> >>>
> >>> I have reviewed the current status of the library and came to the
> >>> conclusion that the design with STRING, READABLE_STRING and
> >>> IMMUTABLE_STRING perfectly reflects the need for STRINGs which we
> >>> discussed in february.
> >>>
> >>> The design for STRING can be used for any other type which needs
> >>> immutability. However if you use the pattern with more classes you end
> >>> up with 3 versions of each class (at least for the classes which needs
> >>> immutability).
> >>>
> >>> Therefore I think that the problem needs a more general solution. I
> have
> >>> encountered a possible solution to express immutability without the
> >>> overhead of having 3 classes and wrote it down in a small white paper.
> >>>
> >>> For those interested they can find it at
> >>>
> >>
> http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt
> >>> <
> >>
> http://tecomp.sourceforge.net/index.php?file=doc/papers/lang/immutability.txt
> >>>
> >>> and discuss it in the forums at the origo site
> >>> http://ecma-eiffel.origo.ethz.ch/forum.
> >>> <http://ecma-eiffel.origo.ethz.ch/forum.>
> >>>
> >>> Immutability will be an important aspect to statically verify
> assertions
> >>> (i.e. proof them).
> >>>
> >>> Regards
> >>>
> >>>
> >>
> >>
> >
> >
> > [Non-text portions of this message have been removed]
> >
> >
> >
> > ------------------------------------
> >
> > Yahoo! Groups Links
> >
> >
> >
>
> --
> --
> Bernd Schoeller, PhD, CTO, Partner
> Comerge AG, Bubenbergstrasse 11, CH-8045 Zurich, www.comerge.net
>  
>

[Non-text portions of this message have been removed]



------------------------------------

Yahoo! Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/eiffel_software/

<*> Your email settings:
    Individual Email | Traditional

<*> To change settings online go to:
    http://groups.yahoo.com/group/eiffel_software/join
    (Yahoo! ID required)

<*> To change settings via email:
    [hidden email]
    [hidden email]

<*> To unsubscribe from this group, send an email to:
    [hidden email]

<*> Your use of Yahoo! Groups is subject to:
    http://docs.yahoo.com/info/terms/