Type checker: duplicate function and operation definitions in SL should be treated as errors

[peterwvj]

VDM-SL does not allow overloading so two operations with the same name are considered duplicate definitions. Given the spec below, Overture currently reports two warnings - once for each operation - saying that op is a duplicate definition. The model type checks in Overture without errors. For the same spec VDMTools correctly identifies the duplicate definitions but instead of reporting a warning, it reports an error - see blow:

Error List: 1 Error, 0 Warnings
...\Dup.vdmsl, l. 8, c. 13:
  Operation already defined

operations

op: nat ==> ()
op (-) == skip;

op: char ==> ()
op (-) == skip;

I believe that the VDMTools behaviour makes more sense.

I should mention that if you do a similar thing for values (using VDMTools) you only get a warning:

...\Dup.vdmsl, l. 5, c. 1:
  Warning[100] : "x" is multiple defined, and must have the same value

values

x = 1;
x = 2;

However, if you do this for type definitions then you get an error

...\Dup.vdmsl, l. 5, c. 9:
  Type already defined

types

N = nat;
N = char;

I don't know why VDMTools only reports a warning if you declare two values with the same same. I think it would be better to report an error.

[ldcouto]

The classic approach do duplicates value names in functional languages is to have the second overshadow the fist. But we should look at the ISO specification and see that it says in terms of duplicate names for the various kinds of defs.

Any volunteers?

[peterwvj]

Maybe we can find it here http://www.nicoplat.com/sites/default/files/tr-isovdmsl.pdf

Unfortunately I can't search the pdf. Maybe @pglvdm knows what the rules for duplicate definitions are? Peter, would you consider it reasonable to always report an error in case of duplicate definitions?

[ldcouto]

Isn't there a searchable pdf somewhere?

Maybe we could try ocr tricks again.

On 23 January 2016 at 19:32, Peter W. V. Tran-Jørgensen < notifications@github.com> wrote:

Maybe we can find it here http://www.nicoplat.com/sites/default/files/tr-isovdmsl.pdf

Unfortunately I can't search the pdf. Maybe @pglvdm https://github.com/pglvdm knows what the rules for duplicate definitions are? Peter, would you consider it reasonable to always report an error in case of duplicate definitions.

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

[peterwvj]

I'm trying to pdfocr the file but each page takes several seconds to convert so it will take a while. I have no idea if this will work, but it's worth a try :)

[ldcouto]

So, on https://github.com/overturetool/language/issues/33 Nick used "pdfimages" and "tesseract". If what you're trying fails, those might be worth a shot.

[pglvdm]

In VDM-SL errors should also be reported with duplicate definitions. It is a pre-condition for the static semantics in the ISO standard that is defined using VDM itself.

[ldcouto]

Does that apply to all kinds of definitions, including values?

[pglvdm]

Yes in VDM-SL there can be no overlap between the names of any definitions (in all categories).

[ldcouto]

Ok, cool. I'm upgrading this to bug.

Is this a type checker or parser bug? @nickbattle is this something the parser can detect?

[nickbattle]

It's a TC bug. The grammar has nothing to say about symbol duplication.

[ldcouto]

Fair enough. TC, it is.

[peterwvj]

Very good. Thanks for your input, Peter

[nickbattle]

I seem to have forgotten about this one too. Will assign myself...