RODIN

In B, it is possible to write sequential code such as (The B-Book p. 400)

WHILE x > 0 DO
  x := x - 1
END

Is this syntax possible in Event-B, if not, are there alternatives?

Regards,
Konstantin Weitz

Re: [Rodin-b-sharp-user] Sequencing and Loops in Event-B From: Hoang, Thai Son <htson@in...> - 2013-01-21 09:59 Dear Konstantin, On 19 Jan 2013, at 00:52, Konstantin Weitz <weitzkon@...> wrote: > In B, it is possible to write sequential code such as (The B-Book p. 400) > > WHILE x > 0 DO > x := x - 1 > END > > Is this syntax possible in Event-B, if not, are there alternatives? Event-B is more general purpose (and simpler) modelling method than B. Hence it is not only to model sequential programs, but also other type of systems, e.g., distributed one. There is no sequential code like WHILE loop in Event-B. Instead, it can usually be modelled using two events: body WHEN x > 0 THEN x := x - 1 END finish WHEN not(x > 0) THEN // do something after the loop END You can find more information about using Event-B to model sequential programs from chapter 15 of Jean-Raymond's Event-B book. The slides for that chapter are available on-line. http://wiki.event-b.org/index.php/Event-B_Language Cheers, Son

Re: [Rodin-b-sharp-user] Sequencing and Loops in Event-B From: Dipak Chaudhari <dipakc@gm...> - 2013-01-21 10:38 Attachments: Message as HTML      You may also find the following papers useful. Hallerstede, S., and M. Leuschel. “Experiments in Program Verification Using Event-B.” Formal Aspects of Computing 24, no. 1 (2012): 97–125. Hallerstede, Stefan. “Structured Event-B Models and Proofs.” In Abstract State Machines, Alloy, B and Z, edited by Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau, and Steve Reeves, 5977:273–286. Lecture Notes in Computer Science. Springer Berlin / Heidelberg, 2010. http://dx.doi.org/10.1007/978-3-642-11811-1_21. Boström, P. “Creating Sequential Programs from Event-B Models.” In Integrated Formal Methods, 74–88, 2010. http://www.springerlink.com/index/W087U6N4VM4135U0.pdf. Regards, Dipak On Mon, Jan 21, 2013 at 3:29 PM, Hoang, Thai Son <htson@...> wrote: > DO

2 messages have been excluded from this view by a project administrator.