overturetool / vdm-vscode

Visual Studio Code extension for VDM language support
GNU General Public License v3.0
21 stars 6 forks source link

Inconsistency: Else being optional #202

Closed mortenhaahr closed 1 year ago

mortenhaahr commented 1 year ago

I found a small inconsistency in the interpreter. When writing an operation it is optional to specify else in an if expression. When writing a function it is mandatory. According to the language manual sec 6.4, it should be mandatory.

Maybe this is a language issue since one might ask the question of why it is mandatory to write the else part. I have an example of code that would be prettier without writing multiple else parts. :smile:

class A

operations
public f1: () ==> bool
f1() == (
    if true then
        return true;
    -- endif
    return false
);

public f2: () ==> bool
f2() == (
    if true then
        return true
    else
        return false
);

functions
-- Error: "Expecting else in if expression"
-- public f3: () -> bool
-- f3() == (
--     if true then
--         true;
--     -- endif
--     false
-- );

public f4: () -> bool
f4() == (
    if true then
        true
    else
        false
);

end A
nickbattle commented 1 year ago

This is deliberate, though perhaps (are you saying?) the LRM could be clearer about why?

The important difference between operations and functions is that the former describe a "process" whereas the latter generate a "value". So the process of an operation may well "do X" if something is true, and then carry on; whereas for a function there is no concept of carrying on, rather the expression is forced to yield a value both when the test is true and when it is false. So if-expressions have a mandatory else clause, and if-statements have an optional else clause.

If you have a function where a test is made and there is no meaning for when the test fails, then (from a specification point of view) you are perhaps missing a precondition ("this must be true" - but then why test it?) or perhaps you are writing a partial function that is undefined for some of its arguments (which again, is best expressed with a precondition, though you could say "else undefined").

But unless I've misunderstood your point, this isn't a bug.

mortenhaahr commented 1 year ago

Hi @nickbattle. Thank you for the quick response. You are absolutely right - this was a mistake on my side, I got expressions and statements mixed up. It correctly states in the LRM that "else" is optional in statements and mandatory in expressions.