Abstract method can be declared private

[peterwvj]

It's allowed to declare private operations and functions abstract as shown for the class below. But it seems strange that you require subclasses to overwrite something they can't see. The only advantage I see is that it allows you to declare your class abstract (in a strange way though), but if you want to guard against instances being created you can just declare the constructor private.

I think the typechecker should report an error here and that abstract functions and operations should only allow protected/public access.

class S

operations

private op : () ==> ()
op () == is subclass responsibility;

end S

[nickbattle]

Yes, I agree this definitely looks wrong and ought to be an error. VDMTools agrees:

Error[438] : Abstract function/operation "op" must be defined as public or protected

It should be an easy fix.

[nickbattle]

I've fixed this in VDMJ now. I'll move the fix over to Overture in the next day or two. I think this is a reasonable change as both VDMTools and VDMJ do implement method overriding in such a way that these constructs are pointless, but I thought I should add a note here to point out that we don't necessarily have to do things this way. To quote from the "OO Issues" document, where the proposed functionality of method overriding is being described:

"An overriding member may not reduce the visibility (public/protected/private) of the member it overrides[2].

[2] This isn't the case in C++. The access specifier determines what can be called from where, but a virtual private method can be overridden by a public version in a subclass, resulting in different behaviour. In Java, a subclass can hide a private superclass method with a public version, but this doesn't override the superclass method."

So we are saying that VDM++ is like Java, not like C++. That's fine, but we must be aware of the choice rather than stumble into it by accident.

[ldcouto]

Just poking in to say that, as of this fix, 6 of the Overture examples no longer type check.

They are: CyberRail(RT), CM(RT), PacemakerConc, MSAWconcur, HomeAutomationConc, CMConc (PP)

These models all have the issue fixed here. This is fine, of course. But we only caught this due to some test failures in the POG.

I feel like we could improve the current example setup. They need to be somewhere where all the modules can access them for testing purposes. And we should have a set of tests that ensures that all examples go through the various plug-ins.

At the workshop, there was some talk of having a few featured examples. We should do it for these ones at least.

[pglvdm]

I can go in and fix these examples.

[ldcouto]

I fixed the examples. I'm more worried about the structural issue. The examples are in 3 places:

• overture import
• parser tests
• pog tests
• possibly others...

There are also no tests to specifically ensure that they run on all the plug-ins.

[nickbattle]

Gah!!! Yes, of course, the examples. Sorry. I always forget to try those. I just run the CSK suite and the internal JUnit tests before I check-in and push (though there seemed to be POG test trouble before I changed anything, so I didn't worry about that).

Can we not get all the tests we have integrated into the Maven process somehow? It's very tedious having to run different tests in different places in different ways, and remember to do it.

[ldcouto]

Yes Nick. I've just begun work on a tests module that will test the examples on all the major plug-ins.

When it's done, it will run as part of a normal maven build.

On the subject of this NIck, how do you submit a multi-file model to the parser? Most of the examples are spread. I can flatten them before submitting but the literate VDM ones are a bit annoying.

On Tue, Jun 24, 2014 at 3:47 PM, Nick Battle notifications@github.com wrote:

Gah!!! Yes, of course, the examples. Sorry. I always forget to try those. I just run the CSK suite and the internal JUnit tests before I check-in and push (though there seemed to be POG test trouble before I changed anything, so I didn't worry about that).

Can we not get all the tests we have integrated into the Maven process somehow? It's very tedious having to run different tests in different places in different ways, and remember to do it.

— Reply to this email directly or view it on GitHub https://github.com/overturetool/overture/issues/326#issuecomment-46980533 .

[ldcouto]

Update: I have completed the new tests module.

As part of this module, there is an AllExamplesTest that tries to parse + TC all examples (that do not have purposeful errors). At the moment, this produces 6 test failures as expected.

The module also has a functionality for providing the typed asts of all examples (for use with other plug-in tests) but that's blocked on the aforementioned 6 example failures.

In addition, the module has, IMO, simpler mechanisms for running tests, storing results, comparing stuff, etc.

You can check it out by merging with ldc/tests (it's in core/tests). I'll talk to @joey-coleman about migrating over to the new system soon.

[joey-coleman]

For stuff related to the test module as such, see #333 — otherwise this will close on my next merge cycle