• bearophile (16/16) Nov 24 2014 If a function returns a lazy range, I can't verify its
• Peter Alexander (3/3) Nov 24 2014 Should be able to do:
• bearophile (13/16) Nov 24 2014 Mine was just an example of the general problem, another example:
• Peter Alexander (8/25) Nov 24 2014 Chunks.save should also be const, so result.save.{...} should
• bearophile (6/12) Nov 24 2014 But it doesn't. Should I have to file two bug reports (ERs) on
• Peter Alexander (10/15) Nov 24 2014 I suppose chunks should be inout, because you might want mutable

"bearophile" <bearophileHUGS lycos.com> writes:

If a function returns a lazy range, I can't verify its 
correctness in the function post-condition because inside the 
post-condition such range is const.

An example of the problem:


import std.range, std.algorithm;

auto foo()
out(result) {
     assert(result.all!(x => x < 10));
} body {
     return iota(5);
}

void main() {}


This limits the usefulness of post-conditions in my code. Do you 
have ideas to solve this problem?

Bye,
bearophile

"Peter Alexander" <peter.alexander.au gmail.com> writes:

Should be able to do:

assert(result.save.all!(x => x < 10));

But iota's save isn't const, so you can't (that's a bug).

"bearophile" <bearophileHUGS lycos.com> writes:

Peter Alexander:

 Should be able to do:

 assert(result.save.all!(x => x < 10));

 But iota's save isn't const, so you can't (that's a bug).

Mine was just an example of the general problem, another example:


import std.range, std.algorithm;

auto foo()
out(result) {
     assert(result.all!(b => b.length == 2));
} body {
     auto a = new int[10];
     return a.chunks(2);
}

void main() {}


Bye,
bearophile

"Peter Alexander" <peter.alexander.au gmail.com> writes:

On Monday, 24 November 2014 at 12:20:40 UTC, bearophile wrote:
 Peter Alexander:

 Should be able to do:

 assert(result.save.all!(x => x < 10));

 But iota's save isn't const, so you can't (that's a bug).

 Mine was just an example of the general problem, another 
 example:


 import std.range, std.algorithm;

 auto foo()
 out(result) {
     assert(result.all!(b => b.length == 2));
 } body {
     auto a = new int[10];
     return a.chunks(2);
 }

 void main() {}

Chunks.save should also be const, so result.save.{...} should 
work.

It becomes a real problem with input ranges, because you can't 
save them. That makes sense though, as there is no way to consume 
the result in a post-condition check that doesn't consume it. 
That's just a fact of life and a limitation of trying to verify 
mutable data.

"bearophile" <bearophileHUGS lycos.com> writes:

Peter Alexander:

 Chunks.save should also be const, so result.save.{...} should 
 work.

But it doesn't. Should I have to file two bug reports (ERs) on 
iota and chunks?


 It becomes a real problem with input ranges, because you can't 
 save them. That makes sense though, as there is no way to 
 consume the result in a post-condition check that doesn't 
 consume it.

I agree.

Bye,
bearophile

"Peter Alexander" <peter.alexander.au gmail.com> writes:

On Monday, 24 November 2014 at 14:20:02 UTC, bearophile wrote:
 Peter Alexander:

 Chunks.save should also be const, so result.save.{...} should 
 work.

 But it doesn't. Should I have to file two bug reports (ERs) on 
 iota and chunks?

I suppose chunks should be inout, because you might want mutable 
chunks.

You could file bug reports, but you can't really add const/inout 
manually in templates. The dependencies on the const-ness of 
template parameters makes it unmanageable. You need it to be 
inferred.

See:

https://issues.dlang.org/show_bug.cgi?id=7521
https://issues.dlang.org/show_bug.cgi?id=8407