{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T18:40:39Z","timestamp":1694630439893},"reference-count":11,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper introduces a number of new techniques that support systematic manipulation of predicates, operators, healthiness conditions, laws and fixpoints of recursive programs. Necessary restrictions are imposed on the definition of each model so that the inheritance relation can be established by checking a few conditions on the healthiness conditions and the commands. In particular, we intend to identify the conditions that simplify the closure proof of the program operators and enable laws and fixpoints of a model to be inherited by its submodel without re-proof. A recursive program may correspond to different recursive functions in a model and its submodels, because the primitives such as abort and assignment statements are normally represented as different predicates in different models (although the original definition of each operator is unchanged). This paper studies meta-theory in this more general setting. A fixpoint theorem is discovered and applied to clarify the relationship between the partially correct relational model and the totally correct sequential model in UTP. It is shown that, although assignment statements are modified by the new healthiness conditions in the latter model, most laws (including many that are re-proved in UTP) and fixpoints can be inherited directly without re-proof, if the first argument of every sequential composition in each command tree corresponds to a terminating computation. This result also singles out a small number of laws and fixpoints that may no longer hold in the totally correct model.<\/jats:p>","DOI":"10.1007\/s00165-007-0051-6","type":"journal-article","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T16:40:41Z","timestamp":1194885641000},"page":"89-106","source":"Crossref","is-referenced-by-count":0,"title":["Semantic inheritance in unifying theories of programming"],"prefix":"10.1145","volume":"25","author":[{"given":"Yifeng","family":"Chen","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200031"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Chen Y (2006) Hierarchical organisation of predicate-semantic models. In: First international symposium on unifying theories of programming vol 4010 of LNCS. Springer Heidelberg pp 155\u2013172","DOI":"10.1007\/11768173_10"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Chen Y (2007) Inheriting laws for processes with states. In: 6th International conference on integrated formal methods (IFM 07) vol 4591 of LNCS. Springer Heidelberg pp 138\u2013155","DOI":"10.1007\/978-3-540-73210-5_8"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234740"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/27651.27653"},{"key":"e_1_2_1_2_6_2","volume-title":"Unifying theories of programming","author":"Hoare CAR","year":"1998"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"issue":"2","key":"e_1_2_1_2_8_2","first-page":"171","article-title":"Probabilistic models for the guarded command language","volume":"28","author":"He J","year":"1997","journal-title":"Sci Comput Programm"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00082-8"},{"key":"e_1_2_1_2_10_2","volume-title":"The Z notation: a reference manual","author":"Spivey JM","year":"1992","edition":"2"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0051-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0051-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0051-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:58:06Z","timestamp":1641484686000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0051-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1]]},"references-count":11,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["10.1007\/s00165-007-0051-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0051-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,1]]}}}