research-article

A simple refinement-based method for constructing algorithms

Author:

Dominique MéryAuthors Info & Claims

ACM SIGCSE Bulletin, Volume 41, Issue 2

Pages 51 - 59

https://doi.org/10.1145/1595453.1595462

Published: 25 June 2009 Publication History

Get Access

Abstract

The Event B modelling language provides a framework for teaching programming methodology based on the famous pre/post-specifications, together with the refinement. We illustrate the call-as-event pattern for helping users to use Event B. As teacher, we are using students to evaluate our methodology and we give comments in italic, when we have got reactions from our students: a given definition, a concept related to our methodology, for instance. We discuss points related to our lectures at different levels of the university, mainly master. Simple case studies illustrate the teaching methodology based on interactive proofs.

References

[1]

Abrial, J.-R. The B book - Assigning Programs to Meanings. Cambridge University Press, 1996.

Digital Library

Google Scholar

[2]

Abrial, J.-R. B#: Toward a synthesis between Z and B. In 3nd International Conference of B and Z Users - ZB 2003, Turku, Finland (June 2003), D. Bert and M. Walden, Eds., Lectures Notes in Computer Science, Springer.

Digital Library

Google Scholar

[3]

Abrial, J.-R. Event based sequential program development: Application to constructing a pointer program. In Fme 2003 (2003), pp. 51--74.

Google Scholar

[4]

Abrial, J.-R., and Cansell, D. Click'n prove: Interactive proofs within set theory. In Tphol 2003 (2003), pp. 1--24.

Google Scholar

[5]

Back, R. On correct refinement of programs. Journal of Computer and System Sciences 23, 1 (1979), 49--68.

Google Scholar

[6]

Cansell, D., and Mery, D. The event-B Modelling Method: Concepts and Case Studies. Springer, 2007, pp. 33--140. See {?}.

Google Scholar

[7]

Cansell, D., and Mery, D. Proved-patterns-based development for structured programs. In CSR (2007), V. Diekert, M.V. Volkov, and A. Voronkov, Eds., vol. 4649 of Lecture Notes in Computer Science, Springer, pp. 104--114.

Digital Library

Google Scholar

[8]

Dijkstra, E.W. A Discipline of Programming. Prentice-Hall, 1976.

Digital Library

Google Scholar

[9]

Gentzen, G. Untersuchungen Uber das Logische Schliessen ou Recherches sur la d&#233;duction loqique. 1955. Traduction de Feys et Ladriere.

Google Scholar

[10]

Hoare, C.A.R. An axiomatic basis for computer programming. Commun. ACM 12 (1969), 576--580.

Digital Library

Google Scholar

[11]

Leavens, G.T., Abrial, J.-R., Batory, D., Butler, M., Coglio, A., Fisler, K., Hehner, E., Jones, C., Miller, D., Peyton-Jones, S., Sitaraman, M., Smith, D.R., and Stump, A. Roadmap for enhanced languages and methods to aid verification. In Fifth Intl. Conf. Generative Programming and Component Engineering (GPCE 2006) (Oct. 2006), ACM, pp. 221--235.

Digital Library

Google Scholar

[12]

Morgan, C. Programming from Specifications. Prentice Hall International Series in Computer Science. Prentice Hall, 1990.

Digital Library

Google Scholar

[13]

Mery, D. Teaching programming methodology using event b. In The B Method: from Research to Teaching (June 2008), H. Habrias, Ed.

Google Scholar

[14]

Project Rodin. Rigorous open development environment for complex systems. http://rodin-b-sharp.sourceforge.net/, 2004. 2004-2007.

Google Scholar

Cited By

View all

Zhumagambetov R(2021)Teaching Formal Methods in Academia: A Systematic Literature ReviewFormal Methods – Fun for Everybody10.1007/978-3-030-71374-4_12(218-226)Online publication date: 11-Mar-2021
https://doi.org/10.1007/978-3-030-71374-4_12
Cheng ZMéry DMonahan R(2016)On Two Friends for Getting Correct ProgramsLeveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques10.1007/978-3-319-47166-2_57(821-838)Online publication date: 5-Oct-2016
https://doi.org/10.1007/978-3-319-47166-2_57
Méry DSingh N(2014)Event BFormal Methods Applied to Complex Systems10.1002/9781119002727.ch10(253-298)Online publication date: 22-Jul-2014
https://doi.org/10.1002/9781119002727.ch10
Show More Cited By

Index Terms

A simple refinement-based method for constructing algorithms
1. Theory of computation

Recommendations

Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
Refinement-Based Verification of Interactive Real-Time Systems

Formal specification provides a system description that is much more precise than the natural language one and it can help to solve a lot of specification problems. But even a formal specification of a system can contain mistakes or can disagree with ...
A refinement-based compiler development for synchronous languages
MEMOCODE '17: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design

In this paper, we are concerned by the elaboration of generic development steps for the code generation for synchronous languages. Our aim is to provide a correct by construction solution. For that purpose, we adopt a refinement-based approach where ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGCSE Bulletin Volume 41, Issue 2

June 2009

166 pages

ISSN:0097-8418

DOI:10.1145/1595453

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 June 2009

Published in SIGCSE Volume 41, Issue 2

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
122
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Zhumagambetov R(2021)Teaching Formal Methods in Academia: A Systematic Literature ReviewFormal Methods – Fun for Everybody10.1007/978-3-030-71374-4_12(218-226)Online publication date: 11-Mar-2021
https://doi.org/10.1007/978-3-030-71374-4_12
Cheng ZMéry DMonahan R(2016)On Two Friends for Getting Correct ProgramsLeveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques10.1007/978-3-319-47166-2_57(821-838)Online publication date: 5-Oct-2016
https://doi.org/10.1007/978-3-319-47166-2_57
Méry DSingh N(2014)Event BFormal Methods Applied to Complex Systems10.1002/9781119002727.ch10(253-298)Online publication date: 22-Jul-2014
https://doi.org/10.1002/9781119002727.ch10
Méry DMosbah MTounsi M(2011)Refinement-based verification of local synchronization algorithmsProceedings of the 17th international conference on Formal methods10.5555/2021296.2021332(338-352)Online publication date: 20-Jun-2011
https://dl.acm.org/doi/10.5555/2021296.2021332
Méry DMosbah MTounsi M(2011)Refinement-Based Verification of Local Synchronization AlgorithmsFM 2011: Formal Methods10.1007/978-3-642-21437-0_26(338-352)Online publication date: 2011
https://doi.org/10.1007/978-3-642-21437-0_26

View Options

Login options

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

Cited By

Index Terms

Recommendations

Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

Refinement-Based Verification of Interactive Real-Time Systems

A refinement-based compiler development for synchronous languages