Type checker: Detection of abstract classes fails when a constructor is declared is sub class responsible

[lausdahl]

Consider the following example:

class A
operations
public A : int ==> A
            A (-) == is subclass responsibility;
end A

class B is subclass of A
operations
public B : int ==> B
            B (-) == skip;
end B

and the class that tries to instantiate B:

class User
operations
public op : () ==> ()
op () == let - = new B(1) in skip;
end User

at new B an error is reported:

Cannot instantiate abstract class B. Unimplemented: A(int ==> A)  

This is not true in this case since we made an constructor in B that has the same signature as the one in A.

Another problem is then when you want to create B and A has only one constructor then B "should" call it otherwise I don't think the object can be created correctly, but that's a different issue.

It might be that having only one declared constructor as is subclass responsibility is meaning less and makes it impossible to ever instantiate the class.

[nickbattle]

​Well, the first thing​ to say is that none of this behaviour is particularly well defined anywhere!

I would quibble about whether B's constructor overrides A's (if that's what you meant). When a B is constructed, both B's and A's constructors must be called, so the rules for constructor overriding cannot be the same as for normal operations. As you say, I think that declaring a constructor as "abstract" is meaningless as it effectively disables the class and any derived classes. You cannot have abstract constructors in Java/C++ as far as I am aware, probably for the same reason.

So I think the improvement here would be to catch that case and declare abstract constructors as an error.

[nickbattle]

If you try this with VDMTools (I'm using 9.0.3 Linux), then the specification typechecks cleanly. You can then create instances of B, either as B() or B(1), but you cannot create instances of A by any means.

What I think is happening is that both A and B automatically have default constructors created (like X: () ==> X), and when the B constructor is called, then A's default constructor is called. Evidently VDMTools does not care whether A is abstract when this happens. VDMJ would also call A's default constructor when constructing B, but it includes a check that says that you cannot construct abstract classes, and so fails.

There is already a bug whereby, if B's constructor explicitly calls a non-default constructor in A, then A's default constructor is called first. Both VDMTools and VDMJ do this, but it only makes sense to call one constructor for an object! Presumably, as with Java/C++, the default constructor creation should be suppressed if explicit one(s) are defined with parameters, and then subclasses would also fail typecheck unless they provided constructors which called the explicit superclass constructor(s). But neither VDMTools nor VDMJ do this. I suspect there are a lot of specifications out there which take liberties during construction, which would break if this was "fixed".

As I keep saying, VDM++ is a mess.