Closed mortenhaahr closed 1 year ago
So firstly, thank you for providing a very clear example of the issue. I can confirm the behaviour you are seeing, and I agree it is confusing at best, and should be changed.
What happens is that a subclass constructor always, and automatically calls the superclass default constructor. It then executes the body, which may call a different constructor explicitly. So your example works if you remove the precondition on the default constructor.
This strange behaviour is present in VDMTools and was copied over to VDMJ (and hence to the VSCode extension). This was designed before my time, but I suspect the reason is that constructor invocation is not special in VDM++ in the way that it is for other OO languages. So you always get "basic" construction, and then the body can go on to do more calls. Unfortunately (as far as I know) the full semantics of construction, and the consequences for calling the default constructor, were never made clear.
The issue was raised in the "OO Issues" document I shared with you before, and the document contains a proposal to change both the syntax and semantics of object creation to be more like C++.
To add a bit more detail, the default constructors for the entire graph of parent objects (since you can have a common parent by diamond inheritance) are called once only at the start of construction. Then the body of the child constructor is executed and this may invoke another parent constructor as an operation, but that does not do anything to the rest of the parent objects unless that constructor explicitly calls another in its parent, etc.
So construction comes in two parts. There is the base construction of the object graph using the default constructors (if defined), followed by an optional explicit initialization via call(s) to other constructors (which are really just like operations).
Very strange :-(
Hi Nick, Once again thank you for the incredibly quick replies.
After investigating the document that you refer to (VDM_OO_Issues_0.2.pdf) it appears that point 14 under section 2.2.1 page 9 might be able to solve this issue.
However, as you stated in the other issue, there doesn't seem to be much progress on these topics.
Yes, we definitely know about the issue, and section 2 tries to clear up the whole areas of initialization and construction (which end up being closely linked). The problem isn't that we can't think of ways to solve it, it's that there are a lot of specifications out there whose semantics could change (not that the authors necessarily know the current strange semantics!). Plus there is the non-trivial effort of updating the language tools, possibly having to support multiple versions.
So although we will discuss this issue at the next LB meeting, realistically this won't change quickly (if ever) and we will be stuck with the current semantics for a while. The OO Issues document was written to keep a record of the long list of problems, so that we can at least show people that we know about them and have some ideas of how to move forward.
That said, if there are incremental changes that we can make that would improve the situation, that may be possible to change. But even apparently simple language changes can have subtle consequences, and will take us a while to work through.
I hope to discuss this at the Language Board meeting on 27th Nov.
I ran the presented spec on VDMTools and got the error as below.
vpp> p new UseClass().test_bad()
Note: specification has changed since last 'init'
Initializing specification ... done
t.vdmpp, l. 8, c. 5:
Run-Time Error 58: The pre-condition evaluated to false
@tomooda , are you able to confirm that VDMTools behaves as in: https://github.com/overturetool/language/issues/57#issuecomment-1320249495
Yes, it looks behaving as you described.
OK, thanks @tomooda. So at the very least, we should update the current version of the LRM to be clear about the semantics. I can give you a few paragraphs and an example, if that helps.
@mortenhaahr We discussed this issue at the Language Board meeting today. It has prompted the LB to review the current state of the OO problems in VDM++, and we hope to make time to discuss it face to face at the next workshop in Luebeck. But as I said before, fixing this will change the semantics for a large number of existing specifications and there are many more OO issues than just construction. It will also take considerably effort to update the current tools. So this will take a while...!
That is nice to hear. Thanks for the effort. :slightly_smiling_face:
@tomooda, I've just pushed a change on the "editing" branch for the 11.1 section on object construction. Can you have a look?
Looks good to me, but the word "unusual" may sound a little self-accusing in a language reference. How about
Please note that in object construction the default initialization
of object fields is ...
LOL, yes fair enough. It's my frustration showing through!
The LRM has been updated. Closed by LB.
Identification of the Originator
Name: Morten Haahr Kristensen Email: mortenhaahrkristensen@gmail.com Role: Master student at Aarhus University
Target of the request, defining the affected components of the language definition
Allow users to specify which constructor of the base class gets called.
Motivation for the request
I found the current behavior to be limiting. E.g. in cases where you don't want to allow default construction of base- or superclass objects.
See example 1.
In other languages this is possible. I have attached a simple C++ example where the concept of constructor delegation gets used. Please see example 2 or https://godbolt.org/z/f3oYqdT3o for an interactive version.
Description of the request
When instantiating an instance of a superclass with a parameterized constructor (a constructor taking arguments), it calls the default constructor of the base class. In itself, this is OK, as it is similar to many other languages, but it is limiting when there is no way of specifying which constructor is used.
Description of the modification
My suggestion: Add delegating constructors to VDM++. We need some way of specifying which base class constructor is used.
benefits from the modification
It allows disallowing default constructors of being used.
possible side effects
Implementation dependant.
Example 1 - Motivation for change:
Example 2 - C++ behavior