Difficult VDMUnit test scenario

[Gronne]

Description

An error will come when making non-returning function calls in between dcl declaration for VDMUnit tests. The error will come at the dcl that comes after the function call. Ex.:

protected TestRouteRouteCopyConstructor : () ==> () TestRouteRouteCopyConstructor() == ( dcl rOA : Route := new Route(); rOA.addToRoute(new Road(100, 10)); dcl rOB : Route := new Route(rOA); assertTrue(rOA.equalTo(rOB)); );

This can be solved by making the function calls in another operation and returning the object (it will return rOA in the above case). This is shown in the example below:

protected TestRouteRouteCopyConstructor : () ==> () TestRouteRouteCopyConstructor() == ( dcl rOA : Route := createRoute([new Road(100, 1), new Road(200, 2), new Road(200, 2)]); dcl rOB : Route := new Route(rOA); assertTrue(rOA.equalTo(rOB)); );

private createRoute : seq of Road ==> Route createRoute(roads) == ( dcl route : Route := new Route(); for road in roads do route.addToRoute(road); return route; );

It is not the non-returning function call that creates the problem as the next example shows:

protected TestRouteAddToRoute : () ==> () TestRouteAddToRoute() == ( dcl rO : Route := new Route(); dcl road : Road := new Road(100, 1); rO.addToRoute(road); assertTrue(rO.getNrOfElements() = 1); );

This makes it more difficult to create tests because more abstraction is required. I do not expect this to be an error but would like to give attention to it as a recommendation to improve the language's utility further.

Steps to Reproduce

1. See above

Expected behavior: be able to use non-returning function calls in between dcl declarations

Actual behavior: It gives an error

Reproduces how often: Not sure

Versions

Windows 10 - Overture Tool 3.0.2

[Gronne]

The same happens when I make a dcl after an assertTrue()

[Gronne]

I can of course just define everything in the beginning without initializing it...

[nickbattle]

Thanks for reporting this. The first thing that struck me looking at the example is that you have "dcl" statements that are not all at the start of the block. The parser should only allow dcls at the start, and as far as I can see both VDMJ and Overture do this, for example:

operations
	op: () ==> nat
	op() ==
	(
		dcl x:nat := 1;
		x := 123;
		dcl y:nat := 2;   <--- ERROR here on the 2nd dcl, because of the statement above.
		return x + y
	)

Error 2063: Unexpected token in statement in 'DEFAULT' (test.vdm) at line 7:9
Parsed 1 module in 0.271 secs. Found 1 syntax error

Is this your issue? There is a syntax error, because a Block Statement is a (possibly empty) set of "dcls" followed by a sequence of non-dcl Statements. If you want a 2nd dcl further down, you need an inner block to introduce it.