An example in Language manual, a strange type error occurred.

[shinsahara]

Description

There is a strange type error in the merge sort example.
in the Language manual(Feb 2018, version 11, version of Overture .exe 2.6.0) p.57-58.

The example is following:

class MergeSort

operations
public mergesort : seq of nat ==> seq of nat 
mergesort(s) ==
	cases s:
		[] -> return [], 
		[x] -> return [x],
		s1 ^ s2 -> return lmerge(mergesort(s1), mergesort(s2))
	end;
	
functions
public lmerge : seq of nat * seq of nat -> seq of nat 
lmerge (s1,s2) ==
	if s1 = [] then s2 
	elseif s2 = [] then s1 
	elseif (hd s1) < (hd s2) then 
		[hd s1] ^ (lmerge (tl s1, s2)) 
	else 
		[hd s2] ^ (lmerge (s1, tl s2));

end MergeSort

MergeSort.vdmpp.zip

Steps to Reproduce

1. read the MergeSort.vdmpp in a project.

Expected behavior:
There is no error.

Actual behavior:
Following type error occurred at line 4:
"Operation returns void value. Actual: (() | [] | seq of (nat)) Expected: seq of (nat) "

Reproduces how often:
every time.

Versions

Which version of Overture are you using?

Version: 2.6.2
Build date: 2018 May 18 11:17 CEST
Git commit description: Release/2.6.2

Also, please include the OS and what version of the OS you're running.

macOS High Sierra version 10.13.8

Additional Information

On VDMTools, there is no error, and can get the result as following:

>> version
The VDM++ Toolbox v9.0.7 - Sat 09-Jun-2018 09:00:27 +0900
VDM Toolbox is currently developed with the cooperation of Research Center
for Architecture-Oriented Formal Methods of Kyusyu University.
>> d new MergeSort().mergesort([3,1,5,2])
[ 1, 2, 3, 5 ]

[nickbattle]

It looks like this is because the cases statement in the operation does not have an 'others' clause? Though I agree that the existing cases do cover all possibilities. Can you try adding an others clause to see whether it changes the error - I'm away again at the moment, so can't try it.

[shinsahara]

I think that "others statement" is optional in VDM10_lang_man and VDMTools's langmanpp_a4E.
So, adding an others clause is not the answer of this problem.

cases statement = ‘cases’, expression, ‘:’,
                  cases statement alternatives, 
                  [ ‘,’, others statement ], ‘end’ ;

[nickbattle]

Yes, others is optional. I'm trying to remotely investigate the issue, not propose a solution. Does VDMTools analyse cases patterns to determine when a cases statement can possibly drop through? I think that VDMJ is incorrectly assuming that this can happen in your example, even though the patterns cover all possibilities. A few experiments with various patterns and an 'other' clause would help.

[shinsahara]

In following example,
if n was not in set {1,2} then VDMTools fall in Run-Time Error 119.
But, if "def type check" was "on" then VDMTools said "Type error [19]."

public casetest : nat ==> nat
casetest(n) == (
	cases n:
		(1)	-> return 1,
		(2) -> return 2
	end
);

In following example,
VDMTools said "there is no type error."

public mergesort : seq of nat ==> seq of nat 
mergesort(s) ==
	cases s:
		[] -> return [], 
		[x] -> return [x],
		s1 ^ s2 -> return lmerge(mergesort(s1), mergesort(s2)) 
	end;

[nickbattle]

OK, thanks Shin. It looks like VDMTools doesn't regard *possible* errors as actual type errors here - def-checking picks it up instead. VDMJ tries to report these as errors, but fails to see that s1^s2 is guaranteed to match, and hence should not raise an error here. We have had several "bugs" before about whether *possible* void paths in an operation are errors or not. Currently they are treated as errors by VDMJ; it seems they are only errors in VDMTools with def semantics. I should be able to tighten the check regarding patterns that match any value.

[nickbattle]

I've now changed VDMJ to determine whether any of the patterns in a cases statement will definitely match a value of the type passed to the statement. If (at least) one of the cases always matches, it has the same effect as an "others" clause - that is, suppressing the drop-through behaviour that could return a void value. So for example:

	cases s:
		[] -> return [], 
		[x] -> return [x]
		-- s1 ^ s2 -> return s2 ^ s1
	end;

This raises an error because the statement can return no value (assuming the operation is ==> seq of nat). If you comment-in the extra case, which is guaranteed to match any sequence (even [] matches a^b, though that is caught earlier anyway), then there is no type error because there is no void path.

It will take me a little longer to move the changes over to Overture...

[nickbattle]

Fix now available in ncb/development.

[nickbattle]

Just pushed a correction - Overture/VDMJ wasn't matching [] and {} with the concatenation and union patterns. Now it does (as VDMTools does). This is important here, otherwise (say) "a ^ b" wouldn't match any value of a sequence type, only non-empty sequences.