{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T17:30:05Z","timestamp":1694626205172},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2006,9,1]],"date-time":"2006-09-01T00:00:00Z","timestamp":1157068800000},"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":[[2006,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            This paper presents a new strand of investigation which complements our previous investigation of refinement for specifications whose semantics is given by\n            <jats:italic>partial<\/jats:italic>\n            relations (using Z as a linguistic vehicle for this semantics). It revolves around extending our mathematical apparatus so as to continue our quest for examining mathematically the essence of the lifted-totalisation semantics (which underlies the de facto standard notion of refinement in Z) and the role of the semantic elements  in model-theoretic refinement, but this time in the\n            <jats:italic>abortive paradigm<\/jats:italic>\n            . The analysis is given in two salient parts. In the first part, we consider the simpler framework of\n            <jats:italic>operation-refinement:<\/jats:italic>\n            we examine the (\n            <jats:italic>de facto<\/jats:italic>\n            ) standard account of operation-refinement in this regime by introducing a simpler,\n            <jats:italic>normative<\/jats:italic>\n            theory which captures the notion of\n            <jats:italic>firing-conditions<\/jats:italic>\n            refinement directly in the language and in terms of the natural properties of preconditions and postconditions. In the second part, we generalise our analysis to a more intricate investigation of\n            <jats:italic>simulation-based<\/jats:italic>\n            <jats:italic>data-refinement<\/jats:italic>\n            . The proof-theoretic approach we undertake in the formal analysis provides us with a mathematical apparatus which enables us to examine\n            <jats:italic>precisely<\/jats:italic>\n            the relationships amongst the various theories of refinement. This enables us to examine the general mathematical role that the  values play in model-theoretic refinement in the abortive paradigm, as well as the significance of the unique interaction of these values with the notions of\n            <jats:italic>lifting<\/jats:italic>\n            (of data simulations) and\n            <jats:italic>lifted-totalisation<\/jats:italic>\n            (of operations) in this regime. Furthermore, we generalise this mathematical analysis to a more\n            <jats:italic>conceptual<\/jats:italic>\n            one which also involves\n            <jats:italic>extreme specifications<\/jats:italic>\n            .\n          <\/jats:p>","DOI":"10.1007\/s00165-006-0006-3","type":"journal-article","created":{"date-parts":[[2006,8,10]],"date-time":"2006-08-10T11:32:23Z","timestamp":1155209543000},"page":"329-363","source":"Crossref","is-referenced-by-count":4,"title":["An analysis of refinement in an abortive paradigm"],"prefix":"10.1145","volume":"18","author":[{"given":"Moshe","family":"Deutsch","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Essex, Wivenhoe Park, CO4 3SQ, Colchester, Essex, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin C.","family":"Henson","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Essex, Wivenhoe Park, CO4 3SQ, Colchester, Essex, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_2_1_2_2_2","unstructured":"Azada D Muenchaisri P (ed.) (2003) APSEC 2003: 10th Asia-Pacific software engineering conference Chiangmai Thailand December 10-12 2003. Proceedings. IEEE Computer Society Press"},{"key":"e_1_2_1_2_3_2","unstructured":"Bowen JP Dunne SE Galloway A King S (ed.) (2000) ZB 2000: Formal specification and development in Z and B first international conference of B and Z users York UK August 29\u2013September 2 2000 Proceedings vol 1878 of Lecture Notes in Computer Science . Springer Berlin Heidelberg New York"},{"key":"e_1_2_1_2_4_2","unstructured":"Boiten EA de Roever WP (2003) Getting to the bottom of relational refinement: relations and correctness partial and total. In: Berghammer R M\u00f6 ller B (eds) RelMiCS 7: 7th international seminar on relational methods in computer science Malente Germany 12\u201317 May Proceedings. pp. 82\u201388 University of Kiel"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bolton C Davies J Woodcock JCP (1999) On the refinement and simulation of data types and processes. In: Araki K Galloway A Taguchi K (eds). Integrated formal methods (IFM \u201999) . Springer Berlin Heidelberg New York","DOI":"10.1007\/978-1-4471-0851-1_15"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bowen JP Fett A Hinchey MG (eds) (1998) ZUM \u201998: The Z formal specification notation 11th international conference of Z users Berlin Germany September 24\u201326 1998 Proceedings vol 1493 of Lecture Notes in Computer Science . Springer Berlin Heidelberg New York","DOI":"10.1007\/b68208"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner D Hoare CAR Langmaack H (1990) (eds) VDM \u201990 VDM and Z \u2013 Formal methods in software development third international symposium of VDM Europe Kiel FRG April 17\u201321 1990 Proceedings vol 428 of Lecture Notes in Computer Science . Springer Berlin Heidelberg New York","DOI":"10.1007\/3-540-52513-0"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_1_2_9_2","unstructured":"Cavalcanti ALC Woodcock JCP (1997) A weakest precondition semantics for Z. Technical Monograph PRG-TR-16-97 . Oxford University Computing Laboratory Oxford"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(99)00044-0"},{"key":"e_1_2_1_2_11_2","unstructured":"Derrick J Boiten EA (2001) Refinement in Z and Object-Z: foundations and advanced applications . Formal approaches to computing and information technology \u2013 FACIT. Springer Berlin Heidelberg New York"},{"key":"e_1_2_1_2_12_2","unstructured":"Derrick J Boiten EA (eds) (2005) REFINE 2005 international workshop Electronic Notes in Theoretical Computer Science . BCS-FACS"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Bert D Bowen JP King S Wald\u00e9n M (eds)(2003) ZB 2003: formal specification and development in Z and B third international conference of B and Z users Turku Finland June 4\u20136 2003 Proceedings vol 2651 of Lecture Notes in Computer Science . Springer Berlin Heidelberg New York","DOI":"10.1007\/3-540-44880-2"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.5.663"},{"key":"e_1_2_1_2_15_2","unstructured":"Deutsch M (2002) Firing Conditions . University of Essex technical report CSM-386"},{"key":"e_1_2_1_2_16_2","unstructured":"Deutsch M (2005) An Analysis of total correctness refinement models for partial relation semantics. PhD thesis University of Essex"},{"key":"e_1_2_1_2_17_2","unstructured":"Deutsch M Henson MC (2003) An analysis of backward simulation data-refinement for partial relation semantics. In: APSEC 2003 AM03 pp. 38\u201348"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Deutsch M Henson MC (2003) An analysis of forward simulation data refinement. In: ZB 2003 [DBKW03 pp. 148\u2013167","DOI":"10.1007\/3-540-44880-2_11"},{"issue":"3","key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1093\/jigpal\/11.3.319","article-title":"An analysis of total correctness refinement models for partial relation semantics II","volume":"11","author":"Deutsch M","year":"2003","journal-title":"Logic J IGPL"},{"key":"e_1_2_1_2_20_2","unstructured":"Deutsch M Henson MC (2003) Four theories for backward simulation data-refinement. In: Muntean T Sere K (eds) RCS\u201903 \u2013 2nd international workshop on refinement of critical systems: methods tools and developments . \u00c4bo Academi Turku \u2013 Finland"},{"key":"e_1_2_1_2_21_2","unstructured":"Deutsch M Henson MC (2005) An analysis of operation-refinement in an abortive paradigm. In: REFINE 2005 [DB05"},{"issue":"3","key":"e_1_2_1_2_22_2","first-page":"287","article-title":"An analysis of total correctness refinement models for partial relation semantics I","volume":"11","author":"Deutsch M","year":"2003","journal-title":"Logic J IGPL"},{"key":"e_1_2_1_2_23_2","unstructured":"Deutsch M Henson MC Reeves S (2003) Modular reasoning in Z: scrutinising monotonicity and refinement. University of Essex technical report CSM-407 (under consideration of FACJ)"},{"key":"e_1_2_1_2_24_2","unstructured":"Diller A (1994) Z: An introduction to formal methods 2nd edn. Wiley New York"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"de Roever WP Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison . Prentice Hall International New Jersey","DOI":"10.1017\/CBO9780511663079"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Fischer C (1998) How to combine Z with a process algebra. In: ZUM \u201998 BFJ98 pp. 5\u201323","DOI":"10.1007\/978-3-540-49676-2_2"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00200-7"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01212407"},{"key":"e_1_2_1_2_29_2","unstructured":"Grundy J (1993) A method of program refinement. PhD thesis University of Cambridge"},{"key":"e_1_2_1_2_30_2","unstructured":"He J Hoare CAR (1990) Prespecification and data refinement. In: Data refinement in a categorical setting technical monograph PRG-90 . Oxford University Computing Laboratory Oxford"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"He J Hoare CAR Sanders JW (1986) Data refinement refined. In: Goos G Hartmanis J (eds) European symposium on programming (ESOP \u201986) vol 213 of Lecture Notes in Computer Science. Springer Berlin Heidelberg New York pp 187\u2013196","DOI":"10.1007\/3-540-16442-1_14"},{"issue":"2","key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0020-0190(87)90224-9","article-title":"Prespecification in data refinement","volume":"25","author":"He J","year":"1987","journal-title":"Inf Proces Lett"},{"key":"e_1_2_1_2_33_2","unstructured":"Hayes IJ Jones CB Nicholls JE (1993) Understanding the differences between VDM and Z. Technical Report UMCS-93-8-1 . Department of Computer Science University of Manchester"},{"key":"e_1_2_1_2_34_2","unstructured":"Henson MC Kajtazi B (2005) The Specification Logic vZ s. In: REFINE 2005 [DB05"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050038"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050039"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.1.43"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Henson MC Reeves S (2000) Program development and specification refinement in the schema calculus. In: ZB 2000 [BDGKB00] pp 344\u2013362","DOI":"10.1007\/3-540-44525-0_20"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Henson MC Reeves S(2003) A logic for schema-based program development. Formal Aspects of Computing 15(1):84\u201399 2003","DOI":"10.1007\/s00165-003-0004-7"},{"issue":"4","key":"e_1_2_1_2_41_2","first-page":"381","article-title":"Z logic and its consequences","volume":"22","author":"Henson MC","year":"2003","journal-title":"Comput Informat"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.5555\/94062"},{"key":"e_1_2_1_2_43_2","volume-title":"Specifying reactive systems in Z Technical Monograph PRG-TR-19-91","author":"Josephs MB","year":"1991"},{"key":"e_1_2_1_2_44_2","unstructured":"Manna Z (1974) Mathematical theory of computation. Computer Science Series . McGraw-Hill New York"},{"key":"e_1_2_1_2_45_2","unstructured":"M\u00e9tayer C Abrial JR Voisin L (2005) Event-B language. RODIN Deliverable 3.2. rigorous open development environment for complex systems \u2013 RODIN"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Miarka R Boiten EA Derrick J (2000) Guards preconditions and refinement in Z. In: ZB 2000 [BDGK00] pp 286\u2013303","DOI":"10.1007\/3-540-44525-0_17"},{"key":"e_1_2_1_2_47_2","unstructured":"Milner AJRG (1971) An algebric definition of simulation between programs. In: Procceedings of 2nd Joint Conference on Artificial Intelligence pp 481\u2013489"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00263649"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Prehn S Toetenel WJ (eds) (1991) VDM \u201991 \u2013 Formal software development 4th international symposium of VDM Europe Noordwijkerhout The Netherlands October 21\u201325 1991 Proceedings Vol 2: Tutorials vol 552 of Lecture Notes in Computer Science . Springer Berlin Heidelberg New York","DOI":"10.1007\/3-540-54834-3"},{"key":"e_1_2_1_2_51_2","unstructured":"Schneider S (2001) The B-Method \u2013 An introduction . Correctness of Computing Palgrave"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Stepney S Cooper D Woodcock JCP (1998) More powerful Z data refinement: pushing the state of the art in industrial refinement. In: ZUM \u201998 [BFH98] pp 284\u2013307","DOI":"10.1007\/978-3-540-49676-2_20"},{"key":"e_1_2_1_2_53_2","unstructured":"Stepney S Cooper D Woodcock JCP (2000) An electronic purse: specification refinement and proof. Technical Monograph PRG-126 . Oxford University Computing Laboratory Oxford"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Strulo B (1995) How firing conditions help inheritance. In: Bowen JP Hinchey MG (eds) ZUM \u201995: the Z formal specification notation 9th international conference of Z users limerick Ireland September 7\u20139 1995 vol 967 of Lecture Notes in Computer Science . Springer Berlin Heidelberg New York pp 264\u2013275","DOI":"10.1007\/3-540-60271-2_125"},{"key":"e_1_2_1_2_55_2","unstructured":"Toyn I (ed) (1999) Z notation: final committee Draft CD 13568.2. Z Standards Panel"},{"key":"e_1_2_1_2_56_2","unstructured":"Woodcock JCP Davies J (1996) Using Z: specification refinement and proof . Prentice Hall New Jersey"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Woodcock JCP Morgan CC (1990) Refinement of State-Based Concurrent Systems. In: VDM \u201990 [NHL90] pp 340\u2013351","DOI":"10.1007\/3-540-52513-0_18"},{"key":"e_1_2_1_2_58_2","unstructured":"Woodcock JCP (1991) An introduction to refinement in Z. In: VDM \u201991 (volume 2) [BT91b] pp 96\u2013117"},{"key":"e_1_2_1_2_59_2","unstructured":"Woodcock JCP (1991) The refinement calculus. In: VDM \u201991 (volume 2) [PTP91b] pp 80\u201395"},{"key":"e_1_2_1_2_60_2","unstructured":"Wordsworth JB (1992) Software development with Z \u2013 A practical approach to formal methods in software engineering. Internalional Computer Science Series . Addison-Wesley Reading"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-006-0006-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-006-0006-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-006-0006-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:50:02Z","timestamp":1641484202000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-006-0006-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,9]]},"references-count":60,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,9]]}},"alternative-id":["10.1007\/s00165-006-0006-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-006-0006-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,9]]}}}