research-article

Open access

ArcAngel: a Tactic Language for Refinement

Authors:

Marcel Oliveira,

Ana Cavalcanti,

Jim WoodcockAuthors Info & Claims

Formal Aspects of Computing, Volume 15, Issue 1

Pages 28 - 47

https://doi.org/10.1007/s00165-003-0003-8

Published: 01 July 2003 Publication History

PDF eReader

Abstract.

Morgan's refinement calculus is a successful technique for developing software in a precise and consistent way. This technique, however, can be hard to use, as developments may be long and repetitive. Many authors have pointed out that a lot can be gained by identifying commonly used development strategies, documenting them as tactics, and using them as single transformation rules. Also, it is useful to have a notation for describing derivations, so that they can be analysed and modified. In this paper, we present ArcAngel, a language for defining such refinement tactics; we present the language, its semantics, and some of its algebraic laws. Apart from Angel, a general-purpose tactic language that we are extending, no other tactic language has a denotational semantics and proof theory of its own.

Cited By

View all

Ribeiro PYe KZeyda FMiyazawa A(2024)A Tour Through the Programming Choices: Semantics and ApplicationsThe Application of Formal Methods10.1007/978-3-031-67114-2_11(261-305)Online publication date: 1-Sep-2024
https://doi.org/10.1007/978-3-031-67114-2_11
Bordis TRunge TSchultz DSchaefer I(2022)Family-Based and Product-Based Development of Correct-by-Construction Software Product LinesJournal of Computer Languages10.1016/j.cola.2022.10111970(101119)Online publication date: Jun-2022
https://doi.org/10.1016/j.cola.2022.101119
Bordis TKodetzki MRunge TSchaefer I(2022)VarCorC: Developing Object-Oriented Software Product Lines Using Correctness-by-ConstructionSoftware Engineering and Formal Methods. SEFM 2022 Collocated Workshops10.1007/978-3-031-26236-4_13(156-163)Online publication date: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-26236-4_13
Show More Cited By

Recommendations

A tactic language for refinement of state-rich concurrent specifications

Circus is a refinement language in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and calculus are distinctive, but since refinements may be long and repetitive,...
Supporting ArcAngel in ProofPower

ArcAngel is a specialised tactic language devised to facilitate and automate program developments using Morgan's refinement calculus. It is especially well-suited for the specification of high-level strategies to derive programs by construction, and ...
A simple refinement language for CASL
WADT'04: Proceedings of the 17th international conference on Recent Trends in Algebraic Development Techniques

We extend Casl architectural specifications with a simple refinement language that allows the formalization of developments as refinement trees. The essence of the extension is to allow refinements of unit specifications in Casl architectural ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Formal Aspects of Computing Volume 15, Issue 1

Jul 2003

99 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 July 2003

Published in FAC Volume 15, Issue 1

Author Tag

ensp; Formal methods; Program development; Refinement calculus

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
54
Total Downloads

Downloads (Last 12 months)39
Downloads (Last 6 weeks)5

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ribeiro PYe KZeyda FMiyazawa A(2024)A Tour Through the Programming Choices: Semantics and ApplicationsThe Application of Formal Methods10.1007/978-3-031-67114-2_11(261-305)Online publication date: 1-Sep-2024
https://doi.org/10.1007/978-3-031-67114-2_11
Bordis TRunge TSchultz DSchaefer I(2022)Family-Based and Product-Based Development of Correct-by-Construction Software Product LinesJournal of Computer Languages10.1016/j.cola.2022.10111970(101119)Online publication date: Jun-2022
https://doi.org/10.1016/j.cola.2022.101119
Bordis TKodetzki MRunge TSchaefer I(2022)VarCorC: Developing Object-Oriented Software Product Lines Using Correctness-by-ConstructionSoftware Engineering and Formal Methods. SEFM 2022 Collocated Workshops10.1007/978-3-031-26236-4_13(156-163)Online publication date: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-26236-4_13
Runge TKittelmann AServetto MPotanin ASchaefer I(2022)Information Flow Control-by-Construction for an Object-Oriented LanguageSoftware Engineering and Formal Methods10.1007/978-3-031-17108-6_13(209-226)Online publication date: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-17108-6_13
Bordis TCleophas LKittelmann ARunge TSchaefer IWatson B(2022)Re-CorC-ing KeY: Correct-by-Construction Software Development Based on KeYThe Logic of Software. A Tasting Menu of Formal Methods10.1007/978-3-031-08166-8_5(80-104)Online publication date: 4-Jul-2022
https://doi.org/10.1007/978-3-031-08166-8_5
Bordis TRunge TSchaefer IErwig MGray J(2020)Correctness-by-construction for feature-oriented software product linesProceedings of the 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3425898.3426959(22-34)Online publication date: 16-Nov-2020
https://dl.acm.org/doi/10.1145/3425898.3426959
Bordis TRunge TKnüppel AThüm TSchaefer I(2020)Variational correctness-by-constructionProceedings of the 14th International Working Conference on Variability Modelling of Software-Intensive Systems10.1145/3377024.3377038(1-9)Online publication date: 5-Feb-2020
https://dl.acm.org/doi/10.1145/3377024.3377038
Knüppel ARunge TSchaefer I(2020)Scaling Correctness-by-ConstructionLeveraging Applications of Formal Methods, Verification and Validation: Verification Principles10.1007/978-3-030-61362-4_10(187-207)Online publication date: 20-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-61362-4_10
Ribeiro PCavalcanti A(2019)Angelic processes for CSP via the UTPTheoretical Computer Science10.1016/j.tcs.2018.10.008756(19-63)Online publication date: Jan-2019
https://doi.org/10.1016/j.tcs.2018.10.008
Runge TThüm TCleophas LSchaefer IWatson B(2019)Comparing Correctness-by-Construction with Post-Hoc Verification—A Qualitative User StudyFormal Methods. FM 2019 International Workshops10.1007/978-3-030-54997-8_25(388-405)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-54997-8_25
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract.

Cited By

Recommendations

A tactic language for refinement of state-rich concurrent specifications

Supporting ArcAngel in ProofPower

A simple refinement language for CASL

Comments

Information

Published In

Publisher

Publication History

Author Tag

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Share

Share this Publication link

Share on social media

Affiliations