CT for Pop3 does not work

[overturetool]

CT for Pop3 does not work

[joey-coleman]

Comment by nick_battle, 2010-12-19 12:16:02:

This is reproducible in VDMJ directly. I will look at it...

[joey-coleman]

Comment by nick_battle, 2010-12-19 13:19:41:

OK, this is an interesting problem. It happens because POP3Test (which contains the trace) is constructed by the CT test at the start. POP3Test creates an instance variable to contain the POP3Server. One of the constructor arguments makes a local function call to POP3Test`MakeMailDrop and that calls MakeMessages. When the function is called, the "self" value is not complete (we're still building instance variables). Therefore the function assumes it is static, as there is no self, and creates a ClassContext that can only see (explicit) static functions. Therefore it cannot see MakeMessages(UserName), as this is not explicitly static.

Therefore you get the same problem if you just ask for "new POP3Test()".

The version of POP3Test I use in VDMJ's internal tests (in test/resources/VDMBook/POP3.vpp) does not include local variables that try to create a POP3Server. Rather, the test1 and test2 operations create the server as a local variable when they start.

[joey-coleman]

Comment by pglvdm, 2010-12-19 14:25:56:

Ok I now changed the example so it works again. After the OO semantics LB improvements this problem should disappear.

[joey-coleman]

Comment by nick_battle, 2010-12-19 14:43:45:

It is also worth noting that the original problem here does not occur with VDM-10, where all functions are implicitly static and so they are visible during construction (even without a self value). Running the original specification under VDM-10 does allow the CT tests to execute (after a declaration is re-ordered to be defined before it is used).

Closing this bug, as the fix is provided in VDM-10, and is a known issue with VDM classic.