research-article

Open access

The Least Conjunctive Refinement and Promotion in the Refinement Calculus

Author:

Brendan P. MahonyAuthors Info & Claims

Formal Aspects of Computing, Volume 11, Issue 1

Pages 75 - 105

https://doi.org/10.1007/s001650050037

Published: 01 September 1999 Publication History

PDF eReader

Abstract.

A syntactic calculation of Morgan's least conjunctive refinement operator for predicate transformers is developed. The operator is used to develop a general approach to lifting relational operators to predicate transformer operators. Predicate transformer versions of the relational conjunction and disjunction operators are considered in detail. The Z-based technique of program promotion is considered in a refinement calculus setting. A standard Z promotion example is recast in the refinement calculus.

Cited By

View all

Owe ORamezanifarkhani TFazeldehkordi E(2017)Hoare-Style Reasoning from Multiple ContractsIntegrated Formal Methods10.1007/978-3-319-66845-1_17(263-278)Online publication date: 27-Aug-2017
https://doi.org/10.1007/978-3-319-66845-1_17
Derrick JBoiten EDerrick JBoiten E(2014)PromotionRefinement in Z and Object-Z10.1007/978-1-4471-5355-9_6(151-172)Online publication date: 2014
https://doi.org/10.1007/978-1-4471-5355-9_6
Deutsch MHenson MReeves S(2003)Operation refinement and monotonicity in the schema calculusProceedings of the 3rd international conference on Formal specification and development in Z and B10.5555/1761968.1761977(103-126)Online publication date: 4-Jun-2003
https://dl.acm.org/doi/10.5555/1761968.1761977
Show More Cited By

Index Terms

The Least Conjunctive Refinement and Promotion in the Refinement Calculus

Index terms have been assigned to the content through auto-classification.

Recommendations

Refinement modal logic

In this paper we present refinement modal logic. A refinement is like a bisimulation, except that from the three relational requirements only 'atoms' and 'back' need to be satisfied. Our logic contains a new operator in addition to the standard box ...
Refinement Calculus: A Systematic Introduction
A refinement calculus for logic programs

Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Formal Aspects of Computing Volume 11, Issue 1

Sep 1999

105 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 September 1999

Published in FAC Volume 11, Issue 1

Author Tag

Keywords: Refinement calculus; Predicate transformers; Z; Promotion; Frame typing

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
44
Total Downloads

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

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Owe ORamezanifarkhani TFazeldehkordi E(2017)Hoare-Style Reasoning from Multiple ContractsIntegrated Formal Methods10.1007/978-3-319-66845-1_17(263-278)Online publication date: 27-Aug-2017
https://doi.org/10.1007/978-3-319-66845-1_17
Derrick JBoiten EDerrick JBoiten E(2014)PromotionRefinement in Z and Object-Z10.1007/978-1-4471-5355-9_6(151-172)Online publication date: 2014
https://doi.org/10.1007/978-1-4471-5355-9_6
Deutsch MHenson MReeves S(2003)Operation refinement and monotonicity in the schema calculusProceedings of the 3rd international conference on Formal specification and development in Z and B10.5555/1761968.1761977(103-126)Online publication date: 4-Jun-2003
https://dl.acm.org/doi/10.5555/1761968.1761977
Deutsch MHenson MReeves S(2003)Operation Refinement and Monotonicity in the Schema CalculusZB 2003: Formal Specification and Development in Z and B10.1007/3-540-44880-2_9(103-126)Online publication date: 27-May-2003
https://doi.org/10.1007/3-540-44880-2_9
Groves L(2002)Refinement and the Z Schema CalculusElectronic Notes in Theoretical Computer Science10.1016/S1571-0661(05)80486-470:3(70-93)Online publication date: Nov-2002
https://doi.org/10.1016/S1571-0661(05)80486-4
Dunne S(2002)Junctive Compositions of Specifications in Total and General CorrectnessElectronic Notes in Theoretical Computer Science10.1016/S1571-0661(05)80480-370:3(4-20)Online publication date: Nov-2002
https://doi.org/10.1016/S1571-0661(05)80480-3
Groves L(2000)A formal approach to program modificationProceedings Seventh Asia-Pacific Software Engeering Conference. APSEC 200010.1109/APSEC.2000.896709(274-281)Online publication date: 2000
https://doi.org/10.1109/APSEC.2000.896709
Hesselink W(1999)Predicate Transformers for Recursive Procedures with Local VariablesFormal Aspects of Computing10.1007/s00165997000211:6(616-636)Online publication date: 1-Dec-1999
https://dl.acm.org/doi/10.1007/s001659970002

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

Index Terms

Recommendations

Refinement modal logic

Refinement Calculus: A Systematic Introduction

A refinement calculus for logic programs

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