Keyword 'is subclass responsibility' in functions are not working as specified in the manual

[cakemaster9001]

Hi

I have been making a model where I wanted a public method that returned the type of a derived class. The way I modelled it looked something like this:

class Base
functions
public getType: () -> ?
getType() == is subclass responsibility;
end Base

class Derived0 is subclass of Base
functions
public getType: () -> ?
getType() == <Derrived0>;
end Derived0

class Derived1 is subclass of Base
functions
public getType: () -> ?
getType() == <Derrived1>;
end Derived1

When I try to run the getType method on any of the derived classes, I get a "getType() = Cannot evaluate getType() : Error 4032: 'is subclass responsibility' expression reached in 'Base'" instead of the expected type.

I thought this would work, as I can see in the VDM10 language manual in chapter 5, page 42, that the 'is subclass responsibility' should be allowed in a function body context.

[nickbattle]

Does it work if the return type is not '?'. It may be confusing the hierarchy calculation. '?' is special/strange/non-standard.

[cakemaster9001]

It gives the same result for other return values, such as nat1. Here is the same code but with the simpler nat1 type:

class Base
functions
public getType: () -> nat1
getType() == is subclass responsibility;
end Base

class Derrived0 is subclass of Base
functions
public getType: () -> nat1
getType() == 1;
end Derrived0

class Derrived1 is subclass of Base
functions
public getType: () -> nat1
getType() == 2;
end Derrived1

[nickbattle]

How are you invoking the functions? My first thought was that functions are implicitly static and therefore they bind statically (ie. using the type of the declared object, rather than the actual type). But that doesn't seem to be the case either, even if I make them explicitly static:

> p let x : Base = new Derrived0() in x.getType()
= 1
Executed in 0.05 secs. 
> p let x : Base = new Derrived1() in x.getType()
= 2
Executed in 0.005 secs. 

There was a lot of discussion about the semantics here in the Language Board a long time ago. I'll try to dig that out to remind us all what this is supposed to do!

[nickbattle]

The Language Board discussion was held in 2009. How time flies :-) But anyway, it appears that we did decide to allow function invocation to bind dynamically (ie. to depend on the actual object type), although functions are implicitly static in a sense (since instance variables are inaccessible).

So... the example I gave above is behaving as expected. Can you show me how you are invoking the functions on the object to get the error?

[cakemaster9001]

I pressed either the launch or the debug button over a public method in VSCode as seen below:

[nickbattle]

Ah! Right, so this is actually an issue with the way the UI launches things, rather than a problem with the language server itself, by the look of it. I confirm I can reproduce this - clicking on the derived function launches produces the problem. I will find out what the code lens and UI uses in this case (since it's clearly wrong!). Thanks for clarifying.

[nickbattle]

The Launch | Debug lens was incorrectly deciding that the launch did not require a new object construction. It was confused by the static nature of the functions, thinking they did not need an instance. I've got a fix working in the development branch of VDMJ.

As a workaround, you can change the .vscode/launch.json entry to run p new Derrived0().getType() instead of p Derrived0.getType()

[nickbattle]

There were some subtle changes for this in VDMJ, but it does now seem to work correctly, so closing this.