RE: [eiffel-users] change in void safety behaviour in 17.01 ? (proofread, read this one.

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

RE: [eiffel-users] change in void safety behaviour in 17.01 ? (proofread, read this one.

Bertrand Meyer (ETH)

(Fixed a couple of typos – BM.)

 

 

Dear Eric:

 

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

 

At Eiffel Software we are pretty much convinced right now 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

CR

ED

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

DO

 

Bear with me as I restart from basics, at the risk of sounding pedantic. In the non-void-safe (non-Eiffel) Dangerous OO World (DO, top level in the chart above), void calls (null pointer dereferences) are a major threat. At the other extreme (bottom level) 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 second best thing to II is the Conceivable Ideal world (CI), next level down, 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 prototype available online, see http://se.inf.ethz.ch/research/autoproof/tutorial/). For circumstantial reasons AutoProof does not use modern Eiffel's void safety and performs its own proofs of void safety. CI can also be called the static analysis world.

 

The downside of working in CI is that when you depend on the compiler tell you whether your program is void-safe there is, particularly for a programmer who is not an expert in program formalization, a certain dose of magic, or if you prefer  lottery: you try to write your program so as to avoid void calls (reaching for 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 CI 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 won’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 "detachable" 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 up from ED to CR, by forsaking the attachment declarations -- in other words, making an effort not to bother the programmer  -- for local variables.

 

The basic rule is simple (although as usual working out the details might 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] [[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 ? (proofread, read this one.

ctillman
It seems like a very good direction to me. The fuller explanation is much appreciated.

On Thu, May 18, 2017 at 9:05 PM, Bertrand Meyer <[hidden email]> wrote:

(Fixed a couple of typos – BM.)

 

 

Dear Eric:

 

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

 

At Eiffel Software we are pretty much convinced right now 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

CR

ED

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

DO

 

Bear with me as I restart from basics, at the risk of sounding pedantic. In the non-void-safe (non-Eiffel) Dangerous OO World (DO, top level in the chart above), void calls (null pointer dereferences) are a major threat. At the other extreme (bottom level) 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 second best thing to II is the Conceivable Ideal world (CI), next level down, 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 prototype available online, see http://se.inf.ethz.ch/research/autoproof/tutorial/). For circumstantial reasons AutoProof does not use modern Eiffel's void safety and performs its own proofs of void safety. CI can also be called the static analysis world.

 

The downside of working in CI is that when you depend on the compiler tell you whether your program is void-safe there is, particularly for a programmer who is not an expert in program formalization, a certain dose of magic, or if you prefer  lottery: you try to write your program so as to avoid void calls (reaching for 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 CI 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 won’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 "detachable" 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 up from ED to CR, by forsaking the attachment declarations -- in other words, making an effort not to bother the programmer  -- for local variables.

 

The basic rule is simple (although as usual working out the details might 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] [[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.



--
Chris Tillman
Developer

--
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 ? (proofread, read this one.

Enrico Nardelli
In reply to this post by Bertrand Meyer (ETH)

Using Eiffel mainly for teaching OO programming, I think the viewpoint of the three attachment statuses is the best way to understand and describe the situation.

It keeps conceptual clarity by making it explicit that
the programmer has not to declare the attachment status of local variables, since the compiler will apply special efforts to guarantee void safety.

The situation with Result is just one bit more complex, since Result is never explicitly declared. But one can always describe it AS IF there were a
  local
    Result: X 
declaration at the beginning of each query routine returning a value of type X. Then the previous reasoning applies

It's not yet 100% clear to me whether the programmer is also dispensed with using object tests on locals. I would say so, but a confirmation is appreciated.

In any case I think it's a nice advance!

Best, Enrico


Il 19/05/2017 05:05, Bertrand Meyer ha scritto:

(Fixed a couple of typos – BM.)

 

 

Dear Eric:

 

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

 

At Eiffel Software we are pretty much convinced right now 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

CR

ED

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

DO

 

Bear with me as I restart from basics, at the risk of sounding pedantic. In the non-void-safe (non-Eiffel) Dangerous OO World (DO, top level in the chart above), void calls (null pointer dereferences) are a major threat. At the other extreme (bottom level) 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 second best thing to II is the Conceivable Ideal world (CI), next level down, 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 prototype available online, see http://se.inf.ethz.ch/research/autoproof/tutorial/). For circumstantial reasons AutoProof does not use modern Eiffel's void safety and performs its own proofs of void safety. CI can also be called the static analysis world.

 

The downside of working in CI is that when you depend on the compiler tell you whether your program is void-safe there is, particularly for a programmer who is not an expert in program formalization, a certain dose of magic, or if you prefer  lottery: you try to write your program so as to avoid void calls (reaching for 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 CI 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 won’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 "detachable" 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 up from ED to CR, by forsaking the attachment declarations -- in other words, making an effort not to bother the programmer  -- for local variables.

 

The basic rule is simple (although as usual working out the details might 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] [[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.

-- EN

=====================================================================
Prof. Enrico Nardelli
Dipartimento di Matematica - Universita' di Roma "Tor Vergata"
Via della Ricerca Scientifica snc - 00133 Roma
tel: +39 06 7259.4204    fax: +39 06 7259.4699
mobile: +39 335 590.2331     e-mail: [hidden email]
home page: http://www.mat.uniroma2.it/~nardelli
blog: http://www.ilfattoquotidiano.it/blog/enardelli/
=====================================================================
-- 

--
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 ? (proofread, read this one.

Eric Bezault
In reply to this post by Bertrand Meyer (ETH)
On 5/19/2017 05:05, Bertrand Meyer wrote:
> 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.

Do we really need to introduce this new attachment status?

What about: when no attachment mark is explicitly specified, then
the default is attached everywhere except for local types where is
detachable. That's the only modification to be made in the Eiffel
standard. The other modification is in the ECF file where a new
option needs to be added: 'local_detachable_by_default' in the
same way we already have 'attached_by_default' for all other types.

With that in place, migration of code from non-void-safe to void-safe
such as:

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

would work without a change. And still, users may still want to add
the explicit 'attached' mark if they really want to. There is no reason
to forbid them to do that, even if the compiler is smarter than
humans (in the same way we can let the user specify the type of a local
variable explicitly even when the compiler can infer it).

--
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 ? (proofread, read this one.

Bertrand Meyer (ETH)
Dear Eric:

Yes, what you describe is exactly the idea!

As to "automatic", I was not suggesting we formally introduce a third attachment status into the language. That concept was just intended for pedagogical purposes, part of my explanation of the mechanism. But your explanation is better.

Thanks,

-- Bertrand Meyer
PS On the lighter side (no connection to Eiffel or the concepts under discussion): I know that when I click "Send" Outlook is going to come up with a popup helpfully asking me if I did not by any chance forget to attach a file to this message. This happens whenever an email has words like "attached" or "attachment" but no attached file, usually revealing a case of the Forgotten Attachment Syndrome, well known to absent-minded and hurried emailers. Now here is a task for AI (deep learning?): using the archive of this forum as training set, devise an algorithm to decide correctly when the content of a message justifies the pop-up and when it does not.

-----Original Message-----
From: Eric Bezault [mailto:[hidden email]]
Sent: Friday, May 19, 2017 07:27
To: [hidden email]; [hidden email]
Cc: [hidden email]
Subject: Re: [eiffel-users] change in void safety behaviour in 17.01 ? (proofread, read this one.

On 5/19/2017 05:05, Bertrand Meyer wrote:
> 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.

Do we really need to introduce this new attachment status?

What about: when no attachment mark is explicitly specified, then the default is attached everywhere except for local types where is detachable. That's the only modification to be made in the Eiffel standard. The other modification is in the ECF file where a new option needs to be added: 'local_detachable_by_default' in the same way we already have 'attached_by_default' for all other types.

With that in place, migration of code from non-void-safe to void-safe such as:

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

would work without a change. And still, users may still want to add the explicit 'attached' mark if they really want to. There is no reason to forbid them to do that, even if the compiler is smarter than humans (in the same way we can let the user specify the type of a local variable explicitly even when the compiler can infer it).

--
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 ? (proofread, read this one.

Thomas Beale-4
In reply to this post by Bertrand Meyer (ETH)

This is a very nice explanation, and I think would be essential in any textbook like material on the subject, to make it clear that the whole void safety concept of today is the art of the possible - a waypoint in a journey to a point of 'perfect programming', which presumably exists where parallel lines meet ...

- thomas

On 19/05/2017 04:05, Bertrand Meyer wrote:

(Fixed a couple of typos – BM.)

 

 

Dear Eric:

 

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

 

At Eiffel Software we are pretty much convinced right now 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

CR

ED

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

DO

 

Bear with me as I restart from basics, at the risk of sounding pedantic. In the non-void-safe (non-Eiffel) Dangerous OO World (DO, top level in the chart above), void calls (null pointer dereferences) are a major threat. At the other extreme (bottom level) 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 second best thing to II is the Conceivable Ideal world (CI), next level down, 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 prototype available online, see http://se.inf.ethz.ch/research/autoproof/tutorial/). For circumstantial reasons AutoProof does not use modern Eiffel's void safety and performs its own proofs of void safety. CI can also be called the static analysis world.

 

The downside of working in CI is that when you depend on the compiler tell you whether your program is void-safe there is, particularly for a programmer who is not an expert in program formalization, a certain dose of magic, or if you prefer  lottery: you try to write your program so as to avoid void calls (reaching for 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 CI 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 won’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 "detachable" 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 up from ED to CR, by forsaking the attachment declarations -- in other words, making an effort not to bother the programmer  -- for local variables.

 

The basic rule is simple (although as usual working out the details might 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,

 


--
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...