{"action":"created","issue":{"url":"https://api.github.com/repos/overturetool/language/issues/27","labels_url":"https://api.github.com/repos/overturetool/language/issues/27/labels{/name}","comments_url":"https://api.github.com/repos/overturetool/language/issues/27/comments","events_url":"https://api.github.com/repos/overturetool/language/issues/27/events","html_url":"https://github.com/overturetool/language/issues/27","id":38982309,"number":27,"title":"\"Pure\" operations called in functions","user":{"login":"joey-coleman","id":1689646,"avatar_url":"https://avatars.githubusercontent.com/u/1689646?v=3","gravatar_id":"","url":"https://api.github.com/users/joey-coleman","html_url":"https://github.com/joey-coleman","followers_url":"https://api.github.com/users/joey-coleman/followers","following_url":"https://api.github.com/users/joey-coleman/following{/other_user}","gists_url":"https://api.github.com/users/joey-coleman/gists{/gist_id}","starred_url":"https://api.github.com/users/joey-coleman/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/joey-coleman/subscriptions","organizations_url":"https://api.github.com/users/joey-coleman/orgs","repos_url":"https://api.github.com/users/joey-coleman/repos","events_url":"https://api.github.com/users/joey-coleman/events{/privacy}","received_events_url":"https://api.github.com/users/joey-coleman/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/overturetool/language/labels/Execution","name":"Execution","color":"009800"},{"url":"https://api.github.com/repos/overturetool/language/labels/Request%20for%20Modification","name":"Request for Modification","color":"006b75"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":240,"created_at":"2014-07-29T12:09:18Z","updated_at":"2015-08-21T14:12:55Z","closed_at":null,"body":"> The following bug was [originally reported](https://sourceforge.net/p/overture/bugs/27/) on Sourceforge by [ldcouto](https://sourceforge.net/u/ldcouto/profile/), 2014-07-28 06:14:14.783000:\n\n1 Identification of the Originator\r\nLuis Diogo Couto\r\n\r\n\r\n2 Target of the request: defining the affected components of the language\r\nIntroduce \"pure\" operations and allow them to be called inside functions. \r\nPure operations do not affect the state of any object.\r\n\r\n\r\n3 Motivation for the request\r\nWhen using an object as a function parameter, it is often necessary to query\r\nthe internal state of the object. A typical example is when the object is used\r\nas an operation parameter and its internal state needs to be inspected in the\r\npre condition.\r\n\r\nThe only way to do that at the moment is to make the relevant instance variables\r\npublic, which breaks encapsulation. \r\n\r\n\r\n4 Description of the request, including: \r\n(a) description of the modification:\r\nAllow pure operations to be called inside functions.  A pure operation does\r\nnot affect the state of  its object nor of any other. It is referentially\r\ntransparent.\r\n\r\nPure operations can only read instance variables and call functions and other\r\npure operations.\r\n\r\nA new keyword \"pure\" can be introduced to identify these operations.\r\n\r\nAnother option is to use the externals clause.  An operation that contains ext\r\nrd x is pure. Currently such an operation can call any operations on x so the\r\nsemantics of ext rd would be altered.\r\n\r\n(b) benefits from the modification: \r\nWhen using an object as a function parameter it would be possible to check (or\r\nget) data that depends on the internal state of the object. This could be done\r\nwithout exposing the internal state of the object, which is an important\r\nprinciple of OO design.\r\n\r\nThis would be particularly helpful if we want to use objects in pre/post\r\nconditions and invariants, which are signature features of VDM.  Pure\r\noperations would be particularly suited to implement the checks that these\r\nconditions rely on.\r\n\r\n(c) possible side effects:\r\nIf the new keyword is introduced, current models that use it as a name will no\r\nlonger be correct. For what it's worth, none of the overture examples use the\r\nword pure as a name.\r\n\r\nIf the semantics of ext rd are altered, models that use it may no longer\r\nbe correct. 11 examples use ext rd, though I have not checked the bodies of\r\nthose operations.\r\n\r\n\r\n5 Source code and technical documentation where applicable\r\nDocumentation: new keyword or updated semantics of ext rd need to explained in\r\nthe language manual.\r\n\r\nSource code: the new keyword would require changes to the parser. Both versions\r\nwould require changes to the type checker.\r\n\r\n\r\n6 A test suite for validation of the modification in the executable models.\r\nN/A\r\n"},"comment":{"url":"https://api.github.com/repos/overturetool/language/issues/comments/133437867","html_url":"https://github.com/overturetool/language/issues/27#issuecomment-133437867","issue_url":"https://api.github.com/repos/overturetool/language/issues/27","id":133437867,"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-08-21T14:12:55Z","updated_at":"2015-08-21T14:12:55Z","body":"PGL is currently going through the example specs that we have, converting them to be \"pure\" (thanks for this Peter!). He's come across an interesting case where a function is creating an object with \"new\".\r\n\r\nIn the discussion above, we concluded that constructors could not be pure - they implicitly change the state of the system, albeit usually only their own state. But I don't have a typechecker error for calls to \"new\" in a functional context. What actually happens is that a runtime check catches that the constructor is not pure while the spec is in \"spooky pure mode\" (a pre/post/inv).\r\n\r\nBut is it really an error to create new objects in a function? We can already treat objects much like records in functions (accessing their fields for example). So is it a problem to create a new one, any more than creating a new mk_R() would be? And does that mean constructors can be pure?"}}