overturetool
Type checker: duplicate function and operation definitions in SL should be treated as errors
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.
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?
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?
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 < [email protected]> 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 .
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 :)
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.
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.
Yes in VDM-SL there can be no overlap between the names of any definitions (in all categories).
Ok, cool. I'm upgrading this to bug.
Is this a type checker or parser bug? @nickbattle is this something the parser can detect?
