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}
(3) 
_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 



1

2
(1) 
3
(4) 
4

5

6

7

8
(3) 
9
(1) 
10

11

12

13

14

15

16

17

18

19

20

21

22

23
(1) 
24

25

26

27

28

29

30
(1) 



From: Renato Silva <ras07r@ec...>  20111130 01:02:59

Dear Rodin Users, I am delighted to announce the release of the Code Generation plugin v0.2. This version has several changes in relation to the previous one. To take advantage of its potential, the theory plugin and the shared event composition plugin should be used. Before using the plugin, I strongly advise users to read the User Manual and the plugin documentation available at the plugin wikipage at: http://wiki.eventb.org/index.php/Code_Generation#Code_Generation_Feature__Version_0.2.0_For_Rodin_2.3 At the moment, C and Ada are supported but other target languages should be supported in the future. For further information or to report problems, please do not hesitate to contact me, Andrew Edmunds <ae2@...> or Chris Lovell <cjl3@...>. Renato Silva ras07r@... 
From: Michael Jastram <michael@ja...>  20111123 20:55:59

Dear all, Most of you are probably aware of the Rodin Handbook project, an effort to improve the Rodin documentation. The Handbook project can be accessed at http://handbook.eventb.org/ In December, we are going to start the forth  and last  iteration of the project. In order to assess our effort so far, and to identify weaknesses for us to focus on in the last iteration, we created a survey. It shouldn't take longer than five minutes to answer. You can access the survey at http://www.kwiksurveys.com/onlinesurvey.php?surveyID=OOKKJK_4e2d5408 Please provide your answer by December 4th. Thank you in advance for your help,  Michael  Michael Jastram (http://www.jastram.de, +49 (162) 274 83 94) Geschäftsführer, Formal Mind GmbH (http://formalmind.com) Wissenschaftler, Heinrich Heine Universität Düsseldorf (http://www.stups.uniduesseldorf.de) 1. Vorsitzender, rheinjug e.V. (http://www.rheinjug.de) 
From: Daniel Plagge <plagge@cs...>  20111109 10:29:56

Hello Nicolas and Matthias, thank you very much for your answers. I'll put that into the corresponding reference sections of the Rodin handbook. Bests Daniel Am 08.11.2011 19:32, schrieb Matthias Schmalz: > Hi Daniel, > > maybe you wonder what distinguishes {}, id, prj1, prj2 from other > constants/operators: they are constants with a type variable in their type. > > {} oftype P('a) > id oftype P('a * 'a) > prj1 oftype P('a * 'b *'a) > prj2 oftype P('a * 'b * 'b) > > More generally, if an operator has a type variable in its result type > that does not occur in an argument type, the operator admits "oftype". > > @Nicolas: > IMHO, it would be helpful if the users could write oftype wherever they > want. Even if the rules about oftype are welldocumented, users still > have to learn and remember them. > > Best, > Matthias > > Am 08.11.2011 18:42, schrieb Nicolas Beauger: >> Hello Daniel, >> >> The documentation has to be updated, as it does not cover the 'oftype' >> subject. >> This documentation can be fetched at: >> http://wiki.eventb.org/index.php/EventB_Mathematical_Language >> >> Roughly speaking, 'oftype' is a hint to the type checker, for cases >> where it cannot be determined from the context. >> It can be used with: >>  generic atomic expressions ({}, id, prj1, prj2) >>  bound variable declarations ('!x . x=x' does not type check, whereas >> '!x oftype INT . x=x' does) >> >> In your formula, '{} = ( {5} oftype POW(INT) )', oftype is not allowed >> after {5}, but the type can be guessed without a hint anyway. >> >> Kind regards, >> Nicolas >> >> Le 08/11/2011 16:09, Daniel Plagge a écrit : >>> Hello, >>> >>> I'm currently working on the reference entry for the oftype operator >>> and I'm a little bit lost. >>> I do not understand what kind of expression is allowed on the left >>> side of the operator. >>> The following works: >>> >>> * {} = ( {} oftype POW(INT) ) >>> * {} = ( id oftype POW(INT**INT) ) >>> >>> But it seems that the right side is restricted to some expressions, e.g. >>> >>> * {} = ( {5} oftype POW(INT) ) >>> >>> yields a "Syntax error: Oftype is not expected here". >>> >>> Can anybody point me to some documentation or explain what kind of >>> expressions are allowed? >>> >>> Best regards >>> Daniel >>> >>> >>> >>>  >>> RSA(R) Conference 2012 >>> Save $700 by Nov 18 >>> Register now >>> http://p.sf.net/sfu/rsasfdev2dev1 >>> >>> >>> _______________________________________________ >>> Rodinbsharpuser mailing list >>> Rodinbsharpuser@... >>> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser >>  >>  >> Nicolas BEAUGER Tél. : (+33)(0)4 42 90 65 66 >> Ingénieur Logiciel >> >> SYSTEREL >>  >> Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site :www.systerel.fr >>  >> >> >> >>  >> RSA(R) Conference 2012 >> Save $700 by Nov 18 >> Register now >> http://p.sf.net/sfu/rsasfdev2dev1 >> >> >> >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser >  > RSA(R) Conference 2012 > Save $700 by Nov 18 > Register now > http://p.sf.net/sfu/rsasfdev2dev1 > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20111108 18:32:45

Hi Daniel, maybe you wonder what distinguishes {}, id, prj1, prj2 from other constants/operators: they are constants with a type variable in their type. {} oftype P('a) id oftype P('a * 'a) prj1 oftype P('a * 'b *'a) prj2 oftype P('a * 'b * 'b) More generally, if an operator has a type variable in its result type that does not occur in an argument type, the operator admits "oftype". @Nicolas: IMHO, it would be helpful if the users could write oftype wherever they want. Even if the rules about oftype are welldocumented, users still have to learn and remember them. Best, Matthias Am 08.11.2011 18:42, schrieb Nicolas Beauger: > Hello Daniel, > > The documentation has to be updated, as it does not cover the 'oftype' > subject. > This documentation can be fetched at: > http://wiki.eventb.org/index.php/EventB_Mathematical_Language > > Roughly speaking, 'oftype' is a hint to the type checker, for cases > where it cannot be determined from the context. > It can be used with: >  generic atomic expressions ({}, id, prj1, prj2) >  bound variable declarations ('!x . x=x' does not type check, whereas > '!x oftype INT . x=x' does) > > In your formula, '{} = ( {5} oftype POW(INT) )', oftype is not allowed > after {5}, but the type can be guessed without a hint anyway. > > Kind regards, > Nicolas > > Le 08/11/2011 16:09, Daniel Plagge a écrit : >> Hello, >> >> I'm currently working on the reference entry for the oftype operator >> and I'm a little bit lost. >> I do not understand what kind of expression is allowed on the left >> side of the operator. >> The following works: >> >> * {} = ( {} oftype POW(INT) ) >> * {} = ( id oftype POW(INT**INT) ) >> >> But it seems that the right side is restricted to some expressions, e.g. >> >> * {} = ( {5} oftype POW(INT) ) >> >> yields a "Syntax error: Oftype is not expected here". >> >> Can anybody point me to some documentation or explain what kind of >> expressions are allowed? >> >> Best regards >> Daniel >> >> >> >>  >> RSA(R) Conference 2012 >> Save $700 by Nov 18 >> Register now >> http://p.sf.net/sfu/rsasfdev2dev1 >> >> >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > >  >  > Nicolas BEAUGER Tél. : (+33)(0)4 42 90 65 66 > Ingénieur Logiciel > > SYSTEREL >  > Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site :www.systerel.fr >  > > > >  > RSA(R) Conference 2012 > Save $700 by Nov 18 > Register now > http://p.sf.net/sfu/rsasfdev2dev1 > > > > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Nicolas Beauger <nicolas.beauger@sy...>  20111108 17:42:29

Hello Daniel, The documentation has to be updated, as it does not cover the 'oftype' subject. This documentation can be fetched at: http://wiki.eventb.org/index.php/EventB_Mathematical_Language Roughly speaking, 'oftype' is a hint to the type checker, for cases where it cannot be determined from the context. It can be used with:  generic atomic expressions ({}, id, prj1, prj2)  bound variable declarations ('!x . x=x' does not type check, whereas '!x oftype INT . x=x' does) In your formula, '{} = ( {5} oftype POW(INT) )', oftype is not allowed after {5}, but the type can be guessed without a hint anyway. Kind regards, Nicolas Le 08/11/2011 16:09, Daniel Plagge a écrit : > Hello, > > I'm currently working on the reference entry for the oftype operator > and I'm a little bit lost. > I do not understand what kind of expression is allowed on the left > side of the operator. > The following works: > > * {} = ( {} oftype POW(INT) ) > * {} = ( id oftype POW(INT**INT) ) > > But it seems that the right side is restricted to some expressions, e.g. > > * {} = ( {5} oftype POW(INT) ) > > yields a "Syntax error: Oftype is not expected here". > > Can anybody point me to some documentation or explain what kind of > expressions are allowed? > > Best regards > Daniel > > > >  > RSA(R) Conference 2012 > Save $700 by Nov 18 > Register now > http://p.sf.net/sfu/rsasfdev2dev1 > > > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser   Nicolas BEAUGER Tél. : (+33)(0)4 42 90 65 66 Ingénieur Logiciel SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Daniel Plagge <plagge@cs...>  20111108 15:46:41

Hello, I'm currently working on the reference entry for the oftype operator and I'm a little bit lost. I do not understand what kind of expression is allowed on the left side of the operator. The following works: * {} = ( {} oftype POW(INT) ) * {} = ( id oftype POW(INT**INT) ) But it seems that the right side is restricted to some expressions, e.g. * {} = ( {5} oftype POW(INT) ) yields a "Syntax error: Oftype is not expected here". Can anybody point me to some documentation or explain what kind of expressions are allowed? Best regards Daniel 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20111103 20:12:24

Hi Alexei, it took me a moment to figure out the details. I finally proved > ! p, f. finite(f) => card(f[p]) <= card(f) in Isabelle. The details are rather unwieldy  I had to make an induction over f. So if you don't mind using Isabelle, you can export the proof obligation and prove it there. Maybe it is also possible to carry out the induction in Rodin. I don't have the time to find out. Best, Matthias P.s.: My Isabelle proof (rather quick and dirty): theory test imports EventB begin lemma card_Image: assumes "finite r" shows "card (r `` A) ≤ card r" using assms proof (induct r rule: finite.induct) case emptyI thus ?case by auto next case (insertI r x) thus ?case proof (induct "x ∈ r") case True hence "insert x r = r" by blast with True show ?case by simp next case False from `finite r` have "finite (Range r)" by (rule finite_Range) moreover have "r `` A ⊆ Range r" by auto ultimately have "finite (r `` A)" by (rule rev_finite_subset) hence "card (insert x r `` A) ≤ card (r `` A) + 1" apply (cases x) apply (case_tac "a ∈ A") apply (case_tac "b ∈ r `` A") by (auto simp add: insert_absorb) with False show ?case by simp qed qed lemma "T ∀^ p f. bfinite f↑ ^⟶^ bcard (brelimg f↑ p↑) .≤. bcard f↑" proof (ebsimp, safe) fix p :: "'a set" and f :: "('a × 'b) set" assume "finite f" hence "finite (Range f)" by (rule finite_Range) moreover have "f `` p ⊆ Range f" by auto ultimately show "finite (f `` p)" by (rule rev_finite_subset) next fix p :: "'a set" and f :: "('a × 'b) set" assume "finite f" hence "card (f `` p) ≤ card f" by (rule card_Image) thus "int (card (f `` p)) ≤ int (card f)" by auto qed end Am 03.11.2011 12:16, schrieb Alexei Iliasov: > Hi fellow Rodin users, > > I am stuck the following innocuous looking condition > > ! p, f. f : NAT +> NAT& finite(f)& p<:NAT => card(f[p])<= card(f) > > If anybody could give hints on how this may be proven (or why it cannot > be) I would be very grateful. > > Best regards, > Alexei > >  > RSA(R) Conference 2012 > Save $700 by Nov 18 > Register now > http://p.sf.net/sfu/rsasfdev2dev1 > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Laurent Voisin <laurent.voisin@sy...>  20111103 12:44:06

Alexei, please ignore my previous mail, it was silly (I misread the consequent for equality instead of inequality). I'm afraid that there is currently not enough support in the user interface to prove such a theorem. I would proceed in stating that "card(f[p]) <= card(p < f)", and then ML can prove that "card(p < f) <= card(f)". However, I don't see a way to prove that "card(f[p]) = card(p < f)" with Rodin 2.3. Maybe it could be done by translating to Isabelle with Matthias' plugin. Cheers, Laurent. Le 3 nov. 2011 à 13:08, Laurent Voisin a écrit : > Hi Alexei, > > Le 3 nov. 2011 à 12:16, Alexei Iliasov a écrit : > >> Hi fellow Rodin users, >> >> I am stuck the following innocuous looking condition >> >> ! p, f. f : NAT +> NAT & finite(f) & p <:NAT => card(f[p]) <= card(f) >> >> If anybody could give hints on how this may be proven (or why it cannot >> be) I would be very grateful. > > You need also that p <: dom(f) . > > Laurent. >  > RSA(R) Conference 2012 > Save $700 by Nov 18 > Register now > http://p.sf.net/sfu/rsasfdev2dev1 > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Laurent Voisin <laurent.voisin@sy...>  20111103 12:08:36

Hi Alexei, Le 3 nov. 2011 à 12:16, Alexei Iliasov a écrit : > Hi fellow Rodin users, > > I am stuck the following innocuous looking condition > > ! p, f. f : NAT +> NAT & finite(f) & p <:NAT => card(f[p]) <= card(f) > > If anybody could give hints on how this may be proven (or why it cannot > be) I would be very grateful. You need also that p <: dom(f) . Laurent. 
From: Alexei Iliasov <alexei.iliasov@nc...>  20111103 11:16:52

Hi fellow Rodin users, I am stuck the following innocuous looking condition ! p, f. f : NAT +> NAT & finite(f) & p <:NAT => card(f[p]) <= card(f) If anybody could give hints on how this may be proven (or why it cannot be) I would be very grateful. Best regards, Alexei 
From: Laurent Voisin <laurent.voisin@sy...>  20111102 09:25:29

Hi Anh Le, a complement to Alexei's answer below. Le 29 oct. 2011 à 17:11, Alexei Iliasov a écrit : > EventB context sets are mutually disjoint by definition (I suspect it > is due to the typing system of EventB). Thus, yours S1 and S2 must be > subsets of some other set, say set S. > > context c > sets S > constants S1, S2, a,b,c,d,e > axioms > @a1 S1 <: S > @a2 S2 <: S > @a3 S1 = {a,b,c} > @a3 S2 = {a,d,e} > > you might also want to say that a,b, ... are distinct elements. To do this, just write instead in axiom @a3 : partition(S1, {a}, {b}, {c}) Cheers, Laurent. >> Hi everyone, >> >> I am first sorry for a very basic question, since I am very new to >> EventB and Rodin. >> >> I created 2 sets S1 = {a,b,c} , S2= {a,d,e}, it informs that there are >> mistakes because of the >> common element a between 2 sets. >> >> How can i represent such 2 sets. >> >> Thank you all in advance. >> >> Anh Le >> >> > > >  > Get your Android app more play: Bring it to the BlackBerry PlayBook > in minutes. BlackBerry App World™ now supports Android™ Apps > for the BlackBerry® PlayBook™. Discover just how easy and simple > it is! http://p.sf.net/sfu/androiddev2dev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 