{"action":"created","issue":{"url":"https://api.github.com/repos/overturetool/overture/issues/499","repository_url":"https://api.github.com/repos/overturetool/overture","labels_url":"https://api.github.com/repos/overturetool/overture/issues/499/labels{/name}","comments_url":"https://api.github.com/repos/overturetool/overture/issues/499/comments","events_url":"https://api.github.com/repos/overturetool/overture/issues/499/events","html_url":"https://github.com/overturetool/overture/issues/499","id":130127995,"number":499,"title":"Pure operation checks not working in SL","user":{"login":"nickbattle","id":1751423,"avatar_url":"https://avatars.githubusercontent.com/u/1751423?v=3","gravatar_id":"","url":"https://api.github.com/users/nickbattle","html_url":"https://github.com/nickbattle","followers_url":"https://api.github.com/users/nickbattle/followers","following_url":"https://api.github.com/users/nickbattle/following{/other_user}","gists_url":"https://api.github.com/users/nickbattle/gists{/gist_id}","starred_url":"https://api.github.com/users/nickbattle/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nickbattle/subscriptions","organizations_url":"https://api.github.com/users/nickbattle/orgs","repos_url":"https://api.github.com/users/nickbattle/repos","events_url":"https://api.github.com/users/nickbattle/events{/privacy}","received_events_url":"https://api.github.com/users/nickbattle/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/overturetool/overture/labels/enhancement","name":"enhancement","color":"84b6eb"}],"state":"open","locked":false,"assignee":null,"milestone":{"url":"https://api.github.com/repos/overturetool/overture/milestones/26","html_url":"https://github.com/overturetool/overture/milestones/v2.3.2","labels_url":"https://api.github.com/repos/overturetool/overture/milestones/26/labels","id":1341669,"number":26,"title":"v2.3.2","description":"","creator":{"login":"afterkelsen","id":9878473,"avatar_url":"https://avatars.githubusercontent.com/u/9878473?v=3","gravatar_id":"","url":"https://api.github.com/users/afterkelsen","html_url":"https://github.com/afterkelsen","followers_url":"https://api.github.com/users/afterkelsen/followers","following_url":"https://api.github.com/users/afterkelsen/following{/other_user}","gists_url":"https://api.github.com/users/afterkelsen/gists{/gist_id}","starred_url":"https://api.github.com/users/afterkelsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/afterkelsen/subscriptions","organizations_url":"https://api.github.com/users/afterkelsen/orgs","repos_url":"https://api.github.com/users/afterkelsen/repos","events_url":"https://api.github.com/users/afterkelsen/events{/privacy}","received_events_url":"https://api.github.com/users/afterkelsen/received_events","type":"User","site_admin":false},"open_issues":32,"closed_issues":32,"state":"open","created_at":"2015-10-07T00:31:18Z","updated_at":"2016-02-11T17:21:24Z","due_on":null,"closed_at":null},"comments":14,"created_at":"2016-01-31T13:36:36Z","updated_at":"2016-02-11T22:55:50Z","closed_at":null,"body":"It looks like there is a problem with the TC of pure operations in VDM-SL. The following simple pure operation gives no TC errors in Overture (2.3.0):\r\n```\r\nstate S of\r\n\tx : nat\r\nend\r\n\r\noperations\r\n\tpure op: () ==> ()\r\n\top() ==\r\n\t\tx := 123;\r\n```\r\nBut in VDMJ it complains as expected:\r\n```\r\nParsed 1 module in 0.155 secs. No syntax errors\r\nError 3338: Cannot update state in a pure operation in 'DEFAULT' (TestSL.vdmsl) at line 9:9\r\nError 3344: Pure operation 'op' must return a value in 'DEFAULT' (TestSL.vdmsl) at line 6:10\r\nType checked 1 module in 0.008 secs. Found 2 type errors\r\n```"},"comment":{"url":"https://api.github.com/repos/overturetool/overture/issues/comments/183092192","html_url":"https://github.com/overturetool/overture/issues/499#issuecomment-183092192","issue_url":"https://api.github.com/repos/overturetool/overture/issues/499","id":183092192,"user":{"login":"peterwvj","id":5388919,"avatar_url":"https://avatars.githubusercontent.com/u/5388919?v=3","gravatar_id":"","url":"https://api.github.com/users/peterwvj","html_url":"https://github.com/peterwvj","followers_url":"https://api.github.com/users/peterwvj/followers","following_url":"https://api.github.com/users/peterwvj/following{/other_user}","gists_url":"https://api.github.com/users/peterwvj/gists{/gist_id}","starred_url":"https://api.github.com/users/peterwvj/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/peterwvj/subscriptions","organizations_url":"https://api.github.com/users/peterwvj/orgs","repos_url":"https://api.github.com/users/peterwvj/repos","events_url":"https://api.github.com/users/peterwvj/events{/privacy}","received_events_url":"https://api.github.com/users/peterwvj/received_events","type":"User","site_admin":false},"created_at":"2016-02-11T22:55:50Z","updated_at":"2016-02-11T22:55:50Z","body":"It seems to work for me to on `pvj/main`\r\n\r\n~~~\r\npeter@peter-ubuntu:~/dev/ovtrepo/core/commandline/target$ cat -n SlDemo.vdmsl\r\n     1\tstate S of\r\n     2\t    x : nat\r\n     3\tend\r\n     4\t\r\n     5\toperations\r\n     6\t    pure op: () ==> nat\r\n     7\t    op() ==\r\n     8\t    (\r\n     9\t        x := 0;     -- Error 3338: Cannot update state in a pure operation\r\n    10\t        return 123\r\n    11\t    )\r\n    12\t\r\n    13\tfunctions\r\n    14\t    f: () -> nat\r\n    15\t    f() == op();    -- Warning 5017: Pure operation call may not be referentially transparent\r\npeter@peter-ubuntu:~/dev/ovtrepo/core/commandline/target$ java -jar Overture-2.3.1-SNAPSHOT.jar -vdmsl -i SlDemo.vdmsl \r\nParsed 1 module in 0.084 secs. No syntax errors\r\nError 3338: Cannot update state in a pure operation in 'DEFAULT' (SlDemo.vdmsl) at line 9:9\r\nWarning 5017: Pure operation call may not be referentially transparent in 'DEFAULT' (SlDemo.vdmsl) at line 15:12\r\nType checked 1 module in 0.068 secs. Found 1 type error and 1 warning\r\nBye\r\n~~~"}}