Re: [Rodin-b-sharp-user] Well-Definedness of modulo

[Daniel P. <pl...@cs...>]

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 (3-5). :)

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
> Event-B. Is somebody out there actually using it? Please send me an email!
>
>   >  That behaviour is somehow inconsistent. The documentation (
>   >  http://deploy-eprints.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/tech-reports/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
>> (3-5) mod 5 = 3
>> instead, Rodin proves the theorem but is unable to prove the
>> (unprovable) WD condition:
>> 0<= (3-5)
> There are two reasons why you can prove the theorem PO. First, it
> includes the (false) hypothesis 0<= (3-5). Second, it has the
> ill-defined goal (3-5) mod 5 = 3. Proof obligations with an ill-defined
> 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 world-class log management solution at an even better
> price-free! And you'll get a free "Love Thy Logs" t-shirt when you
> download Logger. Secure your free ArcSight Logger TODAY!
> http://p.sf.net/sfu/arcsisghtdev2dev
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user