Expressions in let def and let be st statements should not allow operation calls

[nickbattle]

The RHS of the variable assignments in "let def" and "let be st" statements should be functional expressions, involving only expressions, functions or pure operation calls. Currently Overture allows impure operation calls here.

operations
	op: nat ==> nat
	op(a) == return 123 + a;

	t1: nat ==> nat
	t1(a) ==
		let x = op(a) in return x + 1;

	t2: nat ==> nat
	t2(a) ==
		let x in set { op(a), op(a+1) } in return x + 1;

	t3: nat ==> nat
	t3(a) ==
		def x = op(a) in return x + 1;

This should produce a warning for both "let" statements, since they call an impure operation. The def statement in t3 is fine, because this is explicitly intended for operation semantics. A warning, rather than an error, was suggested by PGL and makes Overture the same as VDMTools.

[nlmave]

Hi Nick, Well, in this case it should be allright in fact as 'op' has no side effect as it does not depend on the local state of the object - it basically behaves as a pure function. So it is in fact "possible well-formed" for a let-expression. I suggest to improve the example used - one that explicitly uses a side effect when calling op IMHO this is more of a proof-obligation style of need, rather than a warning or an error. Suggest perhaps to issue a warning if and only if definite well-formedness is selected in the type checker (if that distinction still exists) An error should IMHO only be issued if and only if an operation is called in a let-expression for which a side effect can be obviously (and statically) determined - without the need to go through proof obligation. My two cents worth. Regards, Marcel

…

On 07-09-2020 12:41, Nick Battle wrote: The RHS of the variable assignments in "let def" and "let be st" statements should be functional expressions, involving only expressions, functions or pure operation calls. Currently Overture allows impure operation calls here. |operations op: nat ==> nat op(a) == return 123 + a; t1: nat ==> nat t1(a) == let x = op(a) in return x + 1; t2: nat ==> nat t2(a) == let x in set { op(a), op(a+1) } in return x + 1; t3: nat ==> nat t3(a) == def x = op(a) in return x + 1; | This should produce a warning for both "let" statements, since they call an impure operation. The def statement in t3 is fine, because this is explicitly intended for operation semantics. A warning, rather than an error, was suggested by PGL and makes Overture the same as VDMTools. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#736>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABPAHA5WOBLJKIJTIFKE3MLSES2GRANCNFSM4Q56DWTQ>.

[nickbattle]

The example is definitely a poor one. As you say, this is harmless in fact. But as it stands, we assume an operation is impure (ie. has side effects) unless it is explicitly tagged as "pure", so the example would be treated as suspect.

Producing proof obligations for operations, or parts of them, is difficult because we don't have the well defined context that we have in a function - in general, we're not sure what happened before a statement is executed. We could still make this a PO matter rather than a warning, but the tools won't be able to generate a useful PO.

VDMJ/Overture doesn't have the "def/pos" setting that VDMTools has. It always uses possible semantics. It might be possible to produce a sub-analysis that determines whether operations are definitely impure, and use that.

Having just hacked in the simplest tweak to change this (making the RHS of the assignments "functional"), lots and lots of the test specifications fail, since they do all sorts of things in let statements that we regard as impure, like creating "new" objects or using "time". A lot of them could be changed to use "def statements", which are intended for this, but probably not all of them. So this would have quite a large legacy impact.

Hmm...

[nickbattle]

One helpful suggestion, via Leo, is that we hide this behind the -strict flag. That is used to enable several nit-picking checks that are strictly required, but which VDMJ historically tolerated. This isn't quite in the same category, though the effect is perhaps the same - users can then use legacy specifications with the tools, but enable strict usage for new work and be made aware of the need to use "def statements" in these circumstances.

[nickbattle]

I've just pushed a change to ncb/development, within the -strict flag, to implement this "pure" check for let statements. Without the -strict flag, everything is as it is currently, and all the usual tests pass. This gives us some space to think about what we want to do, but provides the strict functionality for folk that want it.

@idhugoid The IDE currently won't allow us to set the -strict flag, though it's fine from the command line. Would it be possible to add that - it's really a type check option on a per-project basis, so perhaps that's in the VDM Settings dialog for a project?

[idhugoid]

Sure. I will give it a go.

[nickbattle]

I'll leave this issue as open for now, though it would do no harm to include it in the 3.0.2.

[idhugoid]

Hi @nickbattle. This should be ready for tests after build https://build.overture.au.dk/jenkins/job/overture-development/273/ finishes. :)

[idhugoid]

Removing myself from the assignment. @nickbattle, please tell me if I should close this myself, or if you take control over it.

[nickbattle]

I'll give it a test when I get a minute - this is on the development branch, presumably?

[idhugoid]

Yes, here: https://overture.au.dk/overture/development/Build-273_2020-09-08_15-59/

It also includes a merge of the contents of your branch.

[idhugoid]

I will look at how the strict introduction affects type-check (according to #737) and come back to you @nickbattle when it is ready for testing.

[nickbattle]

@idhugoid I've just built db2d546. It's showing a flag called "Strict let def checks" in the Runtime tab of a launcher. But we need that flag in the Project Properties/VDM Settings/Type Checking section (below Suppress Warnings). That's so that it can affect the type checking in the editor, like warning suppression. The problem with the launcher(s) is that you might have more than one for a project, and besides launch-time is a bit late to find out about type checking problems(!).

[nickbattle]

@idhugoid OK, this is better. The flag now is in the correct place in the project properties. It's labelled "Strict let def checks", whereas I was expecting something more general to describe the -strict flag, such as "Strict type checking". But for some reason, when I enable this flag, it only produces the "let def" warnings, not all of the other warnings that I would expect with -strict. How is that possible??

So for example, I get the following with -strict:

module A
definitions
types
	T = nat
	ord a < b == a < b
	inv t == t < 10;

operations
	op: nat ==> nat
	op(a) == return 123 + a;

	t1: nat ==> nat
	t1(a) ==
		let x = op(a) in return x + 1;
end A

Warning 5026: Strict: Order should be inv, eq, ord in 'A' (test.vdm) at line 6:5
Warning 5025: Strict: expecting 'exports all' clause in 'test.vdm' at line 2:1
Parsed 1 module in 0.001 secs. No syntax errors and 2 warnings
Warning 3300: Impure operation 'op' cannot be called from here in 'A' (test.vdm) at line 14:17
Warning 5000: Definition 't1' not used in 'A' (test.vdm) at line 12:5

Those early strict warning come from the parser rather than the type checker, which may be a clue? But they do not appear if I force a re-parse by editing the spec. Maybe the answer is that the parse, as you're typing, also needs this flag to be passed (as well as the type checker)?

PS. I will push a change to make the warning number for impure operations in the 5000 range, to be consistent.

[nickbattle]

I've just pushed a change to ncb/development that produces the following warning numbers/text with -strict:

Warning 5026: Strict: Order should be inv, eq, ord in 'A' (test.vdm) at line 6:5
Warning 5025: Strict: expecting 'exports all' clause in 'test.vdm' at line 2:1
Parsed 1 module in 0.187 secs. No syntax errors and 2 warnings
Warning 5031: Strict: impure operation 'op' cannot be called from here in 'A' (test.vdm) at line 14:17
Warning 5000: Definition 't1' not used in 'A' (test.vdm) at line 12:5

[idhugoid]

@nickbattle, I think it is great that we are now threading in the right path. I will be busy with other tasks until next week. So, I will come back to this later and assign the issue to you, when it is ready to test... BTW Do you get notified in case I do not mention your name explicitly? The @ user id mention GitHub style looks horrible to me... Is there a better way?

[nickbattle]

I do usually see the alert emails for bugs that I follow, like this. So it should be OK.

[nickbattle]

Just pushed another commit to add similar new warnings for threadid, time and "new" expressions in functional contexts.

[idhugoid]

Ok. I think the remaining problems were fixed:

• Improved message db9f31e
• Missing strict warnings due to longstanding bug 90e0da5
• Missing strict setting passing to parse/tc in the call made while user types e6f41cf

This should be ready for testing soon at https://overture.au.dk/overture/development/latest/

BTW. I was thinking about getting into the Overture testing framework to add the file you sent as a test case for the strict option. Do we have anything on this? Can you help me do my first steps with the testing framework Nick?

[nickbattle]

The testing framework is a royal pain in the ar...m. This may help: https://github.com/overturetool/overture/wiki/Test-Framework.

I find is very confusing and whenever I have to tweak tests because of bugfixes, my heart sinks :-(