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

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

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

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.

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

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