[eiffel-users] change in void safety behaviour in 17.01 ?

classic Classic list List threaded Threaded
18 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

[eiffel-users] change in void safety behaviour in 17.01 ?

Enrico Nardelli
The following code when compiled with 15.12 gives two VJAR compilation errors (Type error: source of assignment is not compatible with target) for both the assignemnt instructions.

When compiled with 17.01 only the last assignment (attac := detac)is flagged as VJAR.

class
    APPLICATION
inherit
    ARGUMENTS
create
    make
feature {NONE} -- Initialization
    attac: attached LINKED_LIST [INTEGER]
    detac: detachable LINKED_LIST [INTEGER]

    make
        local
            loc_attac: attached LINKED_LIST [INTEGER]
            loc_detac: detachable LINKED_LIST [INTEGER]
        do
            create attac.make
            loc_attac := loc_detac
            attac := detac
        end

The project in both environments has the setting VoidSafety: Complete.

Why the different behaviour?

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [eiffel-users] change in void safety behaviour in 17.01 ?

'Alexander Kogtenkov' via Eiffel Users
Indeed, one of the changes in 16.05 were relaxed void safety rules for local variables and Result (some details can be found at https://www.eiffel.org/doc/eiffelstudio/Major%20changes%20between%20ISE%20Eiffel%2015.12%20and%20ISE%20Eiffel%2016.05). In short, the idea is that attachment status for a local variable is inferred from the code, not is taken from the type declaration. As a consequence, starting from 16.05 attachment marks are ignored for locals.

The change is supported by the observation that with the new rules non-void-safe code triggers 30% fewer compilation errors. This allows for easier migration of legacy code as well as requires less noisy new code.

Unfortunately, similar rules are not applicable to features, in particular, because of their polymorphic nature and inability to do void safety analysis modularly in this case.

Alexander Kogtenkov


Enrico Nardelli <[hidden email]>:

The following code when compiled with 15.12 gives two VJAR compilation errors (Type error: source of assignment is not compatible with target) for both the assignemnt instructions.

When compiled with 17.01 only the last assignment (attac := detac)is flagged as VJAR.

class
    APPLICATION
inherit
    ARGUMENTS
create
    make
feature {NONE} -- Initialization
    attac: attached LINKED_LIST [INTEGER]
    detac: detachable LINKED_LIST [INTEGER]

    make
        local
            loc_attac: attached LINKED_LIST [INTEGER]
            loc_detac: detachable LINKED_LIST [INTEGER]
        do
            create attac.make
            loc_attac := loc_detac
            attac := detac
        end

The project in both environments has the setting VoidSafety: Complete.

Why the different behavior?


--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [eiffel-users] change in void safety behaviour in 17.01 ?

Colin Adams-4
This makes life harder for people to reason about the code. In the example above, there should be an error raised, because if you change the last assignment to attac := loc_attac, the wrong error will be raised, I think.
That is, I am assuming it will report the same error, which will certainly puzzle the programmer, as it would be a lie. The correct error to report would be that loc_attac has not been initialized to an attached value (or some such message).

On Wed, 17 May 2017 at 11:19 'Alexander Kogtenkov' via Eiffel Users <[hidden email]> wrote:
Indeed, one of the changes in 16.05 were relaxed void safety rules for local variables and Result (some details can be found at https://www.eiffel.org/doc/eiffelstudio/Major%20changes%20between%20ISE%20Eiffel%2015.12%20and%20ISE%20Eiffel%2016.05). In short, the idea is that attachment status for a local variable is inferred from the code, not is taken from the type declaration. As a consequence, starting from 16.05 attachment marks are ignored for locals.

The change is supported by the observation that with the new rules non-void-safe code triggers 30% fewer compilation errors. This allows for easier migration of legacy code as well as requires less noisy new code.

Unfortunately, similar rules are not applicable to features, in particular, because of their polymorphic nature and inability to do void safety analysis modularly in this case.

Alexander Kogtenkov


Enrico Nardelli <[hidden email]>:

The following code when compiled with 15.12 gives two VJAR compilation errors (Type error: source of assignment is not compatible with target) for both the assignemnt instructions.

When compiled with 17.01 only the last assignment (attac := detac)is flagged as VJAR.

class
    APPLICATION
inherit
    ARGUMENTS
create
    make
feature {NONE} -- Initialization
    attac: attached LINKED_LIST [INTEGER]
    detac: detachable LINKED_LIST [INTEGER]

    make
        local
            loc_attac: attached LINKED_LIST [INTEGER]
            loc_detac: detachable LINKED_LIST [INTEGER]
        do
            create attac.make
            loc_attac := loc_detac
            attac := detac
        end

The project in both environments has the setting VoidSafety: Complete.

Why the different behavior?


--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re[2]: [eiffel-users] change in void safety behaviour in 17.01 ?

'Alexander Kogtenkov' via Eiffel Users
There is always a tradeoff between explicit and implicit information: additional annotations instead of more flexible code. Of course, there are also different programming styles, and some users prefer one over another. In any case, the new rules allow for less local variables. For example, the snippet

   foo: X
      do
         Result := bar -- `bar` is detachable
         if not attached Result then
            Result := qux -- `qux` is attached
         end
      end

would have to be written with the older rules as

   foo: X
      local
         x: detachable X
      do
         x := bar -- `bar` is detachable
         if attached x then
            Result := x
         else
            Result := qux -- `qux` is attached
         end
      end

that is more verbose and less readable. A variant with object tests is also possible, but still it introduces new locals that pollute name space.

Also, with explicit type annotations some object initialization patterns become impossible.

In the end, void safety serves as a tool to avoid access on void target, and the rules guarantee that in either case. And my current view is that Eiffel does it much better than most existing languages with potential null dereferencing issue.

Alexander Kogtenkov


Colin Adams <[hidden email]>:

This makes life harder for people to reason about the code. In the example above, there should be an error raised, because if you change the last assignment to attac := loc_attac, the wrong error will be raised, I think.
That is, I am assuming it will report the same error, which will certainly puzzle the programmer, as it would be a lie. The correct error to report would be that loc_attac has not been initialized to an attached value (or some such message).

On Wed, 17 May 2017 at 11:19 'Alexander Kogtenkov' via Eiffel Users <[hidden email]> wrote:
Indeed, one of the changes in 16.05 were relaxed void safety rules for local variables and Result (some details can be found at https://www.eiffel.org/doc/eiffelstudio/Major%20changes%20between%20ISE%20Eiffel%2015.12%20and%20ISE%20Eiffel%2016.05). In short, the idea is that attachment status for a local variable is inferred from the code, not is taken from the type declaration. As a consequence, starting from 16.05 attachment marks are ignored for locals.

The change is supported by the observation that with the new rules non-void-safe code triggers 30% fewer compilation errors. This allows for easier migration of legacy code as well as requires less noisy new code.

Unfortunately, similar rules are not applicable to features, in particular, because of their polymorphic nature and inability to do void safety analysis modularly in this case.

Alexander Kogtenkov


Enrico Nardelli <[hidden email]>:

The following code when compiled with 15.12 gives two VJAR compilation errors (Type error: source of assignment is not compatible with target) for both the assignemnt instructions.

When compiled with 17.01 only the last assignment (attac := detac)is flagged as VJAR.

class
    APPLICATION
inherit
    ARGUMENTS
create
    make
feature {NONE} -- Initialization
    attac: attached LINKED_LIST [INTEGER]
    detac: detachable LINKED_LIST [INTEGER]

    make
        local
            loc_attac: attached LINKED_LIST [INTEGER]
            loc_detac: detachable LINKED_LIST [INTEGER]
        do
            create attac.make
            loc_attac := loc_detac
            attac := detac
        end

The project in both environments has the setting VoidSafety: Complete.

Why the different behavior?


--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.



--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Re[2]: [eiffel-users] change in void safety behaviour in 17.01 ?

Colin Adams-4
That's a strawman argument.
The issue is not Eiffel vs most languages - it is Eiffel vs Eiffel versions. You've introduced bad error messages.

On Wed, 17 May 2017 at 12:16 'Alexander Kogtenkov' via Eiffel Users <[hidden email]> wrote:
There is always a tradeoff between explicit and implicit information: additional annotations instead of more flexible code. Of course, there are also different programming styles, and some users prefer one over another. In any case, the new rules allow for less local variables. For example, the snippet

   foo: X
      do
         Result := bar -- `bar` is detachable
         if not attached Result then
            Result := qux -- `qux` is attached
         end
      end

would have to be written with the older rules as

   foo: X
      local
         x: detachable X
      do
         x := bar -- `bar` is detachable
         if attached x then
            Result := x
         else
            Result := qux -- `qux` is attached
         end
      end

that is more verbose and less readable. A variant with object tests is also possible, but still it introduces new locals that pollute name space.

Also, with explicit type annotations some object initialization patterns become impossible.

In the end, void safety serves as a tool to avoid access on void target, and the rules guarantee that in either case. And my current view is that Eiffel does it much better than most existing languages with potential null dereferencing issue.

Alexander Kogtenkov


Colin Adams <[hidden email]>:


This makes life harder for people to reason about the code. In the example above, there should be an error raised, because if you change the last assignment to attac := loc_attac, the wrong error will be raised, I think.
That is, I am assuming it will report the same error, which will certainly puzzle the programmer, as it would be a lie. The correct error to report would be that loc_attac has not been initialized to an attached value (or some such message).

On Wed, 17 May 2017 at 11:19 'Alexander Kogtenkov' via Eiffel Users <[hidden email]> wrote:
Indeed, one of the changes in 16.05 were relaxed void safety rules for local variables and Result (some details can be found at https://www.eiffel.org/doc/eiffelstudio/Major%20changes%20between%20ISE%20Eiffel%2015.12%20and%20ISE%20Eiffel%2016.05). In short, the idea is that attachment status for a local variable is inferred from the code, not is taken from the type declaration. As a consequence, starting from 16.05 attachment marks are ignored for locals.

The change is supported by the observation that with the new rules non-void-safe code triggers 30% fewer compilation errors. This allows for easier migration of legacy code as well as requires less noisy new code.

Unfortunately, similar rules are not applicable to features, in particular, because of their polymorphic nature and inability to do void safety analysis modularly in this case.

Alexander Kogtenkov


Enrico Nardelli <[hidden email]>:

The following code when compiled with 15.12 gives two VJAR compilation errors (Type error: source of assignment is not compatible with target) for both the assignemnt instructions.

When compiled with 17.01 only the last assignment (attac := detac)is flagged as VJAR.

class
    APPLICATION
inherit
    ARGUMENTS
create
    make
feature {NONE} -- Initialization
    attac: attached LINKED_LIST [INTEGER]
    detac: detachable LINKED_LIST [INTEGER]

    make
        local
            loc_attac: attached LINKED_LIST [INTEGER]
            loc_detac: detachable LINKED_LIST [INTEGER]
        do
            create attac.make
            loc_attac := loc_detac
            attac := detac
        end

The project in both environments has the setting VoidSafety: Complete.

Why the different behavior?


--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: Re[2]: [eiffel-users] change in void safety behaviour in 17.01 ?

Bertrand Meyer (ETH)

Dear Colin:

 

This latest tuning-up of the void-safety mechanism may be subject to improvement. But if you look at the matter again I think you will agree that this is going in the right direction. For years people were complaining on this forum that void safety forced them to write useless extra code. Some were actually saying they would not move to void safety because of the problem. After refinements to the mechanism, such complaints complaint went away for *new* code for which – my impression at least – most people  who have looked into the matter are now comfortable with the idea of starting with void safety. The question remains of how to make it easier to adapt *existing* code to void safety. There was still a feeling that it’s too hard. I think the improvements described by Alexander are an important step towards making the adaptation process completely straightforward.

 

As Alexander writes, it’s a tradeoff. But in the scenario you describe I fail to see any semantic danger. We are just simplifying the writing of code by removing conceptually extraneous declarations and instructions. Can there be a “gotcha”, i.e. code that seems to do something and actually does something else? I don’t think so, but may be missing it.

 

You mention potentially misleading error messages. Thanks for bringing up this point. We will take a closer look at the error messages in situations such as those you describe. I don’t think these situations invalidate the soundness of the new scheme as a whole.

 

With best regards,

 

-- Bertrand Meyer

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Colin Adams
Sent: Wednesday, May 17, 2017 13:22
To: [hidden email]
Subject: Re: Re[2]: [eiffel-users] change in void safety behaviour in 17.01 ?

 

That's a strawman argument.

The issue is not Eiffel vs most languages - it is Eiffel vs Eiffel versions. You've introduced bad error messages.

 

On Wed, 17 May 2017 at 12:16 'Alexander Kogtenkov' via Eiffel Users <[hidden email]> wrote:

There is always a tradeoff between explicit and implicit information: additional annotations instead of more flexible code. Of course, there are also different programming styles, and some users prefer one over another. In any case, the new rules allow for less local variables. For example, the snippet

   foo: X
      do
         Result := bar -- `bar` is detachable
         if not attached Result then
            Result := qux -- `qux` is attached
         end
      end

would have to be written with the older rules as

   foo: X
      local
         x: detachable X
      do
         x := bar -- `bar` is detachable
         if attached x then
            Result := x
         else
            Result := qux -- `qux` is attached
         end
      end

that is more verbose and less readable. A variant with object tests is also possible, but still it introduces new locals that pollute name space.

Also, with explicit type annotations some object initialization patterns become impossible.

In the end, void safety serves as a tool to avoid access on void target, and the rules guarantee that in either case. And my current view is that Eiffel does it much better than most existing languages with potential null dereferencing issue.

Alexander Kogtenkov

Colin Adams <[hidden email]>:

 

This makes life harder for people to reason about the code. In the example above, there should be an error raised, because if you change the last assignment to attac := loc_attac, the wrong error will be raised, I think.

That is, I am assuming it will report the same error, which will certainly puzzle the programmer, as it would be a lie. The correct error to report would be that loc_attac has not been initialized to an attached value (or some such message).

 

On Wed, 17 May 2017 at 11:19 'Alexander Kogtenkov' via Eiffel Users <[hidden email]> wrote:

Indeed, one of the changes in 16.05 were relaxed void safety rules for local variables and Result (some details can be found at https://www.eiffel.org/doc/eiffelstudio/Major%20changes%20between%20ISE%20Eiffel%2015.12%20and%20ISE%20Eiffel%2016.05). In short, the idea is that attachment status for a local variable is inferred from the code, not is taken from the type declaration. As a consequence, starting from 16.05 attachment marks are ignored for locals.

The change is supported by the observation that with the new rules non-void-safe code triggers 30% fewer compilation errors. This allows for easier migration of legacy code as well as requires less noisy new code.

Unfortunately, similar rules are not applicable to features, in particular, because of their polymorphic nature and inability to do void safety analysis modularly in this case.

Alexander Kogtenkov

Enrico Nardelli <[hidden email]>:

The following code when compiled with 15.12 gives two VJAR compilation errors (Type error: source of assignment is not compatible with target) for both the assignemnt instructions.

When compiled with 17.01 only the last assignment (attac := detac)is flagged as VJAR.

class
    APPLICATION
inherit
    ARGUMENTS
create
    make
feature {NONE} -- Initialization
    attac: attached LINKED_LIST [INTEGER]
    detac: detachable LINKED_LIST [INTEGER]

    make
        local
            loc_attac: attached LINKED_LIST [INTEGER]
            loc_detac: detachable LINKED_LIST [INTEGER]
        do
            create attac.make
            loc_attac := loc_detac
            attac := detac
        end

The project in both environments has the setting VoidSafety: Complete.

Why the different behavior?

 

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Re[2]: [eiffel-users] change in void safety behaviour in 17.01 ?

Colin Adams-4
Thank-you.
One approach would be to issue a warning message whenever the compiler overrides the programmer's specified type. 
E.g. Warning: Programmer coded loc_attac: attached LINKED_LIST [INTEGER] but compiler inferred loc_attac: detachable LINKED_LIST [INTEGER]

On Wed, 17 May 2017 at 12:37 Bertrand Meyer <[hidden email]> wrote:

Dear Colin:

 

This latest tuning-up of the void-safety mechanism may be subject to improvement. But if you look at the matter again I think you will agree that this is going in the right direction. For years people were complaining on this forum that void safety forced them to write useless extra code. Some were actually saying they would not move to void safety because of the problem. After refinements to the mechanism, such complaints complaint went away for *new* code for which – my impression at least – most people  who have looked into the matter are now comfortable with the idea of starting with void safety. The question remains of how to make it easier to adapt *existing* code to void safety. There was still a feeling that it’s too hard. I think the improvements described by Alexander are an important step towards making the adaptation process completely straightforward.

 

As Alexander writes, it’s a tradeoff. But in the scenario you describe I fail to see any semantic danger. We are just simplifying the writing of code by removing conceptually extraneous declarations and instructions. Can there be a “gotcha”, i.e. code that seems to do something and actually does something else? I don’t think so, but may be missing it.

 

You mention potentially misleading error messages. Thanks for bringing up this point. We will take a closer look at the error messages in situations such as those you describe. I don’t think these situations invalidate the soundness of the new scheme as a whole.

 

With best regards,

 

-- Bertrand Meyer

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Colin Adams
Sent: Wednesday, May 17, 2017 13:22
To: [hidden email]
Subject: Re: Re[2]: [eiffel-users] change in void safety behaviour in 17.01 ?

 

That's a strawman argument.

The issue is not Eiffel vs most languages - it is Eiffel vs Eiffel versions. You've introduced bad error messages.

 

On Wed, 17 May 2017 at 12:16 'Alexander Kogtenkov' via Eiffel Users <[hidden email]> wrote:

There is always a tradeoff between explicit and implicit information: additional annotations instead of more flexible code. Of course, there are also different programming styles, and some users prefer one over another. In any case, the new rules allow for less local variables. For example, the snippet

   foo: X
      do
         Result := bar -- `bar` is detachable
         if not attached Result then
            Result := qux -- `qux` is attached
         end
      end

would have to be written with the older rules as

   foo: X
      local
         x: detachable X
      do
         x := bar -- `bar` is detachable
         if attached x then
            Result := x
         else
            Result := qux -- `qux` is attached
         end
      end

that is more verbose and less readable. A variant with object tests is also possible, but still it introduces new locals that pollute name space.

Also, with explicit type annotations some object initialization patterns become impossible.

In the end, void safety serves as a tool to avoid access on void target, and the rules guarantee that in either case. And my current view is that Eiffel does it much better than most existing languages with potential null dereferencing issue.

Alexander Kogtenkov

Colin Adams <[hidden email]>:

 

This makes life harder for people to reason about the code. In the example above, there should be an error raised, because if you change the last assignment to attac := loc_attac, the wrong error will be raised, I think.

That is, I am assuming it will report the same error, which will certainly puzzle the programmer, as it would be a lie. The correct error to report would be that loc_attac has not been initialized to an attached value (or some such message).

 

On Wed, 17 May 2017 at 11:19 'Alexander Kogtenkov' via Eiffel Users <[hidden email]> wrote:

Indeed, one of the changes in 16.05 were relaxed void safety rules for local variables and Result (some details can be found at https://www.eiffel.org/doc/eiffelstudio/Major%20changes%20between%20ISE%20Eiffel%2015.12%20and%20ISE%20Eiffel%2016.05). In short, the idea is that attachment status for a local variable is inferred from the code, not is taken from the type declaration. As a consequence, starting from 16.05 attachment marks are ignored for locals.

The change is supported by the observation that with the new rules non-void-safe code triggers 30% fewer compilation errors. This allows for easier migration of legacy code as well as requires less noisy new code.

Unfortunately, similar rules are not applicable to features, in particular, because of their polymorphic nature and inability to do void safety analysis modularly in this case.

Alexander Kogtenkov

Enrico Nardelli <[hidden email]>:

The following code when compiled with 15.12 gives two VJAR compilation errors (Type error: source of assignment is not compatible with target) for both the assignemnt instructions.

When compiled with 17.01 only the last assignment (attac := detac)is flagged as VJAR.

class
    APPLICATION
inherit
    ARGUMENTS
create
    make
feature {NONE} -- Initialization
    attac: attached LINKED_LIST [INTEGER]
    detac: detachable LINKED_LIST [INTEGER]

    make
        local
            loc_attac: attached LINKED_LIST [INTEGER]
            loc_detac: detachable LINKED_LIST [INTEGER]
        do
            create attac.make
            loc_attac := loc_detac
            attac := detac
        end

The project in both environments has the setting VoidSafety: Complete.

Why the different behavior?

 

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: Re[2]: [eiffel-users] change in void safety behaviour in 17.01 ?

Bertrand Meyer (ETH)

Great point, and – because warnings are only warnings – I think* we can actually go further: change the semantics of local variables so that they are always detachable. Then “attached T” is an invalid type (error rather than warning). To make sure that no void calls result we rely (as Alexander explained) on CAPs, i.e. certified patterns enforced by the compiler.

 

Then instead of magic performed by the compiler (which was part of your original complaint) we have a clear language rule.

 

This rule has of course to go through the language committee (Ecma), and experience shows that careful examination of such proposals by the committee may reveal inconsistencies or other problems, but at this point the idea looks attractive.

 

By the way, some of the recent improvements are a result of Alexander Kogtenkov’s recently defended PhD thesis, “Void Safety”, which will be soon be made available online. We’ll give the URL then.

 

Many thanks for the comments.

 

-- Bertrand Meyer

*The idea is due to Emmanuel Stapf.

 

 

 

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Colin Adams
Sent: Wednesday, May 17, 2017 13:51
To: [hidden email]
Cc: [hidden email]
Subject: Re: Re[2]: [eiffel-users] change in void safety behaviour in 17.01 ?

 

Thank-you.

One approach would be to issue a warning message whenever the compiler overrides the programmer's specified type. 

E.g. Warning: Programmer coded loc_attac: attached LINKED_LIST [INTEGER] but compiler inferred loc_attac: detachable LINKED_LIST [INTEGER]

 

On Wed, 17 May 2017 at 12:37 Bertrand Meyer <[hidden email]> wrote:

Dear Colin:

 

This latest tuning-up of the void-safety mechanism may be subject to improvement. But if you look at the matter again I think you will agree that this is going in the right direction. For years people were complaining on this forum that void safety forced them to write useless extra code. Some were actually saying they would not move to void safety because of the problem. After refinements to the mechanism, such complaints complaint went away for *new* code for which – my impression at least – most people  who have looked into the matter are now comfortable with the idea of starting with void safety. The question remains of how to make it easier to adapt *existing* code to void safety. There was still a feeling that it’s too hard. I think the improvements described by Alexander are an important step towards making the adaptation process completely straightforward.

 

As Alexander writes, it’s a tradeoff. But in the scenario you describe I fail to see any semantic danger. We are just simplifying the writing of code by removing conceptually extraneous declarations and instructions. Can there be a “gotcha”, i.e. code that seems to do something and actually does something else? I don’t think so, but may be missing it.

 

You mention potentially misleading error messages. Thanks for bringing up this point. We will take a closer look at the error messages in situations such as those you describe. I don’t think these situations invalidate the soundness of the new scheme as a whole.

 

With best regards,

 

-- Bertrand Meyer

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Colin Adams
Sent: Wednesday, May 17, 2017 13:22
To: [hidden email]
Subject: Re: Re[2]: [eiffel-users] change in void safety behaviour in 17.01 ?

 

That's a strawman argument.

The issue is not Eiffel vs most languages - it is Eiffel vs Eiffel versions. You've introduced bad error messages.

 

On Wed, 17 May 2017 at 12:16 'Alexander Kogtenkov' via Eiffel Users <[hidden email]> wrote:

There is always a tradeoff between explicit and implicit information: additional annotations instead of more flexible code. Of course, there are also different programming styles, and some users prefer one over another. In any case, the new rules allow for less local variables. For example, the snippet

   foo: X
      do
         Result := bar -- `bar` is detachable
         if not attached Result then
            Result := qux -- `qux` is attached
         end
      end

would have to be written with the older rules as

   foo: X
      local
         x: detachable X
      do
         x := bar -- `bar` is detachable
         if attached x then
            Result := x
         else
            Result := qux -- `qux` is attached
         end
      end

that is more verbose and less readable. A variant with object tests is also possible, but still it introduces new locals that pollute name space.

Also, with explicit type annotations some object initialization patterns become impossible.

In the end, void safety serves as a tool to avoid access on void target, and the rules guarantee that in either case. And my current view is that Eiffel does it much better than most existing languages with potential null dereferencing issue.

Alexander Kogtenkov

Colin Adams <[hidden email]>:

 

This makes life harder for people to reason about the code. In the example above, there should be an error raised, because if you change the last assignment to attac := loc_attac, the wrong error will be raised, I think.

That is, I am assuming it will report the same error, which will certainly puzzle the programmer, as it would be a lie. The correct error to report would be that loc_attac has not been initialized to an attached value (or some such message).

 

On Wed, 17 May 2017 at 11:19 'Alexander Kogtenkov' via Eiffel Users <[hidden email]> wrote:

Indeed, one of the changes in 16.05 were relaxed void safety rules for local variables and Result (some details can be found at https://www.eiffel.org/doc/eiffelstudio/Major%20changes%20between%20ISE%20Eiffel%2015.12%20and%20ISE%20Eiffel%2016.05). In short, the idea is that attachment status for a local variable is inferred from the code, not is taken from the type declaration. As a consequence, starting from 16.05 attachment marks are ignored for locals.

The change is supported by the observation that with the new rules non-void-safe code triggers 30% fewer compilation errors. This allows for easier migration of legacy code as well as requires less noisy new code.

Unfortunately, similar rules are not applicable to features, in particular, because of their polymorphic nature and inability to do void safety analysis modularly in this case.

Alexander Kogtenkov

Enrico Nardelli <[hidden email]>:

The following code when compiled with 15.12 gives two VJAR compilation errors (Type error: source of assignment is not compatible with target) for both the assignemnt instructions.

When compiled with 17.01 only the last assignment (attac := detac)is flagged as VJAR.

class
    APPLICATION
inherit
    ARGUMENTS
create
    make
feature {NONE} -- Initialization
    attac: attached LINKED_LIST [INTEGER]
    detac: detachable LINKED_LIST [INTEGER]

    make
        local
            loc_attac: attached LINKED_LIST [INTEGER]
            loc_detac: detachable LINKED_LIST [INTEGER]
        do
            create attac.make
            loc_attac := loc_detac
            attac := detac
        end

The project in both environments has the setting VoidSafety: Complete.

Why the different behavior?

 

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [eiffel-users] change in void safety behaviour in 17.01 ?

Eric Bezault
I'm not sure I understand why we are doing all that.

If we wanted to declare a local variable as detachable, then
CAP was doing its work just fine. Why force users who wants
to declared a local variable as attached to actually declare
it as detachable. What is the benefit?

I have the impression that "issue" that all this compiler
magic was trying to address was no so much about local
variables in general, but more about the use of Result.
When the function is declared with an attached type, then
we want Result to be initialized (i.e. attached) at the
end of the routine. But for migration from non-void-safe
mode to void-safe mode, we would like to use it in the
body of the routine as if it was declared as detachable
so that we don't have to declare an extra local variable.
But this is only for Result. For the other local variables
we just have to declare them as detachable if needed, or
as attached if we want to. I don't see why the language
should force to user exclusively use one or the other.

The suggestion below only applies to normal local variables.
Indeed we don't want to force all functions to have their
types declared as detachable. So it's useless.

--
Eric Bezault
mailto:[hidden email]
http://www.gobosoft.com


On 5/18/2017 18:44, Bertrand Meyer wrote:

> Great point, and – because warnings are only warnings – I think* we can
> actually go further: change the semantics of local variables so that
> they are always detachable. Then “attached T” is an invalid type (error
> rather than warning). To make sure that no void calls result we rely (as
> Alexander explained) on CAPs, i.e. certified patterns enforced by the
> compiler.
>
>
>
> Then instead of magic performed by the compiler (which was part of your
> original complaint) we have a clear language rule.
>
>
>
> This rule has of course to go through the language committee (Ecma), and
> experience shows that careful examination of such proposals by the
> committee may reveal inconsistencies or other problems, but at this
> point the idea looks attractive.
>
>
>
> By the way, some of the recent improvements are a result of Alexander
> Kogtenkov’s recently defended PhD thesis, “Void Safety”, which will be
> soon be made available online. We’ll give the URL then.
>
>
>
> Many thanks for the comments.
>
>
>
> -- Bertrand Meyer
>
> *The idea is due to Emmanuel Stapf.
>
>
>
>
>
>
>
>
>
> *From:*[hidden email]
> [mailto:[hidden email]] *On Behalf Of *Colin Adams
> *Sent:* Wednesday, May 17, 2017 13:51
> *To:* [hidden email]
> *Cc:* [hidden email]
> *Subject:* Re: Re[2]: [eiffel-users] change in void safety behaviour in
> 17.01 ?
>
>
>
> Thank-you.
>
> One approach would be to issue a warning message whenever the compiler
> overrides the programmer's specified type.
>
> E.g. Warning: Programmer coded loc_attac: attached LINKED_LIST [INTEGER]
> but compiler inferred loc_attac: detachable LINKED_LIST [INTEGER]
>
>
>
> On Wed, 17 May 2017 at 12:37 Bertrand Meyer <[hidden email]
> <mailto:[hidden email]>> wrote:
>
>     Dear Colin:
>
>
>
>     This latest tuning-up of the void-safety mechanism may be subject to
>     improvement. But if you look at the matter again I think you will
>     agree that this is going in the right direction. For years people
>     were complaining on this forum that void safety forced them to write
>     useless extra code. Some were actually saying they would not move to
>     void safety because of the problem. After refinements to the
>     mechanism, such complaints complaint went away for **new** code for
>     which – my impression at least – most people  who have looked into
>     the matter are now comfortable with the idea of starting with void
>     safety. The question remains of how to make it easier to adapt
>     **existing** code to void safety. There was still a feeling that
>     it’s too hard. I think the improvements described by Alexander are
>     an important step towards making the adaptation process completely
>     straightforward.
>
>
>
>     As Alexander writes, it’s a tradeoff. But in the scenario you
>     describe I fail to see any semantic danger. We are just simplifying
>     the writing of code by removing conceptually extraneous declarations
>     and instructions. Can there be a “gotcha”, i.e. code that seems to
>     do something and actually does something else? I don’t think so, but
>     may be missing it.
>
>
>
>     You mention potentially misleading error messages. Thanks for
>     bringing up this point. We will take a closer look at the error
>     messages in situations such as those you describe. I don’t think
>     these situations invalidate the soundness of the new scheme as a whole.
>
>
>
>     With best regards,
>
>
>
>     -- Bertrand Meyer
>
>
>
>     *From:*[hidden email]
>     <mailto:[hidden email]>
>     [mailto:[hidden email]
>     <mailto:[hidden email]>] *On Behalf Of *Colin Adams
>     *Sent:* Wednesday, May 17, 2017 13:22
>     *To:* [hidden email]
>     <mailto:[hidden email]>
>     *Subject:* Re: Re[2]: [eiffel-users] change in void safety behaviour
>     in 17.01 ?
>
>
>
>     That's a strawman argument.
>
>     The issue is not Eiffel vs most languages - it is Eiffel vs Eiffel
>     versions. You've introduced bad error messages.
>
>
>
>     On Wed, 17 May 2017 at 12:16 'Alexander Kogtenkov' via Eiffel Users
>     <[hidden email]
>     <mailto:[hidden email]>> wrote:
>
>         There is always a tradeoff between explicit and implicit
>         information: additional annotations instead of more flexible
>         code. Of course, there are also different programming styles,
>         and some users prefer one over another. In any case, the new
>         rules allow for less local variables. For example, the snippet
>
>            foo: X
>               do
>                  Result := bar -- `bar` is detachable
>                  if not attached Result then
>                     Result := qux -- `qux` is attached
>                  end
>               end
>
>         would have to be written with the older rules as
>
>            foo: X
>               local
>                  x: detachable X
>               do
>                  x := bar -- `bar` is detachable
>                  if attached x then
>                     Result := x
>                  else
>                     Result := qux -- `qux` is attached
>                  end
>               end
>
>         that is more verbose and less readable. A variant with object
>         tests is also possible, but still it introduces new locals that
>         pollute name space.
>
>         Also, with explicit type annotations some object initialization
>         patterns become impossible.
>
>         In the end, void safety serves as a tool to avoid access on void
>         target, and the rules guarantee that in either case. And my
>         current view is that Eiffel does it much better than most
>         existing languages with potential null dereferencing issue.
>
>         Alexander Kogtenkov
>
>             Colin Adams <[hidden email]
>             <mailto:[hidden email]>>:
>
>
>
>             This makes life harder for people to reason about the code.
>             In the example above, there should be an error raised,
>             because if you change the last assignment to attac :=
>             loc_attac, the wrong error will be raised, I think.
>
>             That is, I am assuming it will report the same error, which
>             will certainly puzzle the programmer, as it would be a lie.
>             The correct error to report would be that loc_attac has not
>             been initialized to an attached value (or some such message).
>
>
>
>             On Wed, 17 May 2017 at 11:19 'Alexander Kogtenkov' via
>             Eiffel Users <[hidden email]
>             <mailto:[hidden email]>> wrote:
>
>                 Indeed, one of the changes in 16.05 were relaxed void
>                 safety rules for local variables and Result (some
>                 details can be found at
>                 https://www.eiffel.org/doc/eiffelstudio/Major%20changes%20between%20ISE%20Eiffel%2015.12%20and%20ISE%20Eiffel%2016.05).
>                 In short, the idea is that attachment status for a local
>                 variable is inferred from the code, not is taken
>                 from the type declaration. As a consequence, starting
>                 from 16.05 attachment marks are ignored for locals.
>
>                 The change is supported by the observation that with the
>                 new rules non-void-safe code triggers 30% fewer
>                 compilation errors. This allows for easier migration of
>                 legacy code as well as requires less noisy new code.
>
>                 Unfortunately, similar rules are not applicable to
>                 features, in particular, because of their polymorphic
>                 nature and inability to do void safety analysis
>                 modularly in this case.
>
>                 Alexander Kogtenkov
>
>                     Enrico Nardelli <[hidden email]
>                     <mailto:[hidden email]>>:
>
>                     The following code when compiled with 15.12 gives
>                     two VJAR compilation errors (Type error: source of
>                     assignment is not compatible with target) for both
>                     the assignemnt instructions.
>
>                     When compiled with 17.01 only the last assignment
>                     (attac := detac)is flagged as VJAR.
>
>                     class
>                         APPLICATION
>                     inherit
>                         ARGUMENTS
>                     create
>                         make
>                     feature {NONE} -- Initialization
>                         attac: attached LINKED_LIST [INTEGER]
>                         detac: detachable LINKED_LIST [INTEGER]
>
>                         make
>                             local
>                                 loc_attac: attached LINKED_LIST [INTEGER]
>                                 loc_detac: detachable LINKED_LIST [INTEGER]
>                             do
>                                 create attac.make
>                                 loc_attac := loc_detac
>                                 attac := detac
>                             end
>
>                     The project in both environments has the setting
>                     VoidSafety: Complete.
>
>                     Why the different behavior?
>
>
>
>                 --
>                 You received this message because you are subscribed to
>                 the Google Groups "Eiffel Users" group.
>                 To unsubscribe from this group and stop receiving emails
>                 from it, send an email to
>                 [hidden email]
>                 <mailto:[hidden email]>.
>                 Visit this group at
>                 https://groups.google.com/group/eiffel-users.
>                 For more options, visit https://groups.google.com/d/optout.
>
>             --
>             You received this message because you are subscribed to the
>             Google Groups "Eiffel Users" group.
>             To unsubscribe from this group and stop receiving emails
>             from it, send an email to
>             [hidden email]
>             <mailto:[hidden email]>.
>             Visit this group at
>             https://groups.google.com/group/eiffel-users.
>             For more options, visit https://groups.google.com/d/optout.
>
>         --
>         You received this message because you are subscribed to the
>         Google Groups "Eiffel Users" group.
>         To unsubscribe from this group and stop receiving emails from
>         it, send an email to [hidden email]
>         <mailto:[hidden email]>.
>         Visit this group at https://groups.google.com/group/eiffel-users.
>         For more options, visit https://groups.google.com/d/optout.
>
>     --
>     You received this message because you are subscribed to the Google
>     Groups "Eiffel Users" group.
>     To unsubscribe from this group and stop receiving emails from it,
>     send an email to [hidden email]
>     <mailto:[hidden email]>.
>     Visit this group at https://groups.google.com/group/eiffel-users.
>     For more options, visit https://groups.google.com/d/optout.
>
>     --
>     You received this message because you are subscribed to the Google
>     Groups "Eiffel Users" group.
>     To unsubscribe from this group and stop receiving emails from it,
>     send an email to [hidden email]
>     <mailto:[hidden email]>.
>     Visit this group at https://groups.google.com/group/eiffel-users.
>     For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google
> Groups "Eiffel Users" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to [hidden email]
> <mailto:[hidden email]>.
> Visit this group at https://groups.google.com/group/eiffel-users.
> For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google
> Groups "Eiffel Users" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to [hidden email]
> <mailto:[hidden email]>.
> Visit this group at https://groups.google.com/group/eiffel-users.
> For more options, visit https://groups.google.com/d/optout.


--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [eiffel-users] change in void safety behaviour in 17.01 ?

Emmanuel Stapf
Administrator
The idea is not to force users to declare their local variable
detachable, but to simply say that there is no point in putting any
attachment marks to the declaration of local variables as the compiler
will not use this information to figure out if all calls will be made
on an attached targets, that actual arguments of a call will be
attached when formals are attached, ...

Manu

On Thu, May 18, 2017 at 10:21 AM, Eric Bezault <[hidden email]> wrote:

> I'm not sure I understand why we are doing all that.
>
> If we wanted to declare a local variable as detachable, then
> CAP was doing its work just fine. Why force users who wants
> to declared a local variable as attached to actually declare
> it as detachable. What is the benefit?
>
> I have the impression that "issue" that all this compiler
> magic was trying to address was no so much about local
> variables in general, but more about the use of Result.
> When the function is declared with an attached type, then
> we want Result to be initialized (i.e. attached) at the
> end of the routine. But for migration from non-void-safe
> mode to void-safe mode, we would like to use it in the
> body of the routine as if it was declared as detachable
> so that we don't have to declare an extra local variable.
> But this is only for Result. For the other local variables
> we just have to declare them as detachable if needed, or
> as attached if we want to. I don't see why the language
> should force to user exclusively use one or the other.
>
> The suggestion below only applies to normal local variables.
> Indeed we don't want to force all functions to have their
> types declared as detachable. So it's useless.
>
> --
> Eric Bezault
> mailto:[hidden email]
> http://www.gobosoft.com
>
>
> On 5/18/2017 18:44, Bertrand Meyer wrote:
>>
>> Great point, and – because warnings are only warnings – I think* we can
>> actually go further: change the semantics of local variables so that
>> they are always detachable. Then “attached T” is an invalid type (error
>> rather than warning). To make sure that no void calls result we rely (as
>> Alexander explained) on CAPs, i.e. certified patterns enforced by the
>> compiler.
>>
>>
>>
>> Then instead of magic performed by the compiler (which was part of your
>> original complaint) we have a clear language rule.
>>
>>
>>
>> This rule has of course to go through the language committee (Ecma), and
>> experience shows that careful examination of such proposals by the
>> committee may reveal inconsistencies or other problems, but at this
>> point the idea looks attractive.
>>
>>
>>
>> By the way, some of the recent improvements are a result of Alexander
>> Kogtenkov’s recently defended PhD thesis, “Void Safety”, which will be
>> soon be made available online. We’ll give the URL then.
>>
>>
>>
>> Many thanks for the comments.
>>
>>
>>
>> -- Bertrand Meyer
>>
>> *The idea is due to Emmanuel Stapf.
>>
>>
>>
>>
>>
>>
>>
>>
>>
>> *From:*[hidden email]
>> [mailto:[hidden email]] *On Behalf Of *Colin Adams
>> *Sent:* Wednesday, May 17, 2017 13:51
>> *To:* [hidden email]
>> *Cc:* [hidden email]
>> *Subject:* Re: Re[2]: [eiffel-users] change in void safety behaviour in
>> 17.01 ?
>>
>>
>>
>> Thank-you.
>>
>> One approach would be to issue a warning message whenever the compiler
>> overrides the programmer's specified type.
>>
>> E.g. Warning: Programmer coded loc_attac: attached LINKED_LIST [INTEGER]
>> but compiler inferred loc_attac: detachable LINKED_LIST [INTEGER]
>>
>>
>>
>> On Wed, 17 May 2017 at 12:37 Bertrand Meyer <[hidden email]
>> <mailto:[hidden email]>> wrote:
>>
>>     Dear Colin:
>>
>>
>>
>>     This latest tuning-up of the void-safety mechanism may be subject to
>>     improvement. But if you look at the matter again I think you will
>>     agree that this is going in the right direction. For years people
>>     were complaining on this forum that void safety forced them to write
>>     useless extra code. Some were actually saying they would not move to
>>     void safety because of the problem. After refinements to the
>>     mechanism, such complaints complaint went away for **new** code for
>>     which – my impression at least – most people  who have looked into
>>     the matter are now comfortable with the idea of starting with void
>>     safety. The question remains of how to make it easier to adapt
>>     **existing** code to void safety. There was still a feeling that
>>     it’s too hard. I think the improvements described by Alexander are
>>     an important step towards making the adaptation process completely
>>     straightforward.
>>
>>
>>
>>     As Alexander writes, it’s a tradeoff. But in the scenario you
>>     describe I fail to see any semantic danger. We are just simplifying
>>     the writing of code by removing conceptually extraneous declarations
>>     and instructions. Can there be a “gotcha”, i.e. code that seems to
>>     do something and actually does something else? I don’t think so, but
>>     may be missing it.
>>
>>
>>
>>     You mention potentially misleading error messages. Thanks for
>>     bringing up this point. We will take a closer look at the error
>>     messages in situations such as those you describe. I don’t think
>>     these situations invalidate the soundness of the new scheme as a
>> whole.
>>
>>
>>
>>     With best regards,
>>
>>
>>
>>     -- Bertrand Meyer
>>
>>
>>
>>     *From:*[hidden email]
>>     <mailto:[hidden email]>
>>     [mailto:[hidden email]
>>     <mailto:[hidden email]>] *On Behalf Of *Colin Adams
>>     *Sent:* Wednesday, May 17, 2017 13:22
>>     *To:* [hidden email]
>>     <mailto:[hidden email]>
>>     *Subject:* Re: Re[2]: [eiffel-users] change in void safety behaviour
>>     in 17.01 ?
>>
>>
>>
>>     That's a strawman argument.
>>
>>     The issue is not Eiffel vs most languages - it is Eiffel vs Eiffel
>>     versions. You've introduced bad error messages.
>>
>>
>>
>>     On Wed, 17 May 2017 at 12:16 'Alexander Kogtenkov' via Eiffel Users
>>     <[hidden email]
>>     <mailto:[hidden email]>> wrote:
>>
>>         There is always a tradeoff between explicit and implicit
>>         information: additional annotations instead of more flexible
>>         code. Of course, there are also different programming styles,
>>         and some users prefer one over another. In any case, the new
>>         rules allow for less local variables. For example, the snippet
>>
>>            foo: X
>>               do
>>                  Result := bar -- `bar` is detachable
>>                  if not attached Result then
>>                     Result := qux -- `qux` is attached
>>                  end
>>               end
>>
>>         would have to be written with the older rules as
>>
>>            foo: X
>>               local
>>                  x: detachable X
>>               do
>>                  x := bar -- `bar` is detachable
>>                  if attached x then
>>                     Result := x
>>                  else
>>                     Result := qux -- `qux` is attached
>>                  end
>>               end
>>
>>         that is more verbose and less readable. A variant with object
>>         tests is also possible, but still it introduces new locals that
>>         pollute name space.
>>
>>         Also, with explicit type annotations some object initialization
>>         patterns become impossible.
>>
>>         In the end, void safety serves as a tool to avoid access on void
>>         target, and the rules guarantee that in either case. And my
>>         current view is that Eiffel does it much better than most
>>         existing languages with potential null dereferencing issue.
>>
>>         Alexander Kogtenkov
>>
>>             Colin Adams <[hidden email]
>>             <mailto:[hidden email]>>:
>>
>>
>>
>>             This makes life harder for people to reason about the code.
>>             In the example above, there should be an error raised,
>>             because if you change the last assignment to attac :=
>>             loc_attac, the wrong error will be raised, I think.
>>
>>             That is, I am assuming it will report the same error, which
>>             will certainly puzzle the programmer, as it would be a lie.
>>             The correct error to report would be that loc_attac has not
>>             been initialized to an attached value (or some such message).
>>
>>
>>
>>             On Wed, 17 May 2017 at 11:19 'Alexander Kogtenkov' via
>>             Eiffel Users <[hidden email]
>>             <mailto:[hidden email]>> wrote:
>>
>>                 Indeed, one of the changes in 16.05 were relaxed void
>>                 safety rules for local variables and Result (some
>>                 details can be found at
>>
>> https://www.eiffel.org/doc/eiffelstudio/Major%20changes%20between%20ISE%20Eiffel%2015.12%20and%20ISE%20Eiffel%2016.05).
>>                 In short, the idea is that attachment status for a local
>>                 variable is inferred from the code, not is taken
>>                 from the type declaration. As a consequence, starting
>>                 from 16.05 attachment marks are ignored for locals.
>>
>>                 The change is supported by the observation that with the
>>                 new rules non-void-safe code triggers 30% fewer
>>                 compilation errors. This allows for easier migration of
>>                 legacy code as well as requires less noisy new code.
>>
>>                 Unfortunately, similar rules are not applicable to
>>                 features, in particular, because of their polymorphic
>>                 nature and inability to do void safety analysis
>>                 modularly in this case.
>>
>>                 Alexander Kogtenkov
>>
>>                     Enrico Nardelli <[hidden email]
>>                     <mailto:[hidden email]>>:
>>
>>                     The following code when compiled with 15.12 gives
>>                     two VJAR compilation errors (Type error: source of
>>                     assignment is not compatible with target) for both
>>                     the assignemnt instructions.
>>
>>                     When compiled with 17.01 only the last assignment
>>                     (attac := detac)is flagged as VJAR.
>>
>>                     class
>>                         APPLICATION
>>                     inherit
>>                         ARGUMENTS
>>                     create
>>                         make
>>                     feature {NONE} -- Initialization
>>                         attac: attached LINKED_LIST [INTEGER]
>>                         detac: detachable LINKED_LIST [INTEGER]
>>
>>                         make
>>                             local
>>                                 loc_attac: attached LINKED_LIST [INTEGER]
>>                                 loc_detac: detachable LINKED_LIST
>> [INTEGER]
>>                             do
>>                                 create attac.make
>>                                 loc_attac := loc_detac
>>                                 attac := detac
>>                             end
>>
>>                     The project in both environments has the setting
>>                     VoidSafety: Complete.
>>
>>                     Why the different behavior?
>>
>>
>>
>>                 --
>>                 You received this message because you are subscribed to
>>                 the Google Groups "Eiffel Users" group.
>>                 To unsubscribe from this group and stop receiving emails
>>                 from it, send an email to
>>                 [hidden email]
>>                 <mailto:[hidden email]>.
>>                 Visit this group at
>>                 https://groups.google.com/group/eiffel-users.
>>                 For more options, visit
>> https://groups.google.com/d/optout.
>>
>>             --
>>             You received this message because you are subscribed to the
>>             Google Groups "Eiffel Users" group.
>>             To unsubscribe from this group and stop receiving emails
>>             from it, send an email to
>>             [hidden email]
>>             <mailto:[hidden email]>.
>>             Visit this group at
>>             https://groups.google.com/group/eiffel-users.
>>             For more options, visit https://groups.google.com/d/optout.
>>
>>         --
>>         You received this message because you are subscribed to the
>>         Google Groups "Eiffel Users" group.
>>         To unsubscribe from this group and stop receiving emails from
>>         it, send an email to [hidden email]
>>         <mailto:[hidden email]>.
>>         Visit this group at https://groups.google.com/group/eiffel-users.
>>         For more options, visit https://groups.google.com/d/optout.
>>
>>     --
>>     You received this message because you are subscribed to the Google
>>     Groups "Eiffel Users" group.
>>     To unsubscribe from this group and stop receiving emails from it,
>>     send an email to [hidden email]
>>     <mailto:[hidden email]>.
>>     Visit this group at https://groups.google.com/group/eiffel-users.
>>     For more options, visit https://groups.google.com/d/optout.
>>
>>     --
>>     You received this message because you are subscribed to the Google
>>     Groups "Eiffel Users" group.
>>     To unsubscribe from this group and stop receiving emails from it,
>>     send an email to [hidden email]
>>     <mailto:[hidden email]>.
>>     Visit this group at https://groups.google.com/group/eiffel-users.
>>     For more options, visit https://groups.google.com/d/optout.
>>
>> --
>> You received this message because you are subscribed to the Google
>> Groups "Eiffel Users" group.
>> To unsubscribe from this group and stop receiving emails from it, send
>> an email to [hidden email]
>> <mailto:[hidden email]>.
>> Visit this group at https://groups.google.com/group/eiffel-users.
>> For more options, visit https://groups.google.com/d/optout.
>>
>> --
>> You received this message because you are subscribed to the Google
>> Groups "Eiffel Users" group.
>> To unsubscribe from this group and stop receiving emails from it, send
>> an email to [hidden email]
>> <mailto:[hidden email]>.
>> Visit this group at https://groups.google.com/group/eiffel-users.
>> For more options, visit https://groups.google.com/d/optout.
>
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Eiffel Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [hidden email].
> Visit this group at https://groups.google.com/group/eiffel-users.
> For more options, visit https://groups.google.com/d/optout.



--
------------------------------------------------------------------------
Eiffel Software
805-685-1006
http://www.eiffel.com
Customer support: http://support.eiffel.com
User group: http://groups.eiffel.com/join
------------------------------------------------------------------------

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
------------------------------------------------------------------------  
Eiffel Software
805-685-1006
http://www.eiffel.com       
Customer support: http://support.eiffel.com       
User group: http://groups.eiffel.com/join       
------------------------------------------------------------------------  
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: [eiffel-users] change in void safety behaviour in 17.01 ?

Bertrand Meyer (ETH)

By the way, the suggestion applies (in contrast with what Eric writes) to all local variables, including Result.

 

One way to explain that suggestion is that "it's only the result that counts", without or with a pun on "result". There is a difference between queries, particularly attributes, and local variables:

 

·         Attributes are persistent between activations of the class (calls); they are features. Declaring an attribute as attached implies a promise by the compiler (if it accepts the code) that whenever someone accesses the attribute )(in appropriate conditions) its value will not be void.

·         Local variables, on the other hand, are transient. They are only useful for a higher purpose: computing features (“computing” in the sense of executing for commands and evaluating for queries). The less we bother programmers with their declarations the better. (In fact, the current IDE has a mechanism that even allows you in some cases not to declare any type at all for a local variable.) It’s in that sense that “only the result counts”: the local variable does not matter in the overall picture (for example in the interface of a class or routine).

 

[Eric]

> Why force users who wants to declared a

> local variable as attached to actually declare it as detachable. What

> is the benefit?

 

The benefit is simple (as in the example first used by Alexander): if you declared a local variable as detachable, you could not assign it to an attached attribute, even if it is guaranteed to be attached from simple static reasoning (CAP). You would need an object test. This is particularly relevant for Result. See Alexander’s original example below.

 

The proposed language mechanism complicates the language definition a bit (for example, as implied by the above observations, we have to permit the attachment of detachable *local* to attached, subject to the appropriate CAP), but that seems justified in light of the simplification for actual programming.

 

-- BM

 

 

 

 

-----Original Message-----
From: [hidden email] [mailto:[hidden email]] On Behalf Of Emmanuel Stapf
Sent: Thursday, May 18, 2017 19:41
To: Eiffel Users <[hidden email]>
Subject: Re: [eiffel-users] change in void safety behaviour in 17.01 ?

 

The idea is not to force users to declare their local variable detachable, but to simply say that there is no point in putting any attachment marks to the declaration of local variables as the compiler will not use this information to figure out if all calls will be made on an attached targets, that actual arguments of a call will be attached when formals are attached, ...

 

Manu

 

On Thu, May 18, 2017 at 10:21 AM, Eric Bezault <[hidden email]> wrote:

> I'm not sure I understand why we are doing all that.

> 

> If we wanted to declare a local variable as detachable, then CAP was

> doing its work just fine. Why force users who wants to declared a

> local variable as attached to actually declare it as detachable. What

> is the benefit?

> 

> I have the impression that "issue" that all this compiler magic was

> trying to address was no so much about local variables in general, but

> more about the use of Result.

> When the function is declared with an attached type, then we want

> Result to be initialized (i.e. attached) at the end of the routine.

> But for migration from non-void-safe mode to void-safe mode, we would

> like to use it in the body of the routine as if it was declared as

> detachable so that we don't have to declare an extra local variable.

> But this is only for Result. For the other local variables we just

> have to declare them as detachable if needed, or as attached if we

> want to. I don't see why the language should force to user exclusively

> use one or the other.

> 

> The suggestion below only applies to normal local variables.

> Indeed we don't want to force all functions to have their types

> declared as detachable. So it's useless.

> 

> --

> Eric Bezault

> [hidden email]

> http://www.gobosoft.com

> 

> 

> On 5/18/2017 18:44, Bertrand Meyer wrote:

>> 

>> Great point, and – because warnings are only warnings – I think* we

>> can actually go further: change the semantics of local variables so

>> that they are always detachable. Then “attached T” is an invalid type

>> (error rather than warning). To make sure that no void calls result

>> we rely (as Alexander explained) on CAPs, i.e. certified patterns

>> enforced by the compiler.

>> 

>> 

>> 

>> Then instead of magic performed by the compiler (which was part of

>> your original complaint) we have a clear language rule.

>> 

>> 

>> 

>> This rule has of course to go through the language committee (Ecma),

>> and experience shows that careful examination of such proposals by

>> the committee may reveal inconsistencies or other problems, but at

>> this point the idea looks attractive.

>> 

>> 

>> 

>> By the way, some of the recent improvements are a result of Alexander

>> Kogtenkov’s recently defended PhD thesis, “Void Safety”, which will

>> be soon be made available online. We’ll give the URL then.

>> 

>> 

>> 

>> Many thanks for the comments.

>> 

>> 

>> 

>> -- Bertrand Meyer

>> 

>> *The idea is due to Emmanuel Stapf.

>> 

>> 

>> 

>> 

>> 

>> 

>> 

>> 

>> 

>> *From:*[hidden email]

>> [[hidden email]] *On Behalf Of *Colin Adams

>> *Sent:* Wednesday, May 17, 2017 13:51

>> *To:* [hidden email]

>> *Cc:* [hidden email]

>> *Subject:* Re: Re[2]: [eiffel-users] change in void safety behaviour

>> in

>> 17.01 ?

>> 

>> 

>> 

>> Thank-you.

>> 

>> One approach would be to issue a warning message whenever the

>> compiler overrides the programmer's specified type.

>> 

>> E.g. Warning: Programmer coded loc_attac: attached LINKED_LIST

>> [INTEGER] but compiler inferred loc_attac: detachable LINKED_LIST

>> [INTEGER]

>> 

>> 

>> 

>> On Wed, 17 May 2017 at 12:37 Bertrand Meyer

>> <[hidden email]>> wrote:

>> 

>>     Dear Colin:

>> 

>> 

>> 

>>     This latest tuning-up of the void-safety mechanism may be subject to

>>     improvement. But if you look at the matter again I think you will

>>     agree that this is going in the right direction. For years people

>>     were complaining on this forum that void safety forced them to write

>>     useless extra code. Some were actually saying they would not move to

>>     void safety because of the problem. After refinements to the

>>     mechanism, such complaints complaint went away for **new** code for

>>     which – my impression at least – most people  who have looked into

>>     the matter are now comfortable with the idea of starting with void

>>     safety. The question remains of how to make it easier to adapt

>>     **existing** code to void safety. There was still a feeling that

>>     it’s too hard. I think the improvements described by Alexander are

>>     an important step towards making the adaptation process completely

>>     straightforward.

>> 

>> 

>> 

>>     As Alexander writes, it’s a tradeoff. But in the scenario you

>>     describe I fail to see any semantic danger. We are just simplifying

>>     the writing of code by removing conceptually extraneous declarations

>>     and instructions. Can there be a “gotcha”, i.e. code that seems to

>>     do something and actually does something else? I don’t think so, but

>>     may be missing it.

>> 

>> 

>> 

>>     You mention potentially misleading error messages. Thanks for

>>     bringing up this point. We will take a closer look at the error

>>     messages in situations such as those you describe. I don’t think

>>     these situations invalidate the soundness of the new scheme as a

>> whole.

>> 

>> 

>> 

>>     With best regards,

>> 

>> 

>> 

>>     -- Bertrand Meyer

>> 

>> 

>> 

>>     *From:*[hidden email]

>>     <[hidden email]>

>>     [mailto:[hidden email]

>>     <[hidden email]>] *On Behalf Of *Colin Adams

>>     *Sent:* Wednesday, May 17, 2017 13:22

>>     *To:* [hidden email]

>>     <[hidden email]>

>>     *Subject:* Re: Re[2]: [eiffel-users] change in void safety behaviour

>>     in 17.01 ?

>> 

>> 

>> 

>>     That's a strawman argument.

>> 

>>     The issue is not Eiffel vs most languages - it is Eiffel vs Eiffel

>>     versions. You've introduced bad error messages.

>> 

>> 

>> 

>>     On Wed, 17 May 2017 at 12:16 'Alexander Kogtenkov' via Eiffel Users

>>     <[hidden email]

>>     <[hidden email]>> wrote:

>> 

>>         There is always a tradeoff between explicit and implicit

>>         information: additional annotations instead of more flexible

>>         code. Of course, there are also different programming styles,

>>         and some users prefer one over another. In any case, the new

>>         rules allow for less local variables. For example, the

>> snippet

>> 

>>            foo: X

>>               do

>>                  Result := bar -- `bar` is detachable

>>                  if not attached Result then

>>                     Result := qux -- `qux` is attached

>>                  end

>>               end

>> 

>>         would have to be written with the older rules as

>> 

>>            foo: X

>>               local

>>                  x: detachable X

>>               do

>>                  x := bar -- `bar` is detachable

>>                  if attached x then

>>                     Result := x

>>                  else

>>                     Result := qux -- `qux` is attached

>>                  end

>>               end

>> 

>>         that is more verbose and less readable. A variant with object

>>         tests is also possible, but still it introduces new locals that

>>         pollute name space.

>> 

>>         Also, with explicit type annotations some object initialization

>>         patterns become impossible.

>> 

>>         In the end, void safety serves as a tool to avoid access on void

>>         target, and the rules guarantee that in either case. And my

>>         current view is that Eiffel does it much better than most

>>         existing languages with potential null dereferencing issue.

>> 

>>         Alexander Kogtenkov

>> 

>>             Colin Adams <[hidden email]

>>             <[hidden email]>>:

>> 

>> 

>> 

>>             This makes life harder for people to reason about the code.

>>             In the example above, there should be an error raised,

>>             because if you change the last assignment to attac :=

>>             loc_attac, the wrong error will be raised, I think.

>> 

>>             That is, I am assuming it will report the same error, which

>>             will certainly puzzle the programmer, as it would be a lie.

>>             The correct error to report would be that loc_attac has not

>>             been initialized to an attached value (or some such message).

>> 

>> 

>> 

>>             On Wed, 17 May 2017 at 11:19 'Alexander Kogtenkov' via

>>             Eiffel Users <[hidden email]

>>             <[hidden email]>> wrote:

>> 

>>                 Indeed, one of the changes in 16.05 were relaxed void

>>                 safety rules for local variables and Result (some

>>                 details can be found at

>> 

>> https://www.eiffel.org/doc/eiffelstudio/Major%20changes%20between%20ISE%20Eiffel%2015.12%20and%20ISE%20Eiffel%2016.05).

>>                 In short, the idea is that attachment status for a local

>>                 variable is inferred from the code, not is taken

>>                 from the type declaration. As a consequence, starting

>>                 from 16.05 attachment marks are ignored for locals.

>> 

>>                 The change is supported by the observation that with the

>>                 new rules non-void-safe code triggers 30% fewer

>>                 compilation errors. This allows for easier migration of

>>                 legacy code as well as requires less noisy new code.

>> 

>>                 Unfortunately, similar rules are not applicable to

>>                 features, in particular, because of their polymorphic

>>                 nature and inability to do void safety analysis

>>                 modularly in this case.

>> 

>>                 Alexander Kogtenkov

>> 

>>                     Enrico Nardelli <[hidden email]

>>                     <[hidden email]>>:

>> 

>>                     The following code when compiled with 15.12 gives

>>                     two VJAR compilation errors (Type error: source of

>>                     assignment is not compatible with target) for both

>>                     the assignemnt instructions.

>> 

>>                     When compiled with 17.01 only the last assignment

>>                     (attac := detac)is flagged as VJAR.

>> 

>>                     class

>>                         APPLICATION

>>                     inherit

>>                         ARGUMENTS

>>                     create

>>                         make

>>                     feature {NONE} -- Initialization

>>                         attac: attached LINKED_LIST [INTEGER]

>>                         detac: detachable LINKED_LIST [INTEGER]

>> 

>>                         make

>>                             local

>>                                 loc_attac: attached LINKED_LIST [INTEGER]

>>                                 loc_detac: detachable LINKED_LIST

>> [INTEGER]

>>                             do

>>                                 create attac.make

>>                                 loc_attac := loc_detac

>>                                 attac := detac

>>                             end

>> 

>>                     The project in both environments has the setting

>>                     VoidSafety: Complete.

>> 

>>                     Why the different behavior?

>> 

>> 

>> 

>>                 --

>>                 You received this message because you are subscribed to

>>                 the Google Groups "Eiffel Users" group.

>>                 To unsubscribe from this group and stop receiving emails

>>                 from it, send an email to

>>                 [hidden email]

>>                 <[hidden email]>.

>>                 Visit this group at

>>                 https://groups.google.com/group/eiffel-users.

>>                 For more options, visit

>> https://groups.google.com/d/optout.

>> 

>>             --

>>             You received this message because you are subscribed to the

>>             Google Groups "Eiffel Users" group.

>>             To unsubscribe from this group and stop receiving emails

>>             from it, send an email to

>>             [hidden email]

>>             <[hidden email]>.

>>             Visit this group at

>>             https://groups.google.com/group/eiffel-users.

>>             For more options, visit https://groups.google.com/d/optout.

>> 

>>         --

>>         You received this message because you are subscribed to the

>>         Google Groups "Eiffel Users" group.

>>         To unsubscribe from this group and stop receiving emails from

>>         it, send an email to [hidden email]

>>         <[hidden email]>.

>>         Visit this group at https://groups.google.com/group/eiffel-users.

>>         For more options, visit https://groups.google.com/d/optout.

>> 

>>     --

>>     You received this message because you are subscribed to the Google

>>     Groups "Eiffel Users" group.

>>     To unsubscribe from this group and stop receiving emails from it,

>>     send an email to [hidden email]

>>     <[hidden email]>.

>>     Visit this group at https://groups.google.com/group/eiffel-users.

>>     For more options, visit https://groups.google.com/d/optout.

>> 

>>     --

>>     You received this message because you are subscribed to the Google

>>     Groups "Eiffel Users" group.

>>     To unsubscribe from this group and stop receiving emails from it,

>>     send an email to [hidden email]

>>     <[hidden email]>.

>>     Visit this group at https://groups.google.com/group/eiffel-users.

>>     For more options, visit https://groups.google.com/d/optout.

>> 

>> --

>> You received this message because you are subscribed to the Google

>> Groups "Eiffel Users" group.

>> To unsubscribe from this group and stop receiving emails from it,

>> send an email to [hidden email]

>> <[hidden email]>.

>> Visit this group at https://groups.google.com/group/eiffel-users.

>> For more options, visit https://groups.google.com/d/optout.

>> 

>> --

>> You received this message because you are subscribed to the Google

>> Groups "Eiffel Users" group.

>> To unsubscribe from this group and stop receiving emails from it,

>> send an email to [hidden email]

>> <[hidden email]>.

>> Visit this group at https://groups.google.com/group/eiffel-users.

>> For more options, visit https://groups.google.com/d/optout.

> 

> 

> 

> --

> You received this message because you are subscribed to the Google

> Groups "Eiffel Users" group.

> To unsubscribe from this group and stop receiving emails from it, send

> an email to [hidden email].

> Visit this group at https://groups.google.com/group/eiffel-users.

> For more options, visit https://groups.google.com/d/optout.

 

 

 

--

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

Eiffel Software

805-685-1006

http://www.eiffel.com

Customer support: http://support.eiffel.com User group: http://groups.eiffel.com/join

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

 

--

You received this message because you are subscribed to the Google Groups "Eiffel Users" group.

To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].

Visit this group at https://groups.google.com/group/eiffel-users.

For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [eiffel-users] change in void safety behaviour in 17.01 ?

Eric Bezault
In reply to this post by Emmanuel Stapf
On 5/18/2017 19:40, Emmanuel Stapf wrote:
> The idea is not to force users to declare their local variable
> detachable, but to simply say that there is no point in putting any
> attachment marks to the declaration of local variables as the compiler
> will not use this information to figure out if all calls will be made
> on an attached targets, that actual arguments of a call will be
> attached when formals are attached, ...

You really lost me here. Should "attached T" for a local variable
be invalid or not? In Bertrand's message I understood that it should
be invalid. So you are forcing users to declare their local variables
as detachable. That's what it is.

Then Bertrand says that there is not special treatment for Result.
It's a local variable like any other local variable. So, it would
be invalid to declare the type of a function as attached.

--
Eric Bezault
mailto:[hidden email]
http://www.gobosoft.com

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: [eiffel-users] change in void safety behaviour in 17.01 ?

Bertrand Meyer (ETH)
There is no type declaration for Result. Only for the function.

-- BM

-----Original Message-----
From: [hidden email] [mailto:[hidden email]] On Behalf Of Eric Bezault
Sent: Thursday, May 18, 2017 20:40
To: [hidden email]
Subject: Re: [eiffel-users] change in void safety behaviour in 17.01 ?

On 5/18/2017 19:40, Emmanuel Stapf wrote:
> The idea is not to force users to declare their local variable
> detachable, but to simply say that there is no point in putting any
> attachment marks to the declaration of local variables as the compiler
> will not use this information to figure out if all calls will be made
> on an attached targets, that actual arguments of a call will be
> attached when formals are attached, ...

You really lost me here. Should "attached T" for a local variable be invalid or not? In Bertrand's message I understood that it should be invalid. So you are forcing users to declare their local variables as detachable. That's what it is.

Then Bertrand says that there is not special treatment for Result.
It's a local variable like any other local variable. So, it would be invalid to declare the type of a function as attached.

--
Eric Bezault
mailto:[hidden email]
http://www.gobosoft.com

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [eiffel-users] change in void safety behaviour in 17.01 ?

Eric Bezault
In reply to this post by Bertrand Meyer (ETH)
On 5/18/2017 20:10, Bertrand Meyer wrote:
> By the way, the suggestion applies (in contrast with what Eric writes)
> to all local variables, including Result.

You said that "attached T" would be an invalid type for a local
variable. You said that it would be an error, not a warning.
So if this applies to all local variables, including Result,
then it would not be valid anymore to declare a function of type
"attached T".

> The benefit is simple (as in the example first used by Alexander): if
> you declared a local variable as detachable, you could not assign it to
> an attached attribute, even if it is guaranteed to be attached from
> simple static reasoning (CAP). You would need an object test.

Really? The CAP is just for that purpose. And as far as I know it
worked even before 16.05.

> This is particularly relevant for Result.

So we are back to what I wanted to point out. Result is different
from other local variables. With a normal local variable the user
has the choice to declare it as detachable and let the CAP do its
job. The real problem is with Result because if we want the type
of a function to be attached we cannot, as a user, change type of
Result to detachable without some magic from the compiler. This
magic is not needed for the other local variables because the user
can explicitly declare them as detachable if that's what they want.

--
Eric Bezault
mailto:[hidden email]
http://www.gobosoft.com

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [eiffel-users] change in void safety behaviour in 17.01 ?

Eric Bezault
In reply to this post by Bertrand Meyer (ETH)
On 5/18/2017 20:43, Bertrand Meyer wrote:
> There is no type declaration for Result. Only for the function.

So you are saying that the type of Result would not be the type of
the function anymore, but its detachable version.

But still, you are forcing users to detachable other local variables
as detachable even though there is no need for that.
(And of course the language definition would need to be more
subtle than that because we don't want to have to write
"detachable INTEGER".)

So, I had code in non-void safe mode of the form:

local
     s: STRING
do
     s := "foo"
     s.f

and now, in void-safe mode that code would be invalid because
I need to declare `s' as 'detachable STRING'.

--
Eric Bezault
mailto:[hidden email]
http://www.gobosoft.com

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: [eiffel-users] change in void safety behaviour in 17.01 ?

Bertrand Meyer (ETH)

Dear Eric:

 

("detachable INTEGER": clearly this discussion applies to reference types only.)

 

At Eiffel Software we are pretty convinced that the mechanism is the right thing to adopt, but -- even if we are right -- that conviction is not of much use unless we can explain that mechanism. So this whole discussion is extremely useful.

 

The basic idea is not really that all locals are detachable but that their attachment status is best left for automatic inference. Perhaps we can say that there are three attachment statuses: attached, detachable and automatic. Local variables are automatic. In using them, the programmer can just ignore attachment marks and let the compiler do the job.

 

II

CI

AP

CR

ED

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

DO

 

Bear with me as I restart from basics, even if I sound pedantic. In the non-void-safe (non-Eiffel) Dangerous OO World (DO), void calls (null pointer dereferences) are a major threat. At the other extreme there is an Impossible Ideal world (II), where programmers never write programs that cause void calls. People not being perfect, we cannot assume II. The next best thing to II is the Conceivable Ideal world (CI), where programmers can mess up but compilers will reject void-unsafe programs, at minimal or zero extra programmer effort. In fact CI almost exists today thanks to proof tools such as AutoProof for Eiffel (a research tool, see http://se.inf.ethz.ch/research/autoproof/tutorial/). For circumstantial reasons AutoProof does not use modern Eiffel's void safety and does its own proofs of void safety. CI can also be called the static analysis world. The downside is that when you let the compiler tell you whether your program is void-safe or not there is, particular for a programmer who is not an expert in program formalization, a certain dose of magic, or if you prefer a lottery: you try to write your program in a void-safe mode, of course (imagining that you are in II); if the compiler, oracle-like, accepts it great, if not you have to figure out the oracle's pronouncement. So a more convincing version of AP would be the Clear-Rules world (CR), where you have to follow simple to understand, clearly expressed rules in calls, and your program -- without further annotation -- would compile if and only if it followed these rules (and then would be guaranteed to be void-safe). The day we figure out CR we don't need any void-safety constructs any more. We are not quite there yet, so we have to settle for the next best thing, the Explicit Declaration world (ED) where the programmer has to add some annotations to guarantee void safety. Currently the annotations are "detachable" marks and object tests.

 

ED is the current solution: void-safe Eiffel. (Note that all the variants above the line in the preceding figure are void-safe; only DO is not.)

 

But the annotations of ED are imposed by necessity. No one grows up dreaming of a job writing "attached" marks and object tests. Somewhere we all yearn for CR where we just write our programs as we please – following some clear, explicit rules -- and the compiler figures out the void safety guarantees.

 

The mechanism that Alexander Kogtenkov described is an important step in going from ED to CR, by forsaking the attachment declarations -- in other words, leaving the programmer in peace -- for local variables.

 

The basic rule is simple (as usual working out the details may take some more time): local variables do not have attachment marks (and to avoid any ambiguity, specifying "attached" for a local will trigger not just a warning as Colin Adams initially suggested but a good old error); simple CAPs (patterns of valid use) will enable static analysis that guarantees -- if it accepts the code -- the absence of void calls.

 

It may be possible in the future to extend this CR-style approach further, but what we are proposing right now is to remove the annotation burden for locals, because it seems possible and straightforward.

 

With best regards,

 

-- Bertrand Meyer

 

 

 

-----Original Message-----
From: [hidden email] [mailto:[hidden email]] On Behalf Of Eric Bezault
Sent: Thursday, May 18, 2017 21:00
To: [hidden email]
Cc: [hidden email]
Subject: Re: [eiffel-users] change in void safety behaviour in 17.01 ?

 

On 5/18/2017 20:43, Bertrand Meyer wrote:

> There is no type declaration for Result. Only for the function.

 

So you are saying that the type of Result would not be the type of the function anymore, but its detachable version.

 

But still, you are forcing users to detachable other local variables as detachable even though there is no need for that.

(And of course the language definition would need to be more subtle than that because we don't want to have to write "detachable INTEGER".)

 

So, I had code in non-void safe mode of the form:

 

local

     s: STRING

do

     s := "foo"

     s.f

 

and now, in void-safe mode that code would be invalid because I need to declare `s' as 'detachable STRING'.

 

--

Eric Bezault

[hidden email]

http://www.gobosoft.com

 

--

You received this message because you are subscribed to the Google Groups "Eiffel Users" group.

To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].

Visit this group at https://groups.google.com/group/eiffel-users.

For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [eiffel-users] change in void safety behaviour in 17.01 ?

Thomas Beale-4
In reply to this post by Eric Bezault

Surely the rule has to be that the type of Result has to be the type of its function, which is the return type in the signature, detachable or attached as per the global setting adopted for the system (these days for most people, default = attached). But the default of all other locals would be detachable unless marked 'attached'?

- thomas

On 18/05/2017 19:59, Eric Bezault wrote:
On 5/18/2017 20:43, Bertrand Meyer wrote:
There is no type declaration for Result. Only for the function.

So you are saying that the type of Result would not be the type of
the function anymore, but its detachable version.

But still, you are forcing users to detachable other local variables
as detachable even though there is no need for that.
(And of course the language definition would need to be more
subtle than that because we don't want to have to write
"detachable INTEGER".)

So, I had code in non-void safe mode of the form:

local
    s: STRING
do
    s := "foo"
    s.f

and now, in void-safe mode that code would be invalid because
I need to declare `s' as 'detachable STRING'.



--
Thomas Beale
Principal, Ars Semantica
Consultant, ABD Team, Intermountain Healthcare
Management Board, Specifications Program Lead, openEHR Foundation
Chartered IT Professional Fellow, BCS, British Computer Society
Health IT blog | Culture blog

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: [eiffel-users] change in void safety behaviour in 17.01 ?

Bertrand Meyer (ETH)

The rule is the same for Result as for other local variables. Result is treated as a variable of the detachable variant of the function’s type. The rule is simply that on function exit the value of that variable is attached.

 

-- BM

 

PS Although this is probably clear to all let me note the two uses of “attached” and “detachable”, other than triggering Outlook’s solicitousness: “detachable” is a property of the type (the alternative to “attached”, as a property of the type, also known as “statically attached”); “attached” as the last word in the previous paragraph is a property of a (reference) value, also known as “dynamically attached”.

 

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of Woland's Cat
Sent: Friday, May 19, 2017 15:05
To: [hidden email]
Subject: Re: [eiffel-users] change in void safety behaviour in 17.01 ?

 


Surely the rule has to be that the type of Result has to be the type of its function, which is the return type in the signature, detachable or attached as per the global setting adopted for the system (these days for most people, default = attached). But the default of all other locals would be detachable unless marked 'attached'?

- thomas

On 18/05/2017 19:59, Eric Bezault wrote:

On 5/18/2017 20:43, Bertrand Meyer wrote:

There is no type declaration for Result. Only for the function.


So you are saying that the type of Result would not be the type of
the function anymore, but its detachable version.

But still, you are forcing users to detachable other local variables
as detachable even though there is no need for that.
(And of course the language definition would need to be more
subtle than that because we don't want to have to write
"detachable INTEGER".)

So, I had code in non-void safe mode of the form:

local
    s: STRING
do
    s := "foo"
    s.f

and now, in void-safe mode that code would be invalid because
I need to declare `s' as 'detachable STRING'.

 

 

--
Thomas Beale
Principal, Ars Semantica
Consultant, ABD Team, Intermountain Healthcare
Management Board, Specifications Program Lead, openEHR Foundation
Chartered IT Professional Fellow, BCS, British Computer Society
Health IT blog | Culture blog

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
Visit this group at https://groups.google.com/group/eiffel-users.
For more options, visit https://groups.google.com/d/optout.
Loading...