{"action":"created","issue":{"url":"https://api.github.com/repos/overturetool/overture/issues/454","labels_url":"https://api.github.com/repos/overturetool/overture/issues/454/labels{/name}","comments_url":"https://api.github.com/repos/overturetool/overture/issues/454/comments","events_url":"https://api.github.com/repos/overturetool/overture/issues/454/events","html_url":"https://github.com/overturetool/overture/issues/454","id":90936385,"number":454,"title":"Type checker: public class instance variables cannot be accessed from expressions","user":{"login":"nlmave","id":6161283,"avatar_url":"https://avatars.githubusercontent.com/u/6161283?v=3","gravatar_id":"","url":"https://api.github.com/users/nlmave","html_url":"https://github.com/nlmave","followers_url":"https://api.github.com/users/nlmave/followers","following_url":"https://api.github.com/users/nlmave/following{/other_user}","gists_url":"https://api.github.com/users/nlmave/gists{/gist_id}","starred_url":"https://api.github.com/users/nlmave/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nlmave/subscriptions","organizations_url":"https://api.github.com/users/nlmave/orgs","repos_url":"https://api.github.com/users/nlmave/repos","events_url":"https://api.github.com/users/nlmave/events{/privacy}","received_events_url":"https://api.github.com/users/nlmave/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":9,"created_at":"2015-06-25T11:35:58Z","updated_at":"2015-06-26T15:27:32Z","closed_at":null,"body":"The following specification gives a type error while imho it should be allowed\r\n\r\n    class A\r\n    instance variables\r\n      public x : nat\r\n    end A\r\n\r\n    class B\r\n    types\r\n      sa = seq of A\r\n      inv sai == forall i in set inds sai & sai(i).x < 10\r\n    functions\r\n      getX: A -> nat\r\n      getX(pA) == pA.x\r\n    operations\r\n      getOpX: A ==> nat\r\n      getOpX(pA) == return pA.x\r\n    end B\r\n\r\nThe above example produces two errors (in the invariant and in the getX function).\r\nTested on Overture 2.2.6 and VDMTools (which does NOT produce these errors)."},"comment":{"url":"https://api.github.com/repos/overturetool/overture/issues/comments/115730004","html_url":"https://github.com/overturetool/overture/issues/454#issuecomment-115730004","issue_url":"https://api.github.com/repos/overturetool/overture/issues/454","id":115730004,"user":{"login":"nlmave","id":6161283,"avatar_url":"https://avatars.githubusercontent.com/u/6161283?v=3","gravatar_id":"","url":"https://api.github.com/users/nlmave","html_url":"https://github.com/nlmave","followers_url":"https://api.github.com/users/nlmave/followers","following_url":"https://api.github.com/users/nlmave/following{/other_user}","gists_url":"https://api.github.com/users/nlmave/gists{/gist_id}","starred_url":"https://api.github.com/users/nlmave/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nlmave/subscriptions","organizations_url":"https://api.github.com/users/nlmave/orgs","repos_url":"https://api.github.com/users/nlmave/repos","events_url":"https://api.github.com/users/nlmave/events{/privacy}","received_events_url":"https://api.github.com/users/nlmave/received_events","type":"User","site_admin":false},"created_at":"2015-06-26T15:27:32Z","updated_at":"2015-06-26T15:27:32Z","body":"Well I never claimed it would be easy to implement :-). Nevertheless this sounds like reference counting and garbage collecting techniques to me."}}