return statement ignored in nested if

[cakemaster9001]

During development, I needed to call a specific method and then return from my method if multiple different conditions were true. Otherwise, I would call another method. I decided to do this through a nested if statement with no else clauses. This led to errors as the other method was called no matter what. Here is an example of how to reproduce the issue:

class TestNestedIfReturn
operations
public testNestedIf: seq of nat1 ==> ()
testNestedIf(numSeq) == (
    if len numSeq = 1 then (
        if hd numSeq = 42 then (
            return IO`print(hd numSeq);
    ));
    IO`print(nil);
);
end TestNestedIfReturn

If this method is called with the sequence [42] it will print 42nil instead of the expected 42. For all other values, this will print nil as expected. A fix for it is to split the nested return into two lines like this:

class TestNestedIfReturn
operations
public testNestedIfWithReturnOnOtherLine: seq of nat1 ==> ()
testNestedIfWithReturnOnOtherLine(numSeq) == (
    if len numSeq = 1 then (
        if hd numSeq = 42 then (
            IO`print(hd numSeq);
            return;
    ));
    IO`print(nil);
);
end TestNestedIfReturn

This other implementation will behave as expected. To me, the semantics of the two statements are the same, but I might be missing something in the manual somewhere.

[nickbattle]

But IO'print doesn't return a value. So this is really something the type checker should prevent. It "works" because the operation returns "()" too. But really you should do as you have in the working example - i.e. having two calls.

I'll look at the type checker. VDMTools picks this up - "Error[259] : Apply-Expr must return a value" for the return.

[nickbattle]

OK, I've made some changes. It's throwing up a lot of new errors from the CSK test suite, though most of them seem legitimate. But I should really do more checking on this. But your spec now says:

Parsed 2 classes in 0.124 secs. No syntax errors
Error 3365: Statement should be 'return' for void operation in 'TestNestedIfReturn' (test.vpp) at line 7:13
Type checked 2 classes in 0.277 secs. Found 1 type error
Bye

[nickbattle]

OK, I think this is working as intended. There are a surprisingly large number of cases of this "fault" in the old CSK test suite (a collection of 3200+ tests), but their tests frequently have many many type checking errors (deliberately) and this one got lost in the pile. So I've pushed the change to the development branch, having changed the message wording slightly:

Parsed 2 classes in 0.129 secs. No syntax errors
Error 3365: Void operation cannot use 'return <exp>' in 'TestNestedIfReturn' (test.vpp) at line 7:13
Type checked 2 classes in 0.247 secs. Found 1 type error
Bye