Rodin Handbook





 
Previous: In INITIALISATION, I get Witness Xyz must be a disappearing abstract variable or parameter Up: Modeling Next: How can I create a new Event-B Project? User Manual for Rodin v.2.3

Feedback

4.3.4 I’ve added a witness for Xyz but it keeps saying “Identifier Xyz has not been defined”

As specified in the 3.2.3.4.4 section, the witness must be labelled by the name Xyz of the concrete variable being concerned.

Previous: In INITIALISATION, I get Witness Xyz must be a disappearing abstract variable or parameter Up: Modeling Next: How can I create a new Event-B Project?  
User Manual for Rodin v.2.3 : Frequently Asked Questions : Modeling : I’ve added a witness for Xyz but it keeps saying “Identifier Xyz has not been defined”