overturetool / overture

The Overture Tool
http://overturetool.org
GNU General Public License v3.0
48 stars 25 forks source link

Polymorphic function postconditions have the wrong type #740

Closed nickbattle closed 4 years ago

nickbattle commented 4 years ago

The following spec raises a warning, rather than an error as it should:

values
    V = post_poly[nat](1);  -- should be like (1, 2)

functions
    poly[@T]: @T -> @T
    poly(-) == undefined
    post true;

Warning 3060: Too few arguments in 'DEFAULT' (test.vdm) at line 2:9

The problem is that the type checker is calculating the wrong type for the polymorphic postcondition function, thinking it is a union, which causes the error to be downgraded to a warning, incorrectly. VDMJ correctly produces the following:

Error 3060: Too few arguments in 'DEFAULT' (test.vdm) at line 2:9
Args: 1
Params: (nat, nat)
nickbattle commented 4 years ago

The union is created because the type of the post_poly function links back to both the main poly function definition and the postpoly definition. So the type looked like a union of both functions, which is wrong. The fix is to re-built the definition links in the methods that create the pre and post_ function definitions.

nickbattle commented 4 years ago

Fix now available in ncb/development.