{"action":"created","issue":{"url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/398","labels_url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/398/labels{/name}","comments_url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/398/comments","events_url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/398/events","html_url":"https://github.com/Whiley/WhileyCompiler/issues/398","id":40098649,"number":398,"title":"Semantics for List ElementOf","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":[{"url":"https://api.github.com/repos/Whiley/WhileyCompiler/labels/Feature","name":"Feature","color":"02e10c"},{"url":"https://api.github.com/repos/Whiley/WhileyCompiler/labels/Important","name":"Important","color":"DDDDDD"},{"url":"https://api.github.com/repos/Whiley/WhileyCompiler/labels/WYC","name":"WYC","color":"000000"}],"state":"closed","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":19,"closed_issues":10,"state":"open","created_at":"2014-10-11T06:51:33Z","updated_at":"2015-08-01T21:55:27Z","due_on":"2015-04-29T12:00:00Z","closed_at":null},"comments":2,"created_at":"2014-08-12T21:00:29Z","updated_at":"2015-08-01T21:55:27Z","closed_at":"2015-08-01T21:55:27Z","body":"The following does not verify because of the semantics for <code>x in xs</code>, which are rather unclear at the moment.  Specifically, this hits the familiar problem that the verifier believes <code>x</code> is a tuple of <code>(index,element)</code>, rather than just the element.\r\n\r\n<pre>\r\nfunction contains([int] xs, int x) => (bool r)\r\nensures r ==> x in xs:\r\n    //\r\n    int i = 0\r\n    //\r\n    while i < |xs| where i >= 0:\r\n        if xs[i] == x:\r\n            return true\r\n        i = i + 1\r\n    //\r\n    return false\r\n</pre>\r\n\r\nThis really goes to the heart of the problem relating to the semantics of set operations for collections, and subtyping between collections."},"comment":{"url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/comments/126956332","html_url":"https://github.com/Whiley/WhileyCompiler/issues/398#issuecomment-126956332","issue_url":"https://api.github.com/repos/Whiley/WhileyCompiler/issues/398","id":126956332,"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},"created_at":"2015-08-01T21:55:27Z","updated_at":"2015-08-01T21:55:27Z","body":"This is moot now because the element of operator has been removed."}}