Rodin User’s Handbook v.2.8: Witness Xyz must be a disappearing abstract variable or parameter in the INITIALISATION event

Rodin Handbook

This work is sponsored by the Deploy Project

This work is sponsored by the ADVANCE Project

Creative Commons License

This work is licensed under a Creative Commons Attribution 3.0 Unported License

Witness Xyz must be a disappearing abstract variable or parameter in the INITIALISATION event

Rodin User’s Handbook v.2.8

4.3.3 Witness Xyz must be a disappearing abstract variable or parameter in the INITIALISATION event

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.

Rodin User’s Handbook v.2.8 : Frequently Asked Questions : Modelling : Witness Xyz must be a disappearing abstract variable or parameter in the INITIALISATION event