#781 Problem with the Rodin proof generator

[STEVE JEFFREY TUENO FOTSO]

Hello,

The attached archive is a Rodin project that formalises translation rules between SysML/KAOS ontologies and ClearSy B System specifications.
Machine eventbspecsfromontologiesref1 is focussed on rules that generate or update B System logical formulas. It defines an event rule910 which makes use of boolean functions and ⇒ as a way to introduce If-then-Else substitutions to avoid several events that differ slightly.

For instance, a parameter oASc is defined as either an element of variable set Constant ( @grd2), where Constant⊆Constant_Set, or an element of ConstantSet ∖ Constant ( @grd4).

 @grd2 AS ∈ dom(Concept_corresp_Constant) ⇒  o_AS_c = Concept_corresp_Constant(AS)
      @grd3 AS ∈ dom(Concept_corresp_Variable) ⇒  o_AS_v = Concept_corresp_Variable(AS)
      @grd4 AS ∉ (dom(Concept_corresp_Constant)∪dom(Concept_corresp_Variable)) ⇒  (
            (Concept_isVariable(AS)=FALSE ⇒ ((Constant_Set ∖ Constant ≠∅) ∧ (o_AS_c ∈ Constant_Set ∖ Constant)))
            ∧ (Concept_isVariable(AS)=TRUE ⇒ ((Variable_Set ∖ Variable ≠∅) ∧ (o_AS_v ∈ Variable_Set ∖ Variable)))
        )

The substitution @act15 adds in variable set ConstantisInvolvedInLogicFormulas a set ({TRUE↦{o_AS_c↦Constant_isInvolvedIn_LogicFormulas(o_AS_c)∪{1↦o_lg_item}}, FALSE↦ ∅}(bool(AS ∈ dom(Concept_corresp_Constant))))}

However, the generated well definedness proof obligation * rule_9_10/act15/WD* requires to prove that o_AS_c∈dom(Constant_isInvolvedIn_LogicFormulas) instead of AS ∈ dom(Concept_corresp_Constant)⇒o_AS_c∈dom(Constant_isInvolvedIn_LogicFormulas).

Here is the full body of @act15:

@act15 Constant_isInvolvedIn_LogicFormulas≔  Constant_isInvolvedIn_LogicFormulas (
             ({TRUE↦{T_AS_c↦{1↦o_lg_type, 2↦o_lg_item}}, FALSE↦ ∅}(bool(Concept_isVariable(CO1)=FALSE ∧ Concept_isVariable(CO2)=FALSE)))
            ∪ ({TRUE↦({TRUE↦{o_AS_c↦{1↦o_lg_item}}, FALSE↦ ∅}(bool(Concept_isVariable(AS)=FALSE))), FALSE↦ ({TRUE↦{o_AS_c↦Constant_isInvolvedIn_LogicFormulas(o_AS_c)∪{1↦o_lg_item}}, FALSE↦ ∅}(bool(AS ∈ dom(Concept_corresp_Constant))))}(bool(AS ∉ (dom(Concept_corresp_Constant)∪dom(Concept_corresp_Variable)))))
            ∪ ({TRUE↦({TRUE↦({TRUE↦{o_CO1_c↦Constant_isInvolvedIn_LogicFormulas(o_CO1_c)∪({1, 2}×{o_lg_type})},
            FALSE↦ {o_CO1_c↦Constant_isInvolvedIn_LogicFormulas(o_CO1_c)∪{1↦o_lg_type}, o_CO2_c↦Constant_isInvolvedIn_LogicFormulas(o_CO2_c)∪{2↦o_lg_type}}}(bool(CO1=CO2))),
            FALSE↦ {o_CO1_c↦Constant_isInvolvedIn_LogicFormulas(o_CO1_c)∪{1↦o_lg_type}}}(bool(CO2∈ dom(Concept_corresp_Constant)))),
            FALSE↦ ({TRUE↦{o_CO2_c↦Constant_isInvolvedIn_LogicFormulas(o_CO2_c)∪{2↦o_lg_type}}, FALSE↦ ∅}(bool(CO2∈ dom(Concept_corresp_Constant))))}(bool(CO1∈ dom(Concept_corresp_Constant))))
        )

Best regards,
Steve

[STEVE JEFFREY TUENO FOTSO]

Please, consider:
event_b_specs_from_ontologies_ref_1 instead of eventbspecsfromontologiesref1 ,
rule_9_10 instead of rule910,
Constant_Set instead of ConstantSet,
Constant_isInvolvedIn_LogicFormulas instead of ConstantisInvolvedInLogicFormulas,
and o_AS_c instead of oASc.

I think there is a problem with the text editor when applying italic formatting: the '_' are deleted.

[Laurent Voisin]

Dear Steve, you should rather use code quoting like this for event and variable names in ticket messages. This would avoid the issue with _ characters.

I am having a look at your issue.

[Michael Leuschel]

Dear Steve

You can also write something like
(%(dummy).(dummy=0 & x>0|1/x)\/%(dummy).(dummy =0 & not(x>0)|0)) (0)
instead of
{TRUE ↦ 1÷x, FALSE ↦ 0}(bool(x ≠ 0))

The lambda construction is well-defined (but not very readable by a human) and ProB transforms this form internally into an expression
(IF x > 0 THEN 1 ÷ x ELSE 0 END)

Greetings,
Michael

On 28 Feb 2019, at 13:33, Laurent Voisin lvoisin@users.sourceforge.net wrote:

For instance, writing {TRUE ↦ 1÷x, FALSE ↦ 0}(bool(x ≠ 0)) is ill-defined in Event-B when x can be null. The associated WD proof obligation is ¬ x=0.

Note that if you use the Theory plug-in, then you can define some generic operator that are non-WD strict and thus implement generalised if then else-like operators.

[Michael Leuschel]

Dear Steve,

the syntax I wrote was classical B; in Rodin you have to write the lambda slightly differently:
context ifte_wd_test
constants x c
axioms
@axm0 x=0
@axm1 c = ((λdummy·dummy=0 ∧ x>0∣1÷x) ∪ (λdummy·dummy =0 ∧ ¬(x>0)∣0)) (0)
theorem @thm1 c=0
end

The WD PO is proven automatically.

Michael

PS: The lambda translation was introduced by Dominik Hansen in the translation of TLA+ to B; TLA+ has an if-then-else for expressions.

On 28 Feb 2019, at 14:37, Michael Leuschel mleuschel@users.sourceforge.net wrote:

Dear Steve

You can also write something like
(%(dummy).(dummy=0 & x>0|1/x)\/%(dummy).(dummy =0 & not(x>0)|0)) (0)
instead of
{TRUE ↦ 1÷x, FALSE ↦ 0}(bool(x ≠ 0))

The lambda construction is well-defined (but not very readable by a human) and ProB transforms this form internally into an expression
(IF x > 0 THEN 1 ÷ x ELSE 0 END)

Greetings,
Michael

On 28 Feb 2019, at 13:33, Laurent Voisin lvoisin@users.sourceforge.net lvoisin@users.sourceforge.net wrote:

For instance, writing {TRUE ↦ 1÷x, FALSE ↦ 0}(bool(x ≠ 0)) is ill-defined in Event-B when x can be null. The associated WD proof obligation is ¬ x=0.

Note that if you use the Theory plug-in, then you can define some generic operator that are non-WD strict and thus implement generalised if then else-like operators.

[ https://sourceforge.net/p/rodin-b-sharp/bugs/781/

[Laurent Voisin]

As soon as you have the formula Constant_isInvolvedIn_LogicFormulas(o_AS_c) in a strict position (i.e., not protected by a Boolean shortcut operator such as => or &, it is normal that WD requires that o_AS_c ∈ dom(Constant_isInvolvedIn_LogicFormulas). The application of a Boolean function is a strict operation, and thus requires that both operands are well-defined independently of each other.

In other words this function application is not equivalent to an if then else operator as found in functional languages.

For instance, writing {TRUE ↦ 1÷x, FALSE ↦ 0}(bool(x ≠ 0)) is ill-defined in Event-B when x can be null. The associated WD proof obligation is ¬ x=0.

Note that if you use the Theory plug-in, then you can define some generic operator that are non-WD strict and thus implement generalised if then else-like operators.