Expression and Statement Clarifications

alzibab commented 4 years ago

Some areas of Expressions and statements that may require some clarification for VDM-SL.

A VDM-SL file is attached showing examples.

Define Expressions

The Language manual states define expressions can only be used in operations however Overture allows define expressions to be used in function definitions.
Overture allows Define Expressions called in operations can call operations that modify state. The language manual states: "The define statement corresponds to a define expression except that it is also allowed to use operation calls on the right-hand sides. Thus, operations that change the state can also be used here." This would suggest that a define expression cannot call operations?

Let Expressions

Let expressions called within operations can call operations both pure and impure, is this the expected behaviour?

Let Statements

The Language manual states that define statements allow for operation calls, however overture allows let statements to also call operations . How do let and define statements differ?

Apply Expression

Language manual states: "In the VDM languages an operation can also be called here. This is not allowed in standard VDM-SL". Does this mean operation calls are or are not allowed in VDM-SL? Currently you can call operations in apply expressions in VDM-SL.

Return Statement Page 127 Example

if test then opCall() else return FunCall()

The Language manual states that the branches of the If statement must be statements and therefore FunCall must be in a return statement. Overture allows this example without the return and just an apply expression.

ExpStmtClarification.vdmsl.zip

tomooda commented 3 years ago

@alzibab Thank you for posting this RC, and my apologies for the late response. The Language Board has accepted this RC. We are looking into this.

tomooda commented 3 years ago

I asked the developers of VDMTools. Like Overture, VDMTools also allow read access to state variables and operation calls in all of define expressions, define statements, let expressions and let statements. A developer of VDMTools says that the main difference between define and let is the sequential evaluation of bindings. The define evaluates bindings in the order separated by ; whereas the semantics of let keeps a room for re-ordering although VDMTools does not re-order for now.

nickbattle commented 3 years ago

I've compared the behaviour of VDMJ and VDMTools (we can assume Overture is the same as VDMJ), using the attached test spec. The results are recorded in the spreadsheet also attached, which I hope we can use to decide what we want (since the tools differ!).

https://docs.google.com/spreadsheets/d/1slikOuxMJyNYmh7flTOexbZnkVNY2vvOCORtClS2uaM/edit?usp=drive_web issue49.vdm.txt

nickbattle commented 3 years ago

(from Tomo-san email)

VDMTools differentiate let and def by accessibility to the state/operations while VDMJ basically treats them samely except operation calls in let/define statements. It looks the LRM is closer to VDMTools' semantics than VDMJ's. I think it's rather from the classic VDM. In my personal opinion, I think VDMJ's semantics is more conformant to the rest parts of VDM10.

One interesting point of VDMJ's semantics is that it allows any (including a non-pure one) operation call in let expression in an operational context but it prohibits a non-pure operation call in let statement in an operational context. It looks a little odd to me that let expression is more permissive to the stateful access than let statement. Nick, do you know why it is defined in that way?

nickbattle commented 3 years ago

@tomooda The rules were so unclear in the LRM/manuals when VDMJ was written that any difference is almost certainly confusion and/or bugs, rather than a definite decision. So I'd be very happy to clear it up and make the interpretation the same.

nickbattle commented 2 years ago

I've updated the table to add extra columns with the behaviour (in VDMJ/Overture) for operation calls and state variable access from the <body> of let/def expressions and statements.

If we make cell D8 "Y" (meaning you're allowed to call operations from the <expression> in a let statement's bind), then the table seems consistent and symmetrical. The principle would then be, "You can do anything from an operational context, but from a functional context you can't access state and can only use pure operations".

I haven't checked what VDMTools allows.

Updated table

nickbattle commented 2 years ago

I've now filled in the VDMTools tab. It looks like it allows anything except state variable access from a functional context.

tomooda commented 2 years ago

Thank you for the table, @nickbattle. It surely gives a good overview. The new semantics tab in the table says def expression/statement is almost equivalent to let expression/statement except for static typing and concrete syntax. The remaining differentiator between let and def is re-ordering, and that's what the current VDMTools' semantics is a little stricter about (8D) than the new semantics. We need to decide whether or not interpreters reserve the freedom to re-order let bindings. My proposal is "interpreters may re-order evaluations of right-hand sides of let statements only when the side effects of non-pure operation calls do not influence the evaluations of right-hand sides. Interpreters must evaluate the local definitions of def expression/statement in order."

nickbattle commented 2 years ago

Did you mean re-order evaluation of left-hand sides? Meaning the order of the bindings? If so, then I like the proposal, though I think it would be clearer to talk about re-ordering bindings.

tomooda commented 2 years ago

Thank you for the clarification. Yes, I meant the order of bindings.

nickbattle commented 2 years ago

This is now available in the "development" branch of VDMJ (4.5.0-SNAPSHOT). The only change is regarding operation calls within the definitions of a let clause in an operation - I've updated the spreadsheet to show the changed cell in green. Before the change, the test spec attached above used to give the following warning:

Warning 5033: Impure operation 'impOp' cannot be called from here in 'ExprStmtClarification' (test.vdm) at line 71:16

With the correction in place, there are no errors or warnings in the specification.

tomooda commented 1 year ago

I made a draft of the modification in the RC49 branch. https://github.com/overturetool/documentation/commit/f1df37b1e39dcf2542f70b4c41ff0e10d1fe72ca Please check https://github.com/overturetool/documentation/blob/RC49/documentation/VDM10LangMan/VDM10_lang_man.pdf . The changes are Section 6.1, 6.2, and 12.2. If this looks OK, I'll merge it to the editing branch.

nickbattle commented 1 year ago

That looks good, Tomo. Would it help to add something explicitly to 6.1 (lets) to say that the en expression can only involve state or impure operations calls when the let is in the context of an operation?

tomooda commented 1 year ago

Yes, that would be a reasonable supplementary comment. I'll work on that.

tomooda commented 1 year ago

I added a couple of sentences in Section 6.1 to explain that a right hand side of a def expression may contain stateful expressions, such as operation calls and state variables. (https://github.com/overturetool/documentation/commit/d2993e66dc1968de345668a598389020d8734f8f)

nickbattle commented 1 year ago

OK, let's go with that :)

tomooda commented 1 year ago

updated the LRM with version info. Can we close this issue?

nickbattle commented 1 year ago

Have we addressed the last two points in the original request? We've just been focussing on the let/def subtleties only (which I think are now clarified by the spreadsheet, and hopefully the LRM).

It's true that the tools do allow operation calls in assignments, and function applies as "direct" return values.

tomooda commented 1 year ago

Nick, I think VDMJ raises a type error to function application as a statement except the case that the function returns ().

nickbattle commented 1 year ago

Seem to work here? Do you have an example?

functions
    f: nat -> nat
    f(a) == a + 1;

operations
    op: () ==> nat
    op() == f(123);

Parsed 1 module in 0.085 secs. No syntax errors
Type checked 1 module in 0.281 secs. No type errors
Initialized 1 module in 0.179 secs. 
Interpreter started
> p op()
= 124
Executed in 0.011 secs.

tomooda commented 1 year ago

functions
    f: nat->nat
    f(a) == a + 1;
operations
    op1: () ==> ()
    op1() == skip;
    op2: () ==> ()
    op2() == if 1 = 2 then op1() else f(1);

raises

Error 3312: Void operation returns non-void value in 'DEFAULT' (t.vdmsl) at line 7:5
Actual: (() | nat)
Expected: ()

But this type error also looks incorrect because the body of op2 does not have a return statement and therefore returns () implicitly. An easy way to fix it is to add a type check rule on the operation call that the callee's type should be an operation type (==>).

I also think an operation/function call as a statement should be typed (), and the operation/function call as an expression should be typed as its return type. The return statement return exp should be typed as the exp's type. But this change might break existing specs (which are, in my opinion, not actually well-formed).

nickbattle commented 1 year ago

Ah OK, now I understand what you mean. But we did do it this way deliberately, and after some considerable discussion (at least with PGL and MV, as I recall, a decade or more ago). We thought that all paths through an operation must return the right type, so you would get the same behaviour here even if "f" was an operation. Is VDMTools different? (No time to try, sorry!)

tomooda commented 1 year ago

Interesting! I tried on VDMTools and it behaves just the same as vdmj. So, the interpreter has been expected to handle a function call as an operation call since the age of VDM toolbox!? Hmm... I think we need to discuss which semantics we choose, the de-facto interpreters of ages, or the LRM. 😮

nickbattle commented 1 year ago

I'm glad they're the same! But I do remember discussing this at length with people at the time and changing VDMJ as a result. So this is by design. Perhaps the LRM should be updated, if it is unclear?

tomooda commented 1 year ago

Okay, I now understand that it is designed in that way although I still don't get why. Anyway, it's the working semantics and we need to update the LRM to explain the same semantics. As far as I understand, the LRM needs to be updated in the following two points.

The call statement calls a function or an operation which may or may not returns a value.
The call statement returns from the calling context if and only if the callee returns a value.

Are these what you changed VDMJ to?

nickbattle commented 1 year ago

Yes, that's right: in a block, VDMJ treats operation and function "call statements" the same way - except we know a function will always return a value.

tomooda commented 1 year ago

Okay, I think the implicit return statement on a call statement with a return value and the function call as a statement can be considered an implementation extension to the language definition. I mean, they are not a part of the language semantics, but the interpreters may do those extensions for convenience. How about modifying the description that @alzibab pointed out into the following?

Examples: In the following example OpCall() is an operation call whereas FunCall() is a function call. As the if statement only accepts statements in the two branches, FunCall is “converted” to a statement by using the return statement, i.e. return FunCall(). This "conversion" may be carried out explicitly by the specifier, or implicitly by the interpreter.

tomooda commented 1 year ago

solved by 1f13bec5877aba78890c4a110426215cd6b31c93

overturetool / language

Expression and Statement Clarifications #49