{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T05:47:24Z","timestamp":1740808044621,"version":"3.38.0"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,12,11]],"date-time":"2010-12-11T00:00:00Z","timestamp":1292025600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci. China"],"published-print":{"date-parts":[[2011,3]]},"DOI":"10.1007\/s11704-010-0112-5","type":"journal-article","created":{"date-parts":[[2010,12,11]],"date-time":"2010-12-11T06:22:20Z","timestamp":1292048540000},"page":"1-13","source":"Crossref","is-referenced-by-count":2,"title":["Property transformation under specification change"],"prefix":"10.1007","volume":"5","author":[{"given":"Zheng","family":"Fu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Graeme","family":"Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,12,11]]},"reference":[{"key":"112_CR1","volume-title":"Using Z: Specification, Refinement, and Proof","author":"J. C. P. Woodcock","year":"1996","unstructured":"Woodcock J C P, Davies J. Using Z: Specification, Refinement, and Proof. New Jersey: Prentice Hall, 1996"},{"key":"112_CR2","volume-title":"Programming From Specifications","author":"C. C. Morgan","year":"1990","unstructured":"Morgan C C. Programming From Specifications. New Jersey: Prentice Hall, 1990"},{"key":"112_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and Their Comparison","author":"W. P. Roever de","year":"1998","unstructured":"de Roever W P, Engelhardt K. Data Refinement: Model-Oriented Proof Methods and Their Comparison. New York: Cambridge University Press, 1998"},{"issue":"7","key":"112_CR4","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1145\/358557.358572","volume":"25","author":"W. Swartout","year":"1982","unstructured":"Swartout W, Balzer R. On the inevitable intertwining of specification and implementation. Communications of the ACM, 1982, 25(7): 438\u2013440","journal-title":"Communications of the ACM"},{"key":"112_CR5","doi-asserted-by":"crossref","unstructured":"van Schouwen A J, Parnas D, Madey J. Documentation of requirements for computer systems. In: Proceedings of 1st IEEE Symposium on Requirements Engineering. 1993, 198\u2013207","DOI":"10.1109\/ISRE.1993.324857"},{"issue":"4","key":"112_CR6","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/BF01211217","volume":"7","author":"I. J. Hayes","year":"1995","unstructured":"Hayes I J, Sanders J W. Specification by interface separation. Formal Aspects of Computing, 1995, 7(4): 430\u2013439","journal-title":"Formal Aspects of Computing"},{"key":"112_CR7","volume-title":"Defaults in the specification of reactive systems","author":"S. Guerra","year":"1999","unstructured":"Guerra S. Defaults in the specification of reactive systems. Dissertation for the Doctoral Degree. London: University College London, 1999"},{"key":"112_CR8","unstructured":"Bredereke J. Families of formal requirements in telephone switching. In: Calder M, Magill E H, eds. Feature Interactions in Telecommunications and Software Systems. IOS Press, 2000, 257\u2013273"},{"key":"112_CR9","doi-asserted-by":"crossref","unstructured":"van Lamsweerde A, Darimont R, Massonet P. Goaldirected elaboration of requirements for a meeting scheduler: Problems and lessons learnt. In: Proceedings of 2nd IEEE Symposium on Requirements Engineering. 1995, 194\u2013203","DOI":"10.1109\/ISRE.1995.512561"},{"key":"112_CR10","unstructured":"Liu S. Evolution: A more practical approach than refinement for software development. In: Proceedings of 1997 IEEE International Conference on Engineering of Complex Computer Systems. 1997, 142\u2013151"},{"key":"112_CR11","doi-asserted-by":"crossref","unstructured":"Smith G. Stepwise development from ideal specifications. In: Proceedings of 23rd Australasian Computer Science Conference. 2000, 227\u2013233","DOI":"10.1109\/ACSC.2000.824408"},{"issue":"2\u20133","key":"112_CR12","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1016\/j.scico.2007.04.002","volume":"67","author":"R. Banach","year":"2007","unstructured":"Banach R, Poppleton M, Jeske C, Stepney S. Engineering and theoretical underpinnings of retrenchment. Science of Computer Programming, 2007, 67(2\u20133): 301\u2013329","journal-title":"Science of Computer Programming"},{"key":"112_CR13","first-page":"995","volume-title":"Temporal and Modal Logic. Handbook of Theoretical Computer Science (Vol. B): Formal Models and Semantics","author":"E. A. Emerson","year":"1990","unstructured":"Emerson E A. Temporal and Modal Logic. Handbook of Theoretical Computer Science (Vol. B): Formal Models and Semantics. Cambridge: MIT Press, 1990, 995\u20131072"},{"key":"112_CR14","doi-asserted-by":"crossref","unstructured":"Smith G, Winter K. Proving temporal properties of Z specifications using abstraction. In: Proceedings of 3rd International Conference of Z and B Users. 2003, 260\u2013270","DOI":"10.1007\/3-540-44880-2_17"},{"key":"112_CR15","doi-asserted-by":"crossref","unstructured":"Smith G, Wildman L. Model checking Z specifications using SAL. In: Proceedings of 4th International Conference of Z and B Users. 2005, 85\u2013103","DOI":"10.1007\/11415787_6"},{"key":"112_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0257-1","volume-title":"Refinement in Z and Object-Z: Foundations and Advanced Applications","author":"J. Derrick","year":"2001","unstructured":"Derrick J, Boiten E. Refinement in Z and Object-Z: Foundations and Advanced Applications. London: Springer-Verlag, 2001"},{"key":"112_CR17","doi-asserted-by":"crossref","unstructured":"Fu Z, Smith G. Towards more flexible development of Z specifications. In: Proceedings of 2nd IFIP\/IEEE International Symposium on Theoretical Aspects of Software Engineering. 2008, 281\u2013288","DOI":"10.1109\/TASE.2008.20"},{"issue":"3","key":"112_CR18","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G. L. Peterson","year":"1981","unstructured":"Peterson G L. Myths about the mutual exclusion problem. Information Processing Letters, 1981, 12(3): 115\u2013116","journal-title":"Information Processing Letters"},{"key":"112_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5265-9","volume-title":"The Object-Z Specification Language","author":"G. Smith","year":"2000","unstructured":"Smith G. The Object-Z Specification Language. Hingham: Kluwer Academic Publishers, 2000"},{"key":"112_CR20","doi-asserted-by":"crossref","unstructured":"Derrick J, Smith G. Linear temporal logic and Z refinement. In: Proceedings of 10th International Conference on Algebraic Methodology and Software Technology. 2004, 117\u2013131","DOI":"10.1007\/978-3-540-27815-3_13"},{"key":"112_CR21","doi-asserted-by":"crossref","unstructured":"McComb T, Smith G. A minimal set of refactoring rules for Object-Z. In: Proceedings of 10th IFIP WG 6.1 international conference on Formal Methods for Open Object-Based Distributed Systems. 2008, 170\u2013184","DOI":"10.1007\/978-3-540-68863-1_11"}],"container-title":["Frontiers of Computer Science in China"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-010-0112-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-010-0112-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-010-0112-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T18:14:37Z","timestamp":1740766477000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-010-0112-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,11]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,3]]}},"alternative-id":["112"],"URL":"https:\/\/doi.org\/10.1007\/s11704-010-0112-5","relation":{},"ISSN":["1673-7350","1673-7466"],"issn-type":[{"type":"print","value":"1673-7350"},{"type":"electronic","value":"1673-7466"}],"subject":[],"published":{"date-parts":[[2010,12,11]]}}}