{"action":"created","issue":{"url":"https://api.github.com/repos/jcoplien/trygve/issues/76","repository_url":"https://api.github.com/repos/jcoplien/trygve","labels_url":"https://api.github.com/repos/jcoplien/trygve/issues/76/labels{/name}","comments_url":"https://api.github.com/repos/jcoplien/trygve/issues/76/comments","events_url":"https://api.github.com/repos/jcoplien/trygve/issues/76/events","html_url":"https://github.com/jcoplien/trygve/issues/76","id":133601983,"number":76,"title":"Unused stageprop as type","user":{"login":"mbrowne","id":874316,"avatar_url":"https://avatars.githubusercontent.com/u/874316?v=3","gravatar_id":"","url":"https://api.github.com/users/mbrowne","html_url":"https://github.com/mbrowne","followers_url":"https://api.github.com/users/mbrowne/followers","following_url":"https://api.github.com/users/mbrowne/following{/other_user}","gists_url":"https://api.github.com/users/mbrowne/gists{/gist_id}","starred_url":"https://api.github.com/users/mbrowne/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mbrowne/subscriptions","organizations_url":"https://api.github.com/users/mbrowne/orgs","repos_url":"https://api.github.com/users/mbrowne/repos","events_url":"https://api.github.com/users/mbrowne/events{/privacy}","received_events_url":"https://api.github.com/users/mbrowne/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2016-02-15T01:39:03Z","updated_at":"2016-02-17T10:43:00Z","closed_at":null,"body":"I noticed that the following code compiles and runs, and I'm wondering if it should. (If this is more of a discussion item, we can move it to the group.) Note that the 'Amount' stageprop is never bound, so it's not really a stageprop; it's only being used as a parameter type.\r\n\r\n\tcontext Account {\r\n\t\tpublic Account(List<LedgerEntry> ledgers) {\r\n\t\t\tLedgers = ledgers;\r\n\t\t}\r\n\t\r\n\t\tpublic Account() {\r\n\t\t\tLedgers = new List<LedgerEntry>();\r\n\t\t}\r\n\t\r\n\t\tpublic void increaseBalance(Amount amount) {\r\n\t\t\tLedgers.addEntry(\"depositing\", amount + 0);\r\n\t\t}\r\n\t\r\n\t\tpublic void decreaseBalance(Amount amount) {\r\n\t\t\tLedgers.addEntry(\"withdrawing\", 0 - (amount + 0));\r\n\t\t}\r\n\t\r\n\t\tpublic int getBalance() {\r\n\t\t\treturn Ledgers.calculateBalance();\r\n\t\t}\r\n\t\r\n\t\tstageprop Amount {} requires {\r\n\t\t   int compareTo(int amt) const;\r\n\t\t   int +(int amt) const;\r\n\t\t   int -(int amt) const;\r\n\t\t}\r\n\t\r\n\t\trole Ledgers {\r\n\t\t\tpublic void addEntry(String message, int amount) {\r\n\t\t\t\tLedgers.add(new LedgerEntry(message, amount));\r\n\t\t\t}\r\n\t\t\r\n\t\t\tpublic int calculateBalance() {\r\n\t\t\t\tint sum = 0;\r\n\t\t\t\tfor (int i = 0; i < Ledgers.size(); i++) {\r\n\t\t\t\t\tsum = sum + Ledgers.get(i).amount();\r\n\t\t\t\t}\r\n\t\t\t\treturn sum;\r\n\t\t\t}\r\n\t\t}\r\n\t\trequires {\r\n\t\t\tvoid add(LedgerEntry entry);\r\n\t\t\tLedgerEntry get(int pos);\r\n\t\t\tint size();\r\n\t\t}\r\n\t}\r\n\r\n\tclass LedgerEntry\r\n\t{\r\n\t\tprivate String message_;\r\n\t\tprivate int amount_;\r\n\r\n\t\tpublic LedgerEntry(String message, int amount) {\r\n\t\t\tmessage_ = message.clone;\r\n\t\t\tamount_ = amount.clone;\r\n\t\t}\r\n\t\r\n\t\tpublic String message() {\r\n\t\t\treturn message_;\r\n\t\t}\r\n\t\r\n\t\tpublic int amount() {\r\n\t\t\treturn amount_;\r\n\t\t}\r\n\t}\r\n\r\n\t{\r\n\t\tAccount src = new Account();\r\n\t\tsrc.increaseBalance(30);\r\n\t\tSystem.out.println(src.getBalance());\r\n\t}"},"comment":{"url":"https://api.github.com/repos/jcoplien/trygve/issues/comments/185148771","html_url":"https://github.com/jcoplien/trygve/issues/76#issuecomment-185148771","issue_url":"https://api.github.com/repos/jcoplien/trygve/issues/76","id":185148771,"user":{"login":"jcoplien","id":7209130,"avatar_url":"https://avatars.githubusercontent.com/u/7209130?v=3","gravatar_id":"","url":"https://api.github.com/users/jcoplien","html_url":"https://github.com/jcoplien","followers_url":"https://api.github.com/users/jcoplien/followers","following_url":"https://api.github.com/users/jcoplien/following{/other_user}","gists_url":"https://api.github.com/users/jcoplien/gists{/gist_id}","starred_url":"https://api.github.com/users/jcoplien/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jcoplien/subscriptions","organizations_url":"https://api.github.com/users/jcoplien/orgs","repos_url":"https://api.github.com/users/jcoplien/repos","events_url":"https://api.github.com/users/jcoplien/events{/privacy}","received_events_url":"https://api.github.com/users/jcoplien/received_events","type":"User","site_admin":false},"created_at":"2016-02-17T10:43:00Z","updated_at":"2016-02-17T10:43:00Z","body":"\n> Den 16/02/2016 kl. 21.14 skrev Matt Browne <notifications@github.com>:\n> \n> Maybe a compiler error saying there is no code path that would cause the \n> stageprop to be bound.\n\nDo we know of an algorithm that can identify whether a given line is reachable? That is, are you hoping for us to implement a solution to the halting problem?\n\n\n> So to sum up: I'm not really sure, but I \n> thought I'd report this in case you consider it invalid code.\n\nSo we’re not really sure there is a problem?"}}