{"action":"created","issue":{"url":"https://api.github.com/repos/overturetool/overture/issues/480","labels_url":"https://api.github.com/repos/overturetool/overture/issues/480/labels{/name}","comments_url":"https://api.github.com/repos/overturetool/overture/issues/480/comments","events_url":"https://api.github.com/repos/overturetool/overture/issues/480/events","html_url":"https://github.com/overturetool/overture/issues/480","id":115836287,"number":480,"title":"Empty block does not get detected","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},"labels":[{"url":"https://api.github.com/repos/overturetool/overture/labels/bug","name":"bug","color":"fc2929"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-11-09T09:17:52Z","updated_at":"2015-11-18T13:09:18Z","closed_at":null,"body":"In the example given below the type checker does not detect that the `else` branch is an empty block (which is illegal). What's even more odd is that the spec type checks without any errors. This problem only happens in Overture - VDMJ reports the problem with the empty block.\r\n~~~\r\npeter@peter-ubuntu:~/dev/vdm_tools$ cat M.vdmsl \r\noperations\r\n\r\nop: () ==> ()\r\nop () ==\r\n(\r\n  if true then\r\n   a := a + 1\r\n  else\r\n  ()\r\n);\r\npeter@peter-ubuntu:~/dev/vdm_tools$ java -jar vdmj-3.0.1.jar -r vdm10 -vdmsl M.vdmsl \r\nError 2296: Block cannot be empty in 'DEFAULT' (M.vdmsl) at line 9:3\r\nParsed 1 module in 0.129 secs. Found 1 syntax error\r\npeter@peter-ubuntu:~/dev/vdm_tools$ java -jar ~/dev/ovtrepo/core/commandline/target/Overture-2.3.1-SNAPSHOT.jar -r vdm10 -vdmsl M.vdmsl \r\nParsed 1 module in 0.068 secs. No syntax errors\r\nType checked 1 module in 0.062 secs. No type errors\r\npeter@peter-ubuntu:~/dev/vdm_tools$ \r\n~~~"},"comment":{"url":"https://api.github.com/repos/overturetool/overture/issues/comments/157707133","html_url":"https://github.com/overturetool/overture/issues/480#issuecomment-157707133","issue_url":"https://api.github.com/repos/overturetool/overture/issues/480","id":157707133,"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},"created_at":"2015-11-18T13:09:18Z","updated_at":"2015-11-18T13:09:18Z","body":"This is interesting. The logic (in the statement reader, part of the parser) is slightly different between Overture and VDMJ in this area. If you make Overture the same as VDMJ, then it works as expected. So the change was presumably made for some reason, but changing it fixes the problem. Unfortunately, the Overture test suite runs with (and without) the change, so that's not helping me. And the change is present in the oldest version of the file I have in Git (3 years old).\r\n\r\nI suggest I commit this change and we just keep an eye out for empty block or block ending problems?"}}