{"action":"created","issue":{"url":"https://api.github.com/repos/overturetool/language/issues/39","repository_url":"https://api.github.com/repos/overturetool/language","labels_url":"https://api.github.com/repos/overturetool/language/issues/39/labels{/name}","comments_url":"https://api.github.com/repos/overturetool/language/issues/39/comments","events_url":"https://api.github.com/repos/overturetool/language/issues/39/events","html_url":"https://github.com/overturetool/language/issues/39","id":186064776,"number":39,"title":"A Primitive Order Relation for Types in VDM-SL","user":{"login":"paulch42","id":17345606,"avatar_url":"https://avatars.githubusercontent.com/u/17345606?v=3","gravatar_id":"","url":"https://api.github.com/users/paulch42","html_url":"https://github.com/paulch42","followers_url":"https://api.github.com/users/paulch42/followers","following_url":"https://api.github.com/users/paulch42/following{/other_user}","gists_url":"https://api.github.com/users/paulch42/gists{/gist_id}","starred_url":"https://api.github.com/users/paulch42/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/paulch42/subscriptions","organizations_url":"https://api.github.com/users/paulch42/orgs","repos_url":"https://api.github.com/users/paulch42/repos","events_url":"https://api.github.com/users/paulch42/events{/privacy}","received_events_url":"https://api.github.com/users/paulch42/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":8,"created_at":"2016-10-29T07:26:49Z","updated_at":"2016-11-20T12:18:04Z","closed_at":null,"body":"##### Identification of the Originator\r\n\r\nPaul Chisholm\r\n##### Target of the request, defining the affected components of the language definition\r\n\r\nVDM-SL order relation\r\n##### Motivation for the request\r\n\r\nAll types in VDM-SL admit equality via a primitive (i.e. built-in) equality relation. Numeric types in VDM-SL are the only types that admit an order relation. A general purpose order relation can be defined for most types in VDM-SL, in a similar manner to equality. We need only define the < relation; equality plus < allows the derivation of <=, > and >=.\r\n\r\nOrder is ubiquitous. After equality, order is the most commonly used relation in computing. When specifying a data type, we very often require an order relation on the type. In VDM-SL we must define a truth valued function that implements the order relation. If we want the familiar complement of operators (<, <=, >, >=) then we must define four functions. Comparisons in a specification then employ the functions, but using function application notation rather than the familiar symbolic infix notation.\r\n\r\nThe Overture VDM-SL example ISO8601 specifies types for date, time, date/time and duration. The effective use of these types in specifications requires an order relation on each of the four types. Sixteen functions are specified: <, <=, >, >= on each of the four types. In every case the order relation is the ‘obvious’ or ‘natural’ ordering one would expect.\r\n\r\n##### Description of the request\r\n\r\nThe attached VDM-SL module ‘Order.vdmsl’ contains a model of VDM-SL values and defines an order relation over those values. A notion of ‘comparable’ values is defined, with the order relation being total with respect to comparability. The primitive VDM-SL order relation on numeric values could be extended to the order relation defined in ‘Order.vdmsl’.\r\n\r\nNotes:\r\n- As for equality, the ‘:-’ separator in a composite type indicates this field plays no role in the order relation. Since <= is defined in terms of < and = (and >= in terms of > and =), allowing a different set of fields than for equality would lead to inconsistency. That is, it would be possible for both `a=b` and `a<b` to be true.\r\n- Order on functions is excluded.\r\n- Order on tokens is excluded. The VDM-10 Language Manual states “...they cannot be used for anything other than equality and inequality.”\r\n\r\n###### description of the modification\r\n\r\n- Syntax unchanged.\r\n- Type checker generalised to allow the comparison operators to be applied to values of comparable types.\r\n- Interpreter extended to implement order relation.\r\n\r\n###### benefits from the modification\r\n- There is no need to define (up to four) functions associated with a data type.\r\n- Specifications that use the order relation are clearer and easier to interpret since we immediately recognise the familiar symbols and infix notation.\r\n- Proofs can employ the common properties of order relations, rather than having to re-establish them for individual types.\r\n- Sequence comprehension with a set binding requires the set to contain numeric values. With a generic order relation, the sets could contain values of any type that admits order, increasing the utility of sequence comprehension.\r\n- Opens up the possibility of specifying general purpose functions without having to define and pass around explicit order relations.\r\n\r\n###### possible side effects\r\n\r\nNone - existing specifications are semantically unchanged\r\n##### A test suite for validation of the modification in the executable models (if appropriate).\r\n\r\nNone\r\n\r\nThe following is the specification of the order relation as a VDM-SL model.\r\n\r\n[Order.vdmsl.txt](https://github.com/overturetool/language/files/594257/Order.vdmsl.txt)\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/overturetool/language/issues/comments/261774797","html_url":"https://github.com/overturetool/language/issues/39#issuecomment-261774797","issue_url":"https://api.github.com/repos/overturetool/language/issues/39","id":261774797,"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":"2016-11-20T12:18:04Z","updated_at":"2016-11-20T12:18:04Z","body":"Something like:\r\n```\r\nT = nat * nat\r\ninv t == t.#1 <> t.#2\r\norder a, b == (a.#1 + a.#2) < (b.#2 + b.#2);\r\n```\r\nThe order clause would produce a callable function, like T_order: T * T +> bool."}}
{"actor":{"display_login":"nickbattle"}}