{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,15]],"date-time":"2025-03-15T15:10:08Z","timestamp":1742051408698,"version":"3.38.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>ArcAngel is a tactic language devised to facilitate and automate program developments using Morgan\u2019s refinement calculus. It is especially well suited for the specification of high-level refinement strategies, and equipped with a formal semantics that additionally permits reasoning about tactics. In this paper, we present an implementation of ArcAngel for the ProofPower theorem prover. We discuss the underlying design, explain how it implements the semantics of ArcAngel, and examine the interplay between ArcAngel tactics and the native reasoning support of the prover. We also discuss several extensions of ArcAngel that have been entailed by our implementation effort. They are of practical importance and provide a unification of the related tactic languages Angel and ArcAngel<jats:italic>C<\/jats:italic>. Our main result is a mechanisation that reflects directly the ArcAngel semantics, and can be used with any programming model for refinement. The approach can be used to support other formal tactic languages using other theorem provers.<\/jats:p>","DOI":"10.1007\/s00165-011-0218-z","type":"journal-article","created":{"date-parts":[[2011,12,12]],"date-time":"2011-12-12T12:52:30Z","timestamp":1323694350000},"page":"127-160","source":"Crossref","is-referenced-by-count":5,"title":["Mechanised support for sound refinement tactics"],"prefix":"10.1145","volume":"24","author":[{"given":"Frank","family":"Zeyda","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of York, Heslington, York, UK"}]},{"given":"Marcel","family":"Oliveira","sequence":"additional","affiliation":[{"name":"Departamento de Inform\u00e1tica e Matem\u00e1tica Aplicada, Universidade Federal do Rio Grande do Norte, Natal, Brazil"}]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of York, Heslington, York, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/1855020"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Adams M Clayton P (2005) ClawZ: Cost-Effective Formal Verification of Control Systems. In: Formal Methods and Software Engineering. In: Lecture Notes in Computer Science vol 3785 Springer Berlin pp 465\u2013479","DOI":"10.1007\/11576280_32"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Arthan R Caseley P O\u2019Halloran C Smith A (2000) ClawZ: control laws in Z. In: 3 rd International Conference on Formal Engineering Methods. IEEE Computer Society Digital Library pp 169\u2013176","DOI":"10.1109\/ICFEM.2000.873817"},{"key":"e_1_2_1_2_5_2","unstructured":"Arthan R Jones RB (2005) Z in HOL in ProofPower. FACS FACTS 2005:39\u201355 http:\/\/www.bcs.org\/upload\/pdf\/facts200503-compressed.pdf"},{"key":"e_1_2_1_2_6_2","unstructured":"Back R-J (1987) Procedural Abstraction in the Refinement Calculus. Technical Report Ser. A No 55 Department of Computer Science \u00c5bo Akademie Finland"},{"key":"e_1_2_1_2_7_2","unstructured":"Butler M Grundy J L\u00e5ngbacka T Ruk\u0161e\u0331nas R von Wright J (1997) The Refinement Calculator: Proof Support for Program Refinement. In: Formal Methods Pacific\u201997: Proceedings of the FMP\u201997 Springer Berlin pp 40\u201361"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Cavalcanti ALC Clayton P (2006) Verification of Control Systems using Circus. In: Proceedings of the 11th IEEE International Conference on Engineering of Complex Computer Systems IEEE Computer Society pp 269\u2013278","DOI":"10.1109\/ICECCS.2006.1690376"},{"key":"e_1_2_1_2_9_2","unstructured":"Carrington D Hayes I Nickson R Watson G Welsh J (1994) A Review of Existing Refinement Tools. Technical Report UQ-SVRC-94-8 Software Verification Research Centre University of Queensland Australia"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050006"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Clayton P O\u2019Halloran C (2006) Using the Compliance Notation in Industry. In: Refinement Techniques in Software Engineering. Lecture Notes in Computer Science vol 3167. Springer Berlin pp 269\u2013314","DOI":"10.1007\/11889229_7"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050016"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0001-8"},{"key":"e_1_2_1_2_14_2","unstructured":"Dijkstra EW (1976) A Discipline of Programming. Series in Automatic Computation. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Groves L Nickson R Utting M (1992) A tactic driven refinement tool. In: Proceedings of the 5th Refinement Workshop organised by BCS-FACS. Springer January 1992 pp 272\u2013297. Available as a technical report at http:\/\/www.mcs.vuw.ac.nz\/comp\/Publications\/CS-TR-92-5.abs.html","DOI":"10.1007\/978-1-4471-3550-0_14"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80486-4"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Grundy J (1992) A Window Inference Tool for Refinement. In: Proceedings of the 5th Refinement Workshop Workshops in Computing. BCS FACS Springer pp 230\u2013254","DOI":"10.1007\/978-1-4471-3550-0_12"},{"key":"e_1_2_1_2_18_2","unstructured":"Hoare CAR He Jifeng (1998) Unifying Theories of Programming. Prentice Hall Series in Computer Science. Prentice Hall Englewood Cliffs"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Iliasov A Troubitsyna E Laibinis L Romanovsky A (2010) Patterns for Refinement Automation. In: Formal Methods for Components and Objects. Lecture Notes in Computer Science vol 6286. Springer Berlin pp 70\u201388","DOI":"10.1007\/978-3-642-17071-3_4"},{"key":"e_1_2_1_2_20_2","unstructured":"Martin A (1994) Machine-Assisted Theorem Proving for Software Engineering. PhD thesis Oxford University Computing Laboratory Oxford UK (Technical Monograph PRG-121)"},{"key":"e_1_2_1_2_21_2","unstructured":"Martin A (1996) Infinite lists for specifying functional programs in Z. In: Proceedings of Fifth Australasian Refinement Workshop. University of Queensland Australia"},{"key":"e_1_2_1_2_22_2","unstructured":"Martin A Gardiner P Woodcock J (1993) Tactic Semantics and Reasoning. Technical report Oxford University Computing Laboratory Oxford UK"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01213535"},{"key":"e_1_2_1_2_24_2","unstructured":"Martin A Nickson R Utting M (1997) A tactic language for Ergo. In: Formal Methods\u2014Pacific 97 Discrete Mathematics and Theoretical Computer Science pp 186\u2013207"},{"key":"e_1_2_1_2_25_2","unstructured":"Martin A Nickson R Utting M (1997) Improving Angel\u2019s Parallel Operator: Gumtree\u2019s Approach. Technical Report UQ-SVRC-97-15 Software Verification Centre School of Information Technology University of Queensland Australia"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_2_27_2","unstructured":"Morgan CC (1998) Programming from Specifications. Prentice Hall International Series in Computer Science. Prentice Hall Englewood Cliffs"},{"volume-title":"The Definition of Standard ML","year":"1990","author":"Milner R","key":"e_1_2_1_2_28_2"},{"key":"e_1_2_1_2_29_2","unstructured":"Nickson R (1994) Tool Support for the Refinement Calculus. PhD thesis Victoria University of Wellington"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.010"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0003-8"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Oliveira MVM Cavalcanti ALC Woodcock J (2006) Unifying theories in ProofPower-Z. In: Unifying Theories of Programming First International Symposium. Lecture Notes in Computer Science vol 4010. Springer Berlin pp 123\u2013140","DOI":"10.1007\/11768173_8"},{"key":"e_1_2_1_2_33_2","unstructured":"Oliveira MVM Cavalcanti ALC Woodcock J (2007) A UTP semantics for Circus. Form Asp Comput (online first)"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Oliveira MVM Xavier M Cavalcanti ALC (2004) Refine and Gabriel: support for refinement and tactics. In: Proceedings of the Second International Conference on Software Engineering and Formal Methods. IEEE Computer Society pp 310\u2013319","DOI":"10.1109\/SEFM.2004.1347535"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.11.012"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.5555\/524580"},{"key":"e_1_2_1_2_37_2","unstructured":"Event-B and the RODIN Platform. http:\/\/www.event-b.org\/"},{"key":"e_1_2_1_2_38_2","unstructured":"Roscoe AW (1998) The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.2307\/2268577"},{"key":"e_1_2_1_2_40_2","unstructured":"Utting M Whitwell K (1994) Ergo user manual\u2014an interactive theorem prover"},{"key":"e_1_2_1_2_41_2","unstructured":"Vickers T Gardiner P (1994) A Language of Refinements. Technical Report TR-CS-94-05 Computer Science Department Australian National University"},{"key":"e_1_2_1_2_42_2","unstructured":"Vickers T (1990) An overview of a refinement editor. In: Proceedings of the Fith Australian Software Engineering Conference pp 39\u201344"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Vernon M Zeyda F Cavalcanti ALC (2010) Communication Systems in ClawZ. In: Abstract State Machines Alloy B and Z. Lecture Notes in Computer Science vol 5977. Springer-Verlag Berlin pages 334 \u2013 348","DOI":"10.1007\/978-3-642-11811-1_25"},{"key":"e_1_2_1_2_44_2","unstructured":"Woodcock J Davies J (1996) Using Z: Specification Refinement and Proof. International Series in Computer Science. Prentice Hall Englewood Cliffs"},{"key":"e_1_2_1_2_45_2","unstructured":"Wright J (1994) Program refinement by theorem prover. In: Proceedings Of the 6th Refinement Workshop organised by BCS-FACS. Springer Berlin"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.05.055"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Zeyda F Cavalcanti A (2011) Automating Refinement of Circus Programs. In: Formal Methods: Foundations and Applications Lecture Notes in Computer Science vol 6527. Springer Berlin pp 274\u2013290","DOI":"10.1007\/978-3-642-19829-8_18"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Zeyda F Cavalcanti A (2008) Encoding Circus Programs in ProofPower-Z. In: Unifying Theories of Programming 2nd International Symposium. Lecture Notes in Computer Science vol 5713. Springer Berlin pp 218\u2013237","DOI":"10.1007\/978-3-642-14521-6_13"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Zeyda F Cavalcanti ALC (2010) Mechanical reasoning about families of UTP Theories. Sci Comput Program. doi:10.1016\/j.scico.2010.02.010","DOI":"10.1016\/j.entcs.2009.05.055"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.12.027"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0218-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0218-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0218-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,15]],"date-time":"2025-03-15T14:45:40Z","timestamp":1742049940000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0218-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1]]},"references-count":50,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["10.1007\/s00165-011-0218-z"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0218-z","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2012,1]]}}}