Rodin Handbook





 
Previous: Identifier Xyz should not occur free in a witness Up: Modeling Next: I’ve added a witness for Xyz but it keeps saying “Identifier Xyz has not been defined” User Manual for Rodin v.2.3

Feedback

4.3.3 In INITIALISATION, I get Witness Xyz must be a disappearing abstract variable or parameter

The witness is for the after value of the abstract variable, hence you should use the primed variable. The witness label should be Xyz’, and the predicate should refer to Xyz’ too.

Previous: Identifier Xyz should not occur free in a witness Up: Modeling Next: I’ve added a witness for Xyz but it keeps saying “Identifier Xyz has not been defined”  
User Manual for Rodin v.2.3 : Frequently Asked Questions : Modeling : In INITIALISATION, I get Witness Xyz must be a disappearing abstract variable or parameter