You can subscribe to this list here.
2009 
_{Jan}
(10) 
_{Feb}
(57) 
_{Mar}
(16) 
_{Apr}
(15) 
_{May}
(31) 
_{Jun}
(17) 
_{Jul}
(10) 
_{Aug}
(18) 
_{Sep}
(20) 
_{Oct}
(31) 
_{Nov}
(6) 
_{Dec}
(7) 

2010 
_{Jan}
(21) 
_{Feb}
(40) 
_{Mar}
(35) 
_{Apr}
(14) 
_{May}
(21) 
_{Jun}
(6) 
_{Jul}
(33) 
_{Aug}
(97) 
_{Sep}
(55) 
_{Oct}
(37) 
_{Nov}
(35) 
_{Dec}
(23) 
2011 
_{Jan}
(9) 
_{Feb}
(9) 
_{Mar}
(57) 
_{Apr}
(21) 
_{May}
(4) 
_{Jun}
(6) 
_{Jul}
(12) 
_{Aug}
(13) 
_{Sep}
(18) 
_{Oct}
(9) 
_{Nov}
(11) 
_{Dec}
(3) 
2012 
_{Jan}
(45) 
_{Feb}
(18) 
_{Mar}
(18) 
_{Apr}
(14) 
_{May}
(11) 
_{Jun}
(14) 
_{Jul}
(3) 
_{Aug}
(6) 
_{Sep}
(2) 
_{Oct}
(16) 
_{Nov}
(31) 
_{Dec}
(10) 
2013 
_{Jan}
(29) 
_{Feb}
(7) 
_{Mar}
(21) 
_{Apr}
(52) 
_{May}
(32) 
_{Jun}
(8) 
_{Jul}
(9) 
_{Aug}
(9) 
_{Sep}
(7) 
_{Oct}
(22) 
_{Nov}
(12) 
_{Dec}

2014 
_{Jan}
(36) 
_{Feb}
(11) 
_{Mar}
(11) 
_{Apr}
(18) 
_{May}
(8) 
_{Jun}
(19) 
_{Jul}
(15) 
_{Aug}
(22) 
_{Sep}
(11) 
_{Oct}
(8) 
_{Nov}
(4) 
_{Dec}
(14) 
2015 
_{Jan}
(2) 
_{Feb}
(4) 
_{Mar}
(10) 
_{Apr}
(7) 
_{May}
(11) 
_{Jun}
(17) 
_{Jul}
(5) 
_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 






1

2

3

4

5

6

7
(4) 
8

9

10

11
(3) 
12
(5) 
13
(3) 
14

15

16
(4) 
17

18
(2) 
19

20
(3) 
21
(1) 
22

23

24

25

26
(1) 
27
(2) 
28
(3) 
29

30

31







From: Laurent Voisin <laurent.voisin@sy...>  20090528 09:35:27

Hi Jeremy, Le 26 mai 09 à 19:06, Jeremy Bryans a écrit : > In the editor views of Rodin, some of the mathematical symbols come > out as dingbats. > I've attached a screen shot, where act1 should is bignullmap <+ W > > LANG is set to en_GB.UTF8. > > I am running version 0.9.2.1 on Ubuntu. This is because the prettyprint tab actually embeds an external Web browser (the B model is rendered as HTML and opened in the browser). To get proper display of some characters, you have to install the "Brave Sans Mono" font on your computer. The font is available from the Download page on SourceForge: http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181717 Once the font has been installed in your Operating System, everything should display correctly. Laurent. 
From: Laurent Voisin <laurent.voisin@sy...>  20090528 09:09:49

Dear Jonathan, Le 27 mai 09 à 20:39, Jonathan S. Ostroff a écrit : > I am using Rodin 0.9.2.1 (the latest) and Atelier 0.8.4 under > Windows/Vista. > I was trying to import a *.zip project that was apparently developed > with a > later version of the provers, and I obtained import errors (e.g. > "Error > while running tool (Automatic Proof Obligation Manager) gen_hotel_new > hotel_new_4.bpo Unknown"). > > When I tried to update the Atelier software from Eclipse I got the > error > below. > > Any help on how to update my Rodin system would be very much > appreciated. Unfortunately, there is not much that you can do now. We're in the process of publishing a new release of Rodin that will be compatible with JeanRaymond's model. A first release candidate is expected for this weekend. So, please wait for next week. Laurent. 
From: Laurent Voisin <laurent.voisin@sy...>  20090528 09:02:36

Jeremy, Le 27 mai 09 à 13:16, Jeremy Bryans a écrit : > http://wiki.eventb.org/index.php/ASCII_Representations_of_the_Mathematical_Symbols_(Rodin_User_Manual) > > states that >> is the ascii representation of a total surjective > function, but my I find that typing >> produces the correct symbol, > while >> produces a dash followed by the correct symbol. > > Similarly, +>> gives a symbol for a partial srujective function, > rather than +>>. This was a mistake in the wiki. Also note that the ASCII shortcuts are directly available in the Rodin platform. To display them, click "Help > Dynamic Help", then in the help window, click "All Topics" in the bottom. Finally, select "EventB Keyboard User Guide > Getting Started > Special Combos". This will display all the ASCII shortcuts for the mathematical symbols. IMPORTANT NOTE: There is a defect with Rodin 0.9.2.1 which prevents the images of math symbols to appear. This has been fixed since and will be available in Rodin 1.0.0 to come very soon. Laurent. 
From: Jonathan S. Ostroff <jonathan@yo...>  20090527 18:46:13

I am using Rodin 0.9.2.1 (the latest) and Atelier 0.8.4 under Windows/Vista. I was trying to import a *.zip project that was apparently developed with a later version of the provers, and I obtained import errors (e.g. "Error while running tool (Automatic Proof Obligation Manager) gen_hotel_new hotel_new_4.bpo Unknown"). When I tried to update the Atelier software from Eclipse I got the error below. Any help on how to update my Rodin system would be very much appreciated. Jonathan ================================== Cannot complete the install because some dependencies are not satisfiable Unsatisfied dependency: [com.clearsy.atelierb.provers.feature.group 1.0.0] requiredCapability: org.eclipse.equinox.p2.iu/org.eventb.ide.feature.group/[1.0.0,2.0.0) Cannot find a solution where both "org.eventb.ide.feature.group [0.9.2.1]" and "org.eventb.ide.feature.group [1.0.0,2.0.0)" are satisfied. Cannot find a solution where both "org.eventb.ide.feature.group [0.9.2.1]" and "org.eventb.ide.feature.group [1.0.0,2.0.0)" are satisfied. Cannot find a solution where both "org.eventb.ide.feature.group [0.9.2.1]" and "org.eventb.ide.feature.group [1.0.0,2.0.0)" are satisfied. Cannot find a solution where both "org.eventb.ide.feature.group [0.9.2.1]" and "org.eventb.ide.feature.group [1.0.0,2.0.0)" are satisfied. Cannot find a solution where both "org.eventb.ide.feature.group [0.9.2.1]" and "org.eventb.ide.feature.group [1.0.0,2.0.0)" are satisfied. Cannot find a solution where both "org.eventb.ide.feature.group [0.9.2.1]" and "org.eventb.ide.feature.group [1.0.0,2.0.0)" are satisfied. Unsatisfied dependency: [com.clearsy.atelierb.provers.feature.group 1.0.0] requiredCapability: org.eclipse.equinox.p2.iu/org.eventb.ide.feature.group/[1.0.0,2.0.0) Unsatisfied dependency: [com.clearsy.atelierb.provers.feature.group 1.0.0] requiredCapability: org.eclipse.equinox.p2.iu/org.eventb.ide.feature.group/[1.0.0,2.0.0) Unsatisfied dependency: [org.eclipse.platform.feature.group 3.4.1.r341_v200807319I96EiDElYevwzp1bP5zNlAaP7vtX6Utotqsu] requiredCapability: org.eclipse.equinox.p2.iu/org.eclipse.debug.core/[3.4.0.v20080612,3.4.0.v200 80612] Unsatisfied dependency: [org.eclipse.platform.feature.group 3.4.1.r341_v200807319I96EiDElYevwzp1bP5zNlAaP7vtX6Utotqsu] requiredCapability: org.eclipse.equinox.p2.iu/org.eclipse.help.feature.group/[1.0.1.R34x_v200808 277r7xEIxEI6Zu5nEqN7M3UBpglaat,1.0.1.R34x_v200808277r7xEIxEI6Zu5nEqN7M3UBp glaat] Unsatisfied dependency: [org.rodinp.platform.feature.group 0.9.2.1] requiredCapability: org.eclipse.equinox.p2.iu/org.eclipse.platform.feature.group/[3.4.1.r341_v20 0807319I96EiDElYevwzp1bP5zNlAaP7vtX6Utotqsu,3.4.1.r341_v200807319I96EiDE lYevwzp1bP5zNlAaP7vtX6Utotqsu] Unsatisfied dependency: [org.rodinp.platform.feature.group 0.9.2.1] requiredCapability: org.eclipse.equinox.p2.iu/org.rodinp.feature.group/[0.9.2,0.9.2] Unsatisfied dependency: [org.rodinp.feature.group 0.9.2] requiredCapability: org.eclipse.equinox.p2.iu/org.eclipse.platform.feature.group/[3.4.0,4.0.0) Unsatisfied dependency: [org.eclipse.rcp.feature.group 3.4.100.r341_v20080814989JESIEdAciFYfkZZsBfSwQ2341] requiredCapability: org.eclipse.equinox.p2.iu/org.eclipse.ui.workbench/[3.4.1.M200808270800a,3. 4.1.M200808270800a] Unsatisfied dependency: [ac.soton.eventb.latex.feature.feature.group 0.5.0] requiredCapability: org.eclipse.equinox.p2.iu/org.eventb.ide.feature.group/0.0.0 Unsatisfied dependency: [ac.soton.eventb.latex.feature.feature.group 0.5.0] requiredCapability: org.eclipse.equinox.p2.iu/org.eventb.ide.feature.group/0.0.0 Unsatisfied dependency: [org.rodinp.platform.product 0.9.2.1] requiredCapability: org.eclipse.equinox.p2.iu/org.eventb.ide.feature.group/[0.9.2.1,0.9.2.1] Unsatisfied dependency: [org.rodinp.platform.product 0.9.2.1] requiredCapability: org.eclipse.equinox.p2.iu/org.eventb.ide.feature.group/[0.9.2.1,0.9.2.1] Unsatisfied dependency: [org.rodinp.platform.product 0.9.2.1] requiredCapability: org.eclipse.equinox.p2.iu/org.rodinp.platform.feature.group/[0.9.2.1,0.9.2.1 ] Unsatisfied dependency: [org.eventb.ide.feature.group 0.9.2.1] requiredCapability: org.eclipse.equinox.p2.iu/org.rodinp.platform.feature.group/[0.9.2.1,1.0.0) Unsatisfied dependency: [org.eclipse.help.feature.group 1.0.1.R34x_v200808277r7xEIxEI6Zu5nEqN7M3UBpglaat] requiredCapability: org.eclipse.equinox.p2.iu/org.eclipse.rcp.feature.group/[3.4.100.r341_v20080 814989JESIEdAciFYfkZZsBfSwQ2341,3.4.100.r341_v20080814989JESIEdAciFYfkZZsB fSwQ2341] Original Message From: JeanRaymond Abrial [mailto:jabrial@...] Sent: Wednesday, May 27, 2009 1:18 PM To: jonathan@... Subject: Re: [Rodinbsharpuser] Hotel locking system Dear Jonathan, Yes, this is because I used the latest version. Have you access to the intermediate versions through SVN update? If not, ask Laurent how to get it. Then update your Rodin Platform and it will work, I suppose. Cheers, JR On May 27, 2009, at 7:00 PM, Jonathan S. Ostroff wrote: > Dear JeanRaymond, > > Thank you for sending us the hotel example which looks interesting. > > When I imported the hotel.zip Rodin stated that it cannot get the > children > of hotelnewctx and then showed the following errors. > > === > Severity and Description Path Resource Location > Creation time Id > Error while running tool (Automatic Proof Obligation Manager) > gen_hotel_new hotel_new_4.bpo Unknown 1243443347715 698 > Error while running tool (Automatic Proof Obligation Manager) > gen_hotel_new hotel_new_41.bpo Unknown 1243443347252 697 > Error while running tool (Context Static Checker) gen_hotel_new > hotel_new_ctx0.buc Unknown 1243443346056 696 > Error while running tool (Context Static Checker) gen_hotel_new > hotel_new_ctx1.buc Unknown 1243443346001 695 > Error while running tool (Context Static Checker) gen_hotel_new > hotel_new_ctx2.buc Unknown 1243443345643 694 > ====== > > Jonathan > > Original Message > From: JeanRaymond Abrial [mailto:jabrial@...] > Sent: Wednesday, May 27, 2009 1:45 AM > To: Hoang Lan Nguyen > Cc: Jonathan Ostroff > Subject: Re: [Rodinbsharpuser] Hotel locking system > > Dear Lan, > > Here is a set of slides where I presented Rodin but also the Hotel > system > (it starts at slide 46). > > Next is the complete hotel development. The order is: > > hotel_new_00 > hotel_new_0 > hotel_new_1 > hotel_new_2 > hotel_new_3 > > There are two alternative final refinements: hotel_new_4 and > hotel_new_41 > > >> Hi JeanRaymond, >> >> I've been wondering whether you're familiar with the "Hotel Locking >> System" (recordable locks), explained in the Alloy book by Daniel >> Jackson "Software abstractions: logic, language, and analysis". (a >> simple description of the system is attached). >> >> Regards, >> >> Lan > > 
From: Jeremy Bryans <jeremy.bryans@ne...>  20090527 11:16:51

All, http://wiki.eventb.org/index.php/ASCII_Representations_of_the_Mathematical_Symbols_(Rodin_User_Manual) states that >> is the ascii representation of a total surjective function, but my I find that typing >> produces the correct symbol, while >> produces a dash followed by the correct symbol. Similarly, +>> gives a symbol for a partial srujective function, rather than +>>. I suspect this may be related to my previous email about dingbats.. Any help appreciated, as always, cheers, Jeremy 
From: Jeremy Bryans <jeremy.bryans@ne...>  20090526 17:06:57

Hi all, In the editor views of Rodin, some of the mathematical symbols come out as dingbats. I've attached a screen shot, where act1 should is bignullmap <+ W LANG is set to en_GB.UTF8. I am running version 0.9.2.1 on Ubuntu. Many thanks for any help, Cheers, Jeremy 
From: Michael J Butler <mjb@ec...>  20090521 14:40:18

A reminder about the Rodin Developer Workshop in Southampton in July 2009: http://www.eventb.org/rodin09.html Note that we have now decided to hold a 1day tutorial on Rodin plugin development on 15 July just before the workshop. The tutorial is intended for existing and prospective plugin developers. It will give an overview of the architecture of Rodin and provide guidance on building plugins. ORGANISERS: Michael Butler, University of Southampton Stefan Hallerstede, HeinrichHeineUniversität Düsseldorf Laurent Voisin, Systerel To subscribe to rodinbsharp mailing lists: http://wiki.eventb.org/index.php/Mailing_lists 
From: Paulo J. Matos <pocmatos@gm...>  20090520 11:27:12

On Wed, May 20, 2009 at 9:36 AM, Laurent Voisin <laurent.voisin@...> wrote: > Hi Paulo, > > Le 20 mai 09 à 08:21, Paulo J. Matos a écrit : > >> From the EventB 1.0 Mathematical Language, in the typing algorithm >> part we have for exprunary: >> expruna: E ::= E1 [exprunop] >> Let α and β be distinct fresh type variables in >> E1 .ityvars = E.ityvars ∪ {α, β} >> E1 .ityenv = E.ityenv >> E1 .ityeqs = E.ityeqs >> E.styvars = E1 .styvars >> E.styenv = E1 .styenv >> E.styeqs = E1 .styeqs ∪ E >> E.type = τ >> >> Where τ is defined in a table. >> In this expression type and similarly in others, the type variables >> {α, β} are inherited by the arguments of the expression. Is there any >> reason for this or it would be equivalent to: >> expruna: E ::= E1 [exprunop] >> Let α and β be distinct fresh type variables in >> E1 .ityvars = E.ityvars >> E1 .ityenv = E.ityenv >> E1 .ityeqs = E.ityeqs >> E.styvars = E1 .styvars ∪ {α, β} >> E.styenv = E1 .styenv >> E.styeqs = E1 .styeqs ∪ E >> E.type = τ >> >> If they are not equivalent, could you please provide an expression >> where the second one fails to typecheck and the first one doesn't? [I >> simply can't find one, therefore I assume equivalence, but I would >> appreciate some input]. > > Well, looking at your remark I found out that there is some implicitness in > the phrase "fresh type variables". When I wrote that I meant "a type > variable that doesn't occur in E.ityvars". If you give it the meaning "a > type variable that doesn't occur in E.styvars", then your proposed change is > equivalent. > > Indeed, as type variables are used only in synthesised attributes, fresh > type variables can be allocated as well during synthesis. > Great, thanks for the explanation. :) Cheers, Paulo Matos > Laurent. >  Paulo Jorge Matos  pocmatos at gmail.com Webpage: http://www.personal.soton.ac.uk/pocm 
From: Laurent Voisin <laurent.voisin@sy...>  20090520 08:36:51

Hi Paulo, Le 20 mai 09 à 08:21, Paulo J. Matos a écrit : > From the EventB 1.0 Mathematical Language, in the typing algorithm > part we have for exprunary: > expruna: E ::= E1 [exprunop] > Let α and β be distinct fresh type variables in > E1 .ityvars = E.ityvars ∪ {α, β} > E1 .ityenv = E.ityenv > E1 .ityeqs = E.ityeqs > E.styvars = E1 .styvars > E.styenv = E1 .styenv > E.styeqs = E1 .styeqs ∪ E > E.type = τ > > Where τ is defined in a table. > In this expression type and similarly in others, the type variables > {α, β} are inherited by the arguments of the expression. Is there > any > reason for this or it would be equivalent to: > expruna: E ::= E1 [exprunop] > Let α and β be distinct fresh type variables in > E1 .ityvars = E.ityvars > E1 .ityenv = E.ityenv > E1 .ityeqs = E.ityeqs > E.styvars = E1 .styvars ∪ {α, β} > E.styenv = E1 .styenv > E.styeqs = E1 .styeqs ∪ E > E.type = τ > > If they are not equivalent, could you please provide an expression > where the second one fails to typecheck and the first one doesn't? [I > simply can't find one, therefore I assume equivalence, but I would > appreciate some input]. Well, looking at your remark I found out that there is some implicitness in the phrase "fresh type variables". When I wrote that I meant "a type variable that doesn't occur in E.ityvars". If you give it the meaning "a type variable that doesn't occur in E.styvars", then your proposed change is equivalent. Indeed, as type variables are used only in synthesised attributes, fresh type variables can be allocated as well during synthesis. Laurent. 
From: Paulo J. Matos <pocmatos@gm...>  20090520 06:22:10

Hi, >From the EventB 1.0 Mathematical Language, in the typing algorithm part we have for exprunary: expruna: E ::= E1 [exprunop] Let α and β be distinct fresh type variables in E1 .ityvars = E.ityvars ∪ {α, β} E1 .ityenv = E.ityenv E1 .ityeqs = E.ityeqs E.styvars = E1 .styvars E.styenv = E1 .styenv E.styeqs = E1 .styeqs ∪ E E.type = τ Where τ is defined in a table. In this expression type and similarly in others, the type variables {α, β} are inherited by the arguments of the expression. Is there any reason for this or it would be equivalent to: expruna: E ::= E1 [exprunop] Let α and β be distinct fresh type variables in E1 .ityvars = E.ityvars E1 .ityenv = E.ityenv E1 .ityeqs = E.ityeqs E.styvars = E1 .styvars ∪ {α, β} E.styenv = E1 .styenv E.styeqs = E1 .styeqs ∪ E E.type = τ If they are not equivalent, could you please provide an expression where the second one fails to typecheck and the first one doesn't? [I simply can't find one, therefore I assume equivalence, but I would appreciate some input]. Cheers,  Paulo Jorge Matos  pocmatos at gmail.com Webpage: http://www.personal.soton.ac.uk/pocm 
From: Ken Robinson <kenr@cs...>  20090518 11:00:50

Laurent, I missed Paulo's reply because for some reason it got directed into my junk mail box! :) No reflection on what you said Paulo. On 18/05/2009, at 19:07 PM, Laurent Voisin wrote: > Le 16 mai 09 à 14:44, Paulo J. Matos a écrit : >> On Sat, May 16, 2009 at 12:19 PM, Thai Son Hoang >> <htson@...> wrote: >>> Ken Robinson wrote: >>>> I first saw this in an earlier release of Rodin, but it's still >>>> there. >>>> Why does Rodin object to the use of the same variable name in these >>>> disjoint quantifiers? >>>> >>> It is just an warning to the user, i.e. it is not incorrect (error), >>> but it is better to change it (that is my interpretation of >>> warning). >>> >> This is definitely NOT my interpretation of the mathematical >> language. >> Page 24 of the mathematical language states that: >> " For a formula to be considered legible, we ask that, beyond >> being syntacti >> cally correct, it also satisfies the two following conditions: >> 1. Any identifier that occurs in the formula, should have only free >> occurrences >> or bound occurrences, but not both. >> 2. Any identifier that occurs bound in the formula, should be bound >> in ex >> actly one place (i.e., by only one quantifier)." >> >> Ken is in his example failing to meet point 2 since the variable l is >> bound in the same formula twice. This is obviously not a mathematical >> error but it is indeed considered a legibility error in EventB and >> RODIN marks it as such. Yes, I accept this is not a bug and that it's only a warning. I clearly have not read that part of the language manual, and I'd better read it to find out what other legibility rules it has. I think legibility is a bit tricky. I very much appreciate opinions on legibility and I regard legibility. It's clearly subjective, but I don't regard my preferred form of expression at all illegible. > This is indeed not a bug, as this check is described in the > mathematical language specification. However, I understand that > this check can sometimes be spurious. I've therefore entered a > feature request in SourceForge to make this check optional: > > https://sourceforge.net/tracker/?func=detail&aid=2793244&group_id=108850&atid=651672 Laurent: your comments on this feature request appear to concur with my comments above, and I appreciate your suggested remedy. If there are more of these legibility checks, perhaps they should all be optional? Thanks, Ken 
From: Laurent Voisin <laurent.voisin@sy...>  20090518 09:07:22

Ken, Le 16 mai 09 à 14:44, Paulo J. Matos a écrit : > On Sat, May 16, 2009 at 12:19 PM, Thai Son Hoang <htson@...> > wrote: >> Ken Robinson wrote: >>> I first saw this in an earlier release of Rodin, but it's still >>> there. >>> Why does Rodin object to the use of the same variable name in these >>> disjoint quantifiers? >>> >> It is just an warning to the user, i.e. it is not incorrect (error), >> but it is better to change it (that is my interpretation of warning). >> > This is definitely NOT my interpretation of the mathematical language. > Page 24 of the mathematical language states that: > " For a formula to be considered legible, we ask that, beyond > being syntacti > cally correct, it also satisfies the two following conditions: > 1. Any identifier that occurs in the formula, should have only free > occurrences > or bound occurrences, but not both. > 2. Any identifier that occurs bound in the formula, should be bound > in ex > actly one place (i.e., by only one quantifier)." > > Ken is in his example failing to meet point 2 since the variable l is > bound in the same formula twice. This is obviously not a mathematical > error but it is indeed considered a legibility error in EventB and > RODIN marks it as such. This is indeed not a bug, as this check is described in the mathematical language specification. However, I understand that this check can sometimes be spurious. I've therefore entered a feature request in SourceForge to make this check optional: https://sourceforge.net/tracker/?func=detail&aid=2793244&group_id=108850&atid=651672 Laurent. 
From: Paulo J. Matos <pocmatos@gm...>  20090516 12:44:55

On Sat, May 16, 2009 at 12:19 PM, Thai Son Hoang <htson@...> wrote: > > Dear Ken, > Ken Robinson wrote: >> I first saw this in an earlier release of Rodin, but it's still there. >> >> Consider >> >> >>  >> >> >> >> >> Why does Rodin object to the use of the same variable name in these >> disjoint quantifiers? >> > > It is just an warning to the user, i.e. it is not incorrect (error), > but it is better to change it (that is my interpretation of warning). > [snip] Hello, This is definitely NOT my interpretation of the mathematical language. Page 24 of the mathematical language states that: " For a formula to be considered legible, we ask that, beyond being syntacti cally correct, it also satisfies the two following conditions: 1. Any identifier that occurs in the formula, should have only free occurrences or bound occurrences, but not both. 2. Any identifier that occurs bound in the formula, should be bound in ex actly one place (i.e., by only one quantifier)." Ken is in his example failing to meet point 2 since the variable l is bound in the same formula twice. This is obviously not a mathematical error but it is indeed considered a legibility error in EventB and RODIN marks it as such. Cheers, Paulo Matos >  > Crystal Reports  New Free Runtime and 30 Day Trial > Check out the new simplified licensing option that enables > unlimited royaltyfree distribution of the report engine > for externally facing server and web deployment. > http://p.sf.net/sfu/businessobjects > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser >  Paulo Jorge Matos  pocmatos at gmail.com Webpage: http://www.personal.soton.ac.uk/pocm 
From: Ken Robinson <kenr@cs...>  20090516 12:23:36

Dear Son, Thanks for your reply. On 16/05/2009, at 20:08 PM, Thai Son Hoang wrote: > Ken Robinson wrote: >> I first saw this in an earlier release of Rodin, but it's still >> there. >> Consider >>  >> Why does Rodin object to the use of the same variable name in these >> disjoint quantifiers? > > It is just an warning to the user, i.e. it is not incorrect (error), > but it is better to change it (that is my interpretation of warning). > >> If the above is invalid, what are the scoping rules for Rodin in >> this context? > > Basically, it is complain that you use the same bounded variables, > and it could be clearer if you use different ones. Logically, there > is nothing wrong with it, but in terms of modelling, this is > probably not a good idea. I take your point that this is a warning, but it's annoying enough that it might as well be an error. I would prefer to regard this as a bug. Rodin is warning about something that is purely style. What's the limit of all the style warnings that Rodin could give if we continued down that road? In this case I quite deliberately chose the same identifier for the quantification as the quantification is essentially over the same construct. I could have used a single quantification and had two separate choices, but I chose to make them separate. I'm copying this reply back to the Rodin user mail list, as I'd be interested in any other reactions to this Cheers, Ken 
From: Thai Son Hoang <htson@in...>  20090516 11:21:48

Dear Ken, Ken Robinson wrote: > I first saw this in an earlier release of Rodin, but it's still there. > > Consider > > >  > > > > > Why does Rodin object to the use of the same variable name in these > disjoint quantifiers? > It is just an warning to the user, i.e. it is not incorrect (error), but it is better to change it (that is my interpretation of warning). > If the above is invalid, what are the scoping rules for Rodin in this > context? > Basically, it is complain that you use the same bounded variables, and it could be clearer if you use different ones. Logically, there is nothing wrong with it, but in terms of modelling, this is probably not a good idea. Cheers, Son 
From: Ken Robinson <kenr@cs...>  20090516 03:02:19

I first saw this in an earlier release of Rodin, but it's still there. Consider 
From: Hoang Lan Nguyen <lan@cs...>  20090513 18:15:36

Thank you so much, JeanRaymond. I think you pointed out the exact problem of my model. Problem solved. Lan On Wed, 13 May 2009, JeanRaymond Abrial wrote: > Dear Lan, > > If the function is > > DATA >> NAT > > it is normal that the FIS PO cannot be discharged. The set DATA is a priori > any nonempty set: it can be far bigger than NAT. If DATA is instantiated to > POW(NAT) then such an injection does not exist! > > JR > 
From: JeanRaymond Abrial <jabrial@in...>  20090513 03:18:41

Dear Lan, If the function is DATA >> NAT it is normal that the FIS PO cannot be discharged. The set DATA is a priori any nonempty set: it can be far bigger than NAT. If DATA is instantiated to POW(NAT) then such an injection does not exist! JR 
From: Hoang Lan Nguyen <lan@cs...>  20090513 00:40:27

Yes, it works if my function is NAT +> DATA. But what if my function is DATA >> NAT (where DATA is a carrier set), then the function cannot be initialized to empty. My question is: if I want to initialize two nonempty functions v1 and v2 such that they must be equal to each other, how would I do that ? I figured the way JeanRaymond suggested, like writing: v1,v2 : v1' : DATA >> NAT & v2' : DATA >> NAT & v1' = v2' didn't discharge the FIS PO (I guess because v1, v2 are functions). Lan On Wed, 13 May 2009, Thai Son Hoang wrote: > > Hi Lan, > Hoang Lan Nguyen wrote: >> You're right, Son. It discharged. However, when I applied this method to >> functions, the FIS PO didn't discharge. This is what I did: >> >> v1,v2 : v1' : NAT +> DATA & v2' : NAT +> DATA & v1' = v2' >> >> Do you know why FIS PO doesn't discharge when v1 and v2 are functions ? >> Is there any way to get it discharged ? >> > > If this is the case then you can just initialised v1, v2 to empty set, > i.e. v1,v2 := {}, {}. You will not need to prove this FIS PO at all. > Cheers, > Son > >  > The NEW KODAK i700 Series Scanners deliver under ANY circumstances! Your > production scanning environment may not be a perfect world  but thanks to > Kodak, there's a perfect scanner to get the job done! With the NEW KODAK i700 > Series Scanner you'll get full speed at 300 dpi even with all image > processing features enabled. http://p.sf.net/sfu/kodakcom > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 
From: Thai Son Hoang <htson@in...>  20090512 22:54:04

Hi Lan, Hoang Lan Nguyen wrote: > You're right, Son. It discharged. However, when I applied this method to > functions, the FIS PO didn't discharge. This is what I did: > > v1,v2 : v1' : NAT +> DATA & v2' : NAT +> DATA & v1' = v2' > > Do you know why FIS PO doesn't discharge when v1 and v2 are functions ? > Is there any way to get it discharged ? > If this is the case then you can just initialised v1, v2 to empty set, i.e. v1,v2 := {}, {}. You will not need to prove this FIS PO at all. Cheers, Son 
From: Thai Son Hoang <htson@in...>  20090512 21:56:36

Hi Lan, Hoang Lan Nguyen wrote: > Hi JeanRaymond, > > Yes, this works for natural numbers NAT. But what if my v1 and v2 > variables belong to a carrier set, which could be anything. For example, > if I declare a carrier set DATA as a constant in my context, then if I > initialize v1 and v2 as you suggested: > > v1,v2 : v1' : DATA & v2' : DATA & v1' = v2' > > That gave me no error but I couldn't get the Feasibility PO discharged, > because I must show there exists a value X in DATA that v1 = v2 = X. But > since I declared DATA as a generic carrier set (with no specific > elements), I couldn't find such X that could discharge the PO. > > Do you have any ideas how to solve this ? > > Thanks a lot for your helps so far. I really appreciated it. > On second thought, DATA is nonempty set by convention of carrier set, hence this should be provable. I just tried the following on Rodin 9.2.1 CONTEXT c SETS S THEOREM #x,y. x : S & y : S & x = y END Then the theorem is proved automatically by Aterlier B ML. I wonder if you have the actual prover installed. Cheers, Son 
From: Hoang Lan Nguyen <lan@cs...>  20090512 21:53:46

You're right, Son. It discharged. However, when I applied this method to functions, the FIS PO didn't discharge. This is what I did: v1,v2 : v1' : NAT +> DATA & v2' : NAT +> DATA & v1' = v2' Do you know why FIS PO doesn't discharge when v1 and v2 are functions ? Is there any way to get it discharged ? Lan On Tue, 12 May 2009, Thai Son Hoang wrote: > > Hi Lan, > Hoang Lan Nguyen wrote: >> Hi JeanRaymond, >> >> Yes, this works for natural numbers NAT. But what if my v1 and v2 variables >> belong to a carrier set, which could be anything. For example, if I declare >> a carrier set DATA as a constant in my context, then if I initialize v1 and >> v2 as you suggested: >> >> v1,v2 : v1' : DATA & v2' : DATA & v1' = v2' >> >> That gave me no error but I couldn't get the Feasibility PO discharged, >> because I must show there exists a value X in DATA that v1 = v2 = X. But >> since I declared DATA as a generic carrier set (with no specific elements), >> I couldn't find such X that could discharge the PO. >> >> Do you have any ideas how to solve this ? >> >> Thanks a lot for your helps so far. I really appreciated it. >> > > You are missing an axiom for DATA to say that it is not empty, i.e. DATA /= > {}. That should get the FIS PO discharged. > Cheers, > Son > 
From: Hoang Lan Nguyen <lan@cs...>  20090512 21:07:59

Hi JeanRaymond, Yes, this works for natural numbers NAT. But what if my v1 and v2 variables belong to a carrier set, which could be anything. For example, if I declare a carrier set DATA as a constant in my context, then if I initialize v1 and v2 as you suggested: v1,v2 : v1' : DATA & v2' : DATA & v1' = v2' That gave me no error but I couldn't get the Feasibility PO discharged, because I must show there exists a value X in DATA that v1 = v2 = X. But since I declared DATA as a generic carrier set (with no specific elements), I couldn't find such X that could discharge the PO. Do you have any ideas how to solve this ? Thanks a lot for your helps so far. I really appreciated it. Lan On Tue, 12 May 2009, JeanRaymond Abrial wrote: > Dear Lan, > > It is very simple. > > v1,v2 : v1':NAT & v2':NAT & v1'=v2' > > The reason why ANY is vorbidden in INIT is that the guard is not necessarily > true. An initialisation assignment must always be possible so such > initialisation never contains any potentially non true guard. > > With the assignment I gave you the Proof Obligation Generator generates a > Feasibility PO, which, in this case, is discharged automatically. Try it. > > Cheers, > > JeanRaymond > On May 12, 2009, at 12:59 AM, Hoang Lan Nguyen wrote: > >> Hi JeanRaymond, >> >> But that would not work if I'd want to initialize two variables with the >> same arbitrary value, like this: >> >> INITIALISATION >> ANY n WHERE >> n : NAT >> THEN >> v1 := n >> v2 := n >> END >> >> I tried this in Rodin and it gave me an error that Initialisation event >> does not take parameters. >> >> How would you solve this in Rodin ? >> >> Thanks, >> >> Lan >> >> On Mon, 11 May 2009, JeanRaymond Abrial wrote: >> >>> Dear Lan, >>> >>> >>> V :: NAT >>> >>> JeanRaymond >>> >>> On May 11, 2009, at 10:58 PM, Hoang Lan Nguyen wrote: >>> >>>> Hi, >>>> In B, I believe we can do the following in the INITIALISATION event: >>>> INITIALISATION >>>> ANY n WHERE >>>> n : NAT >>>> THEN >>>> v := n >>>> END >>>> So I was wondering how we would do the same thing as above in Rodin >>>> EventB ? >>>> Thanks a lot. >>>> Lan >>>>  >>>> The NEW KODAK i700 Series Scanners deliver under ANY circumstances! Your >>>> production scanning environment may not be a perfect world  but thanks >>>> to >>>> Kodak, there's a perfect scanner to get the job done! With the NEW KODAK >>>> i700 >>>> Series Scanner you'll get full speed at 300 dpi even with all image >>>> processing features enabled. http://p.sf.net/sfu/kodakcom >>>> _______________________________________________ >>>> Rodinbsharpuser mailing list >>>> Rodinbsharpuser@... >>>> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser >>> > 
From: JeanRaymond Abrial <jabrial@in...>  20090512 05:46:24

Dear Lan, It is very simple. v1,v2 : v1':NAT & v2':NAT & v1'=v2' The reason why ANY is vorbidden in INIT is that the guard is not necessarily true. An initialisation assignment must always be possible so such initialisation never contains any potentially non true guard. With the assignment I gave you the Proof Obligation Generator generates a Feasibility PO, which, in this case, is discharged automatically. Try it. Cheers, JeanRaymond On May 12, 2009, at 12:59 AM, Hoang Lan Nguyen wrote: > Hi JeanRaymond, > > But that would not work if I'd want to initialize two variables with > the same arbitrary value, like this: > > INITIALISATION > ANY n WHERE > n : NAT > THEN > v1 := n > v2 := n > END > > I tried this in Rodin and it gave me an error that Initialisation > event does not take parameters. > > How would you solve this in Rodin ? > > Thanks, > > Lan > > On Mon, 11 May 2009, JeanRaymond Abrial wrote: > >> Dear Lan, >> >> >> V :: NAT >> >> JeanRaymond >> >> On May 11, 2009, at 10:58 PM, Hoang Lan Nguyen wrote: >> >>> Hi, >>> In B, I believe we can do the following in the INITIALISATION event: >>> INITIALISATION >>> ANY n WHERE >>> n : NAT >>> THEN >>> v := n >>> END >>> So I was wondering how we would do the same thing as above in >>> Rodin EventB ? >>> Thanks a lot. >>> Lan >>>  >>> The NEW KODAK i700 Series Scanners deliver under ANY >>> circumstances! Your >>> production scanning environment may not be a perfect world  but >>> thanks to >>> Kodak, there's a perfect scanner to get the job done! With the NEW >>> KODAK i700 >>> Series Scanner you'll get full speed at 300 dpi even with all image >>> processing features enabled. http://p.sf.net/sfu/kodakcom >>> _______________________________________________ >>> Rodinbsharpuser mailing list >>> Rodinbsharpuser@... >>> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser >> 
From: Hoang Lan Nguyen <lan@cs...>  20090511 22:59:42

Hi JeanRaymond, But that would not work if I'd want to initialize two variables with the same arbitrary value, like this: INITIALISATION ANY n WHERE n : NAT THEN v1 := n v2 := n END I tried this in Rodin and it gave me an error that Initialisation event does not take parameters. How would you solve this in Rodin ? Thanks, Lan On Mon, 11 May 2009, JeanRaymond Abrial wrote: > Dear Lan, > > > V :: NAT > > JeanRaymond > > On May 11, 2009, at 10:58 PM, Hoang Lan Nguyen wrote: > >> Hi, >> >> In B, I believe we can do the following in the INITIALISATION event: >> >> INITIALISATION >> ANY n WHERE >> n : NAT >> THEN >> v := n >> END >> >> So I was wondering how we would do the same thing as above in Rodin EventB >> ? >> >> Thanks a lot. >> >> Lan >> >>  >> The NEW KODAK i700 Series Scanners deliver under ANY circumstances! Your >> production scanning environment may not be a perfect world  but thanks to >> Kodak, there's a perfect scanner to get the job done! With the NEW KODAK >> i700 >> Series Scanner you'll get full speed at 300 dpi even with all image >> processing features enabled. http://p.sf.net/sfu/kodakcom >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > 