{"action":"opened","issue":{"url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/509","labels_url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/509/labels{/name}","comments_url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/509/comments","events_url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/509/events","html_url":"https://github.com/Whiley/WhileyCompiler/issues/509","id":97272190,"number":509,"title":"Variable Capture with Quantifiers","user":{"login":"DavePearce","id":484459,"avatar_url":"https://avatars.githubusercontent.com/u/484459?v=3","gravatar_id":"","url":"https://api.github.com/users/DavePearce","html_url":"https://github.com/DavePearce","followers_url":"https://api.github.com/users/DavePearce/followers","following_url":"https://api.github.com/users/DavePearce/following{/other_user}","gists_url":"https://api.github.com/users/DavePearce/gists{/gist_id}","starred_url":"https://api.github.com/users/DavePearce/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DavePearce/subscriptions","organizations_url":"https://api.github.com/users/DavePearce/orgs","repos_url":"https://api.github.com/users/DavePearce/repos","events_url":"https://api.github.com/users/DavePearce/events{/privacy}","received_events_url":"https://api.github.com/users/DavePearce/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":{"url":"https://api.github.com/repos/Whiley/WhileyCompiler/milestones/30","html_url":"https://github.com/Whiley/WhileyCompiler/milestones/ChangeList%20Pre%20v0.4.0","labels_url":"https://api.github.com/repos/Whiley/WhileyCompiler/milestones/30/labels","id":822002,"number":30,"title":"ChangeList Pre v0.4.0","description":"This milestone characterises the complete list of changes I'm planning ahead of the v0.4.0 release.","creator":{"login":"DavePearce","id":484459,"avatar_url":"https://avatars.githubusercontent.com/u/484459?v=3","gravatar_id":"","url":"https://api.github.com/users/DavePearce","html_url":"https://github.com/DavePearce","followers_url":"https://api.github.com/users/DavePearce/followers","following_url":"https://api.github.com/users/DavePearce/following{/other_user}","gists_url":"https://api.github.com/users/DavePearce/gists{/gist_id}","starred_url":"https://api.github.com/users/DavePearce/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DavePearce/subscriptions","organizations_url":"https://api.github.com/users/DavePearce/orgs","repos_url":"https://api.github.com/users/DavePearce/repos","events_url":"https://api.github.com/users/DavePearce/events{/privacy}","received_events_url":"https://api.github.com/users/DavePearce/received_events","type":"User","site_admin":false},"open_issues":21,"closed_issues":7,"state":"open","created_at":"2014-10-11T06:51:33Z","updated_at":"2015-07-26T01:14:45Z","due_on":"2015-04-29T12:00:00Z","closed_at":null},"comments":0,"created_at":"2015-07-26T01:14:45Z","updated_at":"2015-07-26T01:14:45Z","closed_at":null,"body":"The following fails to verify in WyCS because of variable capture between quantifiers:\r\n\r\n<pre>\r\ndefine invariant([int] items, int item, int i) is:\r\n    forall (int j):\r\n        if:\r\n            0 <= j\r\n            j < i\r\n        then:\r\n            items[j] == item\r\n\r\nassert:\r\n    forall ([int] items, int item, int i):\r\n        if:\r\n            invariant(items, item, i)            \r\n        then:\r\n            invariant(items, item, i)\r\n</pre>\r\n\r\nThe generated WyRL automaton looks like this:\r\n\r\n<pre>\r\nExists[{[Var(\"r4\"),ArrayT[true,IntT]],[Var(\"r5\"),IntT],[Var(\"r6\"),IntT],[Var(\"r3\"),IntT]},Or{\r\n\tAnd{\r\n\t\tForAll[{[Var(\"r3\"),IntT]},Or{\r\n\t\t\tInequality[IntT,Sum[-1.0,{|Mul[-1.0,{|Var(\"r3\")|}]|}]],\r\n\t\t\tInequality[IntT,Sum[0.0,{|Mul[-1.0,{|Var(\"r6\")|}],Mul[1.0,{|Var(\"r3\")|}]|}]],\r\n\t\t\tEquation[IntT,Sum[0.0,{|Mul[-1.0,{|IndexOf[Var(\"r4\"),Var(\"r3\")]|}],Mul[1.0,{|Var(\"r5\")|}]|}]]\r\n\t\t}],\r\n\t\tInequality[IntT,Var(\"r3\")],\r\n\t\tInequality[IntT,Sum[-1.0,{|Mul[-1.0,{|Var(\"r3\")|}],Mul[1.0,{|Var(\"r6\")|}]|}]],\r\n\t\tInequality[IntT,Sum[-1.0,{|Mul[1.0,{|IndexOf[Var(\"r4\"),Var(\"r3\")]|}],Mul[-1.0,{|Var(\"r5\")|}]|}]]\r\n\t},\r\n\tAnd{\r\n\t\tForAll[{[Var(\"r3\"),IntT]},Or{\r\n\t\t\tInequality[IntT,Sum[-1.0,{|Mul[-1.0,{|Var(\"r3\")|}]|}]],\r\n\t\t\tInequality[IntT,Sum[0.0,{|Mul[-1.0,{|Var(\"r6\")|}],Mul[1.0,{|Var(\"r3\")|}]|}]],\r\n\t\t\tEquation[IntT,Sum[0.0,{|Mul[-1.0,{|IndexOf[Var(\"r4\"),Var(\"r3\")]|}],Mul[1.0,{|Var(\"r5\")|}]|}]]\r\n\t\t}],\r\n\t\tInequality[IntT,Var(\"r3\")],\r\n\t\tInequality[IntT,Sum[-1.0,{|Mul[-1.0,{|Var(\"r3\")|}],Mul[1.0,{|Var(\"r6\")|}]|}]],\r\n\t\tInequality[IntT,Sum[-1.0,{|Mul[-1.0,{|IndexOf[Var(\"r4\"),Var(\"r3\")]|}],Mul[1.0,{|Var(\"r5\")|}]|}]]\r\n\t}\r\n}]\r\n</pre>\r\n\r\nHere we can see that variable <code>r3</code> is defined twice."}}