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}
(7) 
_{Sep}
(23) 
_{Oct}
(4) 
_{Nov}
(9) 
_{Dec}

S  M  T  W  T  F  S 


1
(2) 
2

3

4

5

6
(1) 
7

8

9

10

11

12
(1) 
13

14

15
(1) 
16

17

18
(1) 
19
(2) 
20

21

22
(1) 
23

24

25

26

27

28

29

30

31
(4) 



From: Laurent Voisin <laurent.voisin@sy...>  20110831 14:01:39

Dear All, Matthias response is very accurate and to the point. Thank you Matthias. I'm just adding a rationale for some of the design decisions. The precedence comes from the Ada language specification where all additive operators (e.g., unary minus) have lower precedence than multiplicative operators (e.g., mod). As concerns the WD condition for modulo, it comes from Atelier B which supports modulo only for nonnegative integers. This restriction allows the seamless integration of the Atelier B provers for all arithmetic formulas. Cheers, Laurent. Le 31 août 2011 à 15:16, Matthias Schmalz a écrit : > Hi, > > the modulo operator is certainly one of the more surprising concepts in > EventB. Is somebody out there actually using it? Please send me an email! > >> That behaviour is somehow inconsistent. The documentation ( >> http://deployeprints.ecs.soton.ac.uk/11/4/kernel_lang.pdf , page 43 >> ) says that the WD condition for "a mod b" is "b>0". > > The WD condition of "a mod b" is "a >= 0 & b > 0". The mathematical > language specification incorrectly states "b /= 0", and not "b > 0" as > you write. Interestingly, the WD condition of "a div b" is "b /= 0". So > div accepts negative numbers, while modulo does not. > > I have spent a lot of time in figuring out such details. The result can > be found in > ftp://ftp.inf.ethz.ch/pub/publications/techreports/6xx/698.pdf > During the process I have learned to always question the correctness of > the mathematical language specification. > >> If I have the theorem >> 2 mod 5 = 3 >> Rodin (version 2.2.2) is able to prove the WD condition but not the theorem. > > The reason is that mod has higher priority than unary minus. So "2 mod > 5" is parsed as "(2 mod 5)". Nice, isn't it? > >> But if I write >> (35) mod 5 = 3 >> instead, Rodin proves the theorem but is unable to prove the >> (unprovable) WD condition: >> 0 <= (35) > > There are two reasons why you can prove the theorem PO. First, it > includes the (false) hypothesis 0 <= (35). Second, it has the > illdefined goal (35) mod 5 = 3. Proof obligations with an illdefined > hypothesis or goal are considered valid, although few rules are > available to actually prove such proof obligations. > > This last design decision on sequent semantics is actually crucial for > term rewriting. If that point is of interest to you, read my paper > http://www.infsec.ethz.ch/people/mschmalz/icfem2011_tr.pdf > > Matthias 
From: Daniel Plagge <plagge@cs...>  20110831 13:54:30

Thank you very much for the helpful answer, Matthias. I'm currently working on a first draft of some reference sections in the Rodin documentation. I'll will have a closer look at your papers for the future parts. Jens (who's sitting in the same office) already suggested to look at the parenthesis, but I only looked at (35). :) Best regards Daniel On 31.08.2011 15:16, Matthias Schmalz wrote: > Hi, > > the modulo operator is certainly one of the more surprising concepts in > EventB. Is somebody out there actually using it? Please send me an email! > > > That behaviour is somehow inconsistent. The documentation ( > > http://deployeprints.ecs.soton.ac.uk/11/4/kernel_lang.pdf , page 43 > > ) says that the WD condition for "a mod b" is "b>0". > > The WD condition of "a mod b" is "a>= 0& b> 0". The mathematical > language specification incorrectly states "b /= 0", and not "b> 0" as > you write. Interestingly, the WD condition of "a div b" is "b /= 0". So > div accepts negative numbers, while modulo does not. > > I have spent a lot of time in figuring out such details. The result can > be found in > ftp://ftp.inf.ethz.ch/pub/publications/techreports/6xx/698.pdf > During the process I have learned to always question the correctness of > the mathematical language specification. > >> If I have the theorem >> 2 mod 5 = 3 >> Rodin (version 2.2.2) is able to prove the WD condition but not the theorem. > The reason is that mod has higher priority than unary minus. So "2 mod > 5" is parsed as "(2 mod 5)". Nice, isn't it? > >> But if I write >> (35) mod 5 = 3 >> instead, Rodin proves the theorem but is unable to prove the >> (unprovable) WD condition: >> 0<= (35) > There are two reasons why you can prove the theorem PO. First, it > includes the (false) hypothesis 0<= (35). Second, it has the > illdefined goal (35) mod 5 = 3. Proof obligations with an illdefined > hypothesis or goal are considered valid, although few rules are > available to actually prove such proof obligations. > > This last design decision on sequent semantics is actually crucial for > term rewriting. If that point is of interest to you, read my paper > http://www.infsec.ethz.ch/people/mschmalz/icfem2011_tr.pdf > > Matthias > >  > Special Offer  Download ArcSight Logger for FREE! > Finally, a worldclass log management solution at an even better > pricefree! And you'll get a free "Love Thy Logs" tshirt when you > download Logger. Secure your free ArcSight Logger TODAY! > http://p.sf.net/sfu/arcsisghtdev2dev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20110831 13:16:30

Hi, the modulo operator is certainly one of the more surprising concepts in EventB. Is somebody out there actually using it? Please send me an email! > That behaviour is somehow inconsistent. The documentation ( > http://deployeprints.ecs.soton.ac.uk/11/4/kernel_lang.pdf , page 43 > ) says that the WD condition for "a mod b" is "b>0". The WD condition of "a mod b" is "a >= 0 & b > 0". The mathematical language specification incorrectly states "b /= 0", and not "b > 0" as you write. Interestingly, the WD condition of "a div b" is "b /= 0". So div accepts negative numbers, while modulo does not. I have spent a lot of time in figuring out such details. The result can be found in ftp://ftp.inf.ethz.ch/pub/publications/techreports/6xx/698.pdf During the process I have learned to always question the correctness of the mathematical language specification. > If I have the theorem > 2 mod 5 = 3 > Rodin (version 2.2.2) is able to prove the WD condition but not the theorem. The reason is that mod has higher priority than unary minus. So "2 mod 5" is parsed as "(2 mod 5)". Nice, isn't it? > But if I write > (35) mod 5 = 3 > instead, Rodin proves the theorem but is unable to prove the > (unprovable) WD condition: > 0 <= (35) There are two reasons why you can prove the theorem PO. First, it includes the (false) hypothesis 0 <= (35). Second, it has the illdefined goal (35) mod 5 = 3. Proof obligations with an illdefined hypothesis or goal are considered valid, although few rules are available to actually prove such proof obligations. This last design decision on sequent semantics is actually crucial for term rewriting. If that point is of interest to you, read my paper http://www.infsec.ethz.ch/people/mschmalz/icfem2011_tr.pdf Matthias 
From: Daniel Plagge <plagge@cs...>  20110831 11:46:22

Hello everybody, I just stumbled across the modulo operator and its welldefinedness condition. If I have the theorem 2 mod 5 = 3 Rodin (version 2.2.2) is able to prove the WD condition but not the theorem. But if I write (35) mod 5 = 3 instead, Rodin proves the theorem but is unable to prove the (unprovable) WD condition: 0 <= (35) That behaviour is somehow inconsistent. The documentation ( http://deployeprints.ecs.soton.ac.uk/11/4/kernel_lang.pdf , page 43 ) says that the WD condition for "a mod b" is "b>0". Best regards Daniel 
From: Stephen Bryant <StephenRB<ryant@gm...>  20110822 15:42:21

Hi Matthias, Thank you for the fast and thorough response, it answered my question and gave me useful background information, Steve 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20110819 12:02:42

Hi Stephen, Am 19.08.2011 13:35, schrieb Stephen Bryant: > Hi, > > I'm still very new to both EventB and Rodin (and to some extent > predicate logic), and I have encountered an issue with inverting a > boolean variable in Rodin. The error I received was, "Syntax error: > Unexpected subformula, expected: a predicate but was: an expression". > > What I hoped to achieve is shown below: > > variable  b > invariant  b : BOOL > event action  b := not(b) > > However, this does not work. I think this is because BOOL is merely the > 'meaningless' set {TRUE,FALSE} that we then attach meaning to ourselves. Correct, although I wouldn't call {TRUE, FALSE} meaningless. For historical reasons, EventB distinguishes the two syntactical categories of predicates (e.g., true, 1 = 2, x : S) and expressions (e.g., 1, 1 + 1, A \/ B). In other communities, predicates are often designated as formulae and expressions as terms. Several years ago (I think already in the B method) it turned out to be useful to have variables ranging over booleans and also to admit sets and pairs of booleans. Therefore the type BOOL with the constants TRUE and FALSE was introduced. Note that TRUE and FALSE are expressions, while true and false are predicates. Instead of duplicating boolean connectives (such as &, , =>) and quantifiers for the type BOOL, the "casting" operator "bool" was introduced. The operator bool takes a predicate and maps it to the corresponding boolean expression. An operator casting boolean expressions to predicates needs not be introduced, because the predicate t = TRUE already corresponds to t. For example, your above action can be correctly stated as b := bool(not (b = TRUE)). But your replacement b :: BOOL \ {b} is also correct. It is hard to say which way of formalizing your action is more appropriate. In the end, you should write your specification in a way that is easy to understand both for you and the theorem provers. To find out what that means you have to experiment. Sometimes these two requirements are contradictory. Good luck, Matthias 
From: Stephen Bryant <stephen.bryant@gm...>  20110819 11:35:22

Hi, I'm still very new to both EventB and Rodin (and to some extent predicate logic), and I have encountered an issue with inverting a boolean variable in Rodin. The error I received was, "Syntax error: Unexpected subformula, expected: a predicate but was: an expression". What I hoped to achieve is shown below: variable  b invariant  b : BOOL event action  b := not(b) However, this does not work. I think this is because BOOL is merely the 'meaningless' set {TRUE,FALSE} that we then attach meaning to ourselves. I have written an alternative action that should do what I need: event action  b :: BOOL \ {b} Is this an appropriate way to achieve what I want? Is there a better way? Steve 
From: Daniel Plagge <plagge@cs...>  20110818 14:09:55

Hello Oana Ionita, we haven't ported the disprover plugin to the current Rodin version yet. So there's currently no way to install it with a uptodate version of Rodin. (For your interest: We have actually a disprover functionality in the ProB core plugin which is working  the constraint based invariant check. The disprover plugin on the other side tries to find counterexamples to specific proof obligations  but is currently not working.) Best regards Daniel On 12.08.2011 16:54, Oana Ionita wrote: > Greetings, > Greetings, > I am technical staff at a university and I was asked to install Rodin > with some plugins in a Windows lab. I am looking to install ProB > Disprover. The update site specified on the Disprover wiki is not > functional. > > http://wiki.eventb.org/index.php/Disprover > > *snip* > The ProB Disprover is available through the ProB Update Site. To Install it: > > * Go to the Update manager (Help > Software Updates...) > * Open the ProB Update Site > (http://www.stups.uniduesseldorf.de/update) > * Select all items under "ProB Disprover" > > *snip* > > Please advise. Thank you. > > Oana > >  > Get a FREE DOWNLOAD! and learn more about uberSVN rich system, > user administration capabilities and model configuration. Take > the hassle out of deploying and managing Subversion and the > tools developers use with it. > http://p.sf.net/sfu/wandiscodev2dev > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Issam Maamria <im06r@ec...>  20110815 16:23:33

Dear Rodin Users, I am delighted to announce the release of Theory v1.2. This is a bugfix release, and is only compatible with Rodin 2.2.2. 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/Theory_Plugin A help section is also provided as part of the Rodin Help Content. For further information or to report problems, please do not hesitate to contact me. *Issam Maamria* *Email:*/im06r@... <mailto:im06r@...>/ *Dependable Systems and Software Engineering Group* *School of Electronics and Computer Science* *University of Southampton* *England, UK* 
From: Oana Ionita <oana@cs...>  20110812 14:55:09

Greetings, Greetings, I am technical staff at a university and I was asked to install Rodin with some plugins in a Windows lab. I am looking to install ProB Disprover. The update site specified on the Disprover wiki is not functional. http://wiki.eventb.org/index.php/Disprover *snip* The ProB Disprover is available through the ProB Update Site. To Install it: * Go to the Update manager (Help > Software Updates...) * Open the ProB Update Site (http://www.stups.uniduesseldorf.de/update) * Select all items under "ProB Disprover" *snip* Please advise. Thank you. Oana 
From: Issam Maamria <im06r@ec...>  20110806 15:40:46

Dear Rodin Users, I am delighted to announce the release of Theory v1.1 together with the first version of the theory library. The library can be downloaded from : https://sourceforge.net/tracker/download.php?group_id=108850&atid=1558661&file_id=420425&aid=3387243 It should, then, be unzipped and copied to the MathExtensions project. It can, then, be used in model development. This first version includes: theory of sequences, inductive lists, inductive binary trees and boolean operators. This release is only compatible with Rodin 2.2.2. 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/Theory_Plugin A help section is also provided as part of the Rodin Help Content. For further information or to report problems, please do not hesitate to contact me. *Issam Maamria* *Email:*/im06r@... <mailto:im06r@...>/ *Dependable Systems and Software Engineering Group* *School of Electronics and Computer Science* *University of Southampton* *England, UK* 
From: Nicolas Beauger <nicolas.beauger@sy...>  20110801 09:00:12

Dear Rodin users, A maintenance release of Rodin is now available, please see the following page for details and upgrade: http://wiki.eventb.org/index.php/Rodin_Platform_2.2.2_Release_Notes This release contains bug fixes, most notably concerning proofs with 'ae' (more details at the bug page <http://sourceforge.net/tracker/index.php?func=detail&aid=3370087&group_id=108850&atid=651669>;). Kind regards, The Rodin Team 
From: Nicolas Beauger <nicolas.beauger@sy...>  20110801 08:36:12

Hi Chris, We have also experienced slowness accessing rodin update site (it takes about 10 minutes just to display the list of available features). We are trying to understand what is going on and find a solution . best regards, The Rodin Team Le 30/07/2011 03:26, Chris Chia a écrit : > Hi, > I have difficulties accessing > http://rodinbsharp.sourceforge.net/updates from the rodin updates. > Can you please check it? > Thanks >   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  