B-ASM: Specification of ASM à la B

David Michel 0001, Frédéric Gervais, Pierre Valarcher
Digital Printed Abstract View Cite
Type
Short Paper
Publication
2nd International Conference on ASM, Alloy, B, and Z (ABZ'10)

Abstract

We aim at extending the B language in order to build ASM programs which are correct with respect to B-like logical specifications. On the one hand, the main strengths of the B formal method are: i) the ability to express logical statements, and ii) the construction of a correct implementation by refinement. On the other hand, from our viewpoint, the striking aspects of ASM are the non-bounded outer loop that can reach the fixed point of a program and the power to express naturally any kind of (sequential) algorithms.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{MichelGV10,
  author       = {David Michel and
                  Fr{\'{e}}d{\'{e}}ric Gervais and
                  Pierre Valarcher},
  editor       = {Marc Frappier and
                  Uwe Gl{\"{a}}sser and
                  Sarfraz Khurshid and
                  R{\'{e}}gine Laleau and
                  Steve Reeves},
  title        = {{B-ASM:} Specification of {ASM} {\`{a}} la {B}},
  booktitle    = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
                  {ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5977},
  pages        = {391},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-11811-1\_29},
  doi          = {10.1007/978-3-642-11811-1\_29},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/MichelGV10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'10

Related