Why can't a return statement be present in a contract? A contract is basically a function returning void. And those can have return statements.
Seems like a pointless restriction to me...
Comment #1 by andrej.mitrovich — 2014-05-09T20:38:28Z
Test-case?
Comment #2 by monarchdodra — 2014-05-09T20:51:20Z
(In reply to Andrej Mitrovic from comment #1)
> Test-case?
//----
void foo(int i)
in
{
if (i == 0)
return;
assert(10/i > 1);
}
body
{
}
//----
Comment #3 by andrej.mitrovich — 2014-05-09T20:59:39Z
Yeah it seems like an arbitrary limitation since invariants allow return statements.
Comment #4 by bearophile_hugs — 2014-05-11T18:28:22Z
I am strongly against this and I suggest to close this issue down as soon as possible. My vote is -2. Please don't turn D contracts programming into a semantic soup.
(In reply to Andrej Mitrovic from comment #3)
> Yeah it seems like an arbitrary limitation since invariants allow return
> statements.
I didn't know this, let's remove returns from invariants ASAP. I'll open an ER to ask them to be removed.
Comment #5 by bearophile_hugs — 2014-05-11T18:30:44Z
(In reply to Andrej Mitrovic from comment #3)
> Yeah it seems like an arbitrary limitation since invariants allow return
> statements.
That limitation is very far from being arbitrary.
Comment #6 by monarchdodra — 2014-05-11T19:30:09Z
(In reply to bearophile_hugs from comment #4)
> I am strongly against this...
Why though? What's your arguments?
It's pretty arbitrary. If you don't *need* to use a return, then don't use one. If you *do* need a return, why would we want to restrain it?
Comment #7 by bearophile_hugs — 2014-05-11T20:26:47Z
(In reply to monarchdodra from comment #6)
> What's your arguments?
Is return from contract present in the DbC of Eiffel/Ada/C#/Racket? What does it means returning from a test that verifies if a contract is holding? I think allowing returns goes against the meaning of contracts. They are not meant to change the flow of the code, all they have to do is to verify the input or outputs or invariants are correct.
Comment #8 by monarchdodra — 2014-05-11T21:23:56Z
(In reply to bearophile_hugs from comment #7)
> (In reply to monarchdodra from comment #6)
>
> > What's your arguments?
>
> What does it means returning from a test that
> verifies if a contract is holding?
It means you've tested what needs to be tested, and the input given need to proceed with the rest of the code.
Actual example in phobos:
auto assumeSorted(Range)(Range r)
in
{
if (range.length <= 1) return;
//more than 1 element, do actual tests
...
}
body
> I think allowing returns goes against the meaning of contracts. They are not
> meant to change the flow of the code, all they have to do is to verify the
> input or outputs or invariants are correct.
"Flow of code" does not mean the code actual "does" anything, and I see nothing wrong with having control structures in a contract.
Not being able to return in the middle of the contract is basically *forcing* the "single point of exit" paradigm. And we know how that ends...
In any case, it's completely inconsistent with the rest of the language. Besides, it can be just as easily worked around with:
in
{
void doTest(){...}
doTest();
}
or
in
{{
if (...)
goto end;
}end:}
Long story short: If you *do* need to prematurely end the function, you are forced to write crap.
Comment #9 by bearophile_hugs — 2014-05-11T21:53:16Z
(In reply to monarchdodra from comment #8)
> It means you've tested what needs to be tested, and the input given need to
> proceed with the rest of the code.
So the return ends just the contract. I misunderstood this, sorry.
Comment #10 by monarchdodra — 2014-05-12T19:18:22Z
(In reply to bearophile_hugs from comment #9)
> (In reply to monarchdodra from comment #8)
>
> > It means you've tested what needs to be tested, and the input given need to
> > proceed with the rest of the code.
>
> So the return ends just the contract. I misunderstood this, sorry.
I understand why you are against this now. Seems like a misunderstanding on what the return would actually do.
Comment #11 by deadalnix — 2016-12-20T05:39:49Z
Maybe using break instead of return would avoid the confusion.
Comment #12 by robert.schadek — 2024-12-13T18:20:30Z