QVT13 — QVTr: Deletion semantics

I’m having trouble with the semantics of DELETE on p. 189 of the QVT Specification (v1.1). It reads in part:

FORALL OBJVAR IN MAKESET(<DOMAIN_K_VARIABLE_SET>) (
…
AND BELONGSTO(OBJVAR, MAKESET(<DOMAIN_K_VARIABLE_SET>))

I guess I don’t understand MAKESET and BELONGSTO. First of all, <DOMAIN_K_VARIABLE_SET> is already a set, so what’s the MAKESET function do? Second, the FORALL iterates OBJVAR over the results of the same MAKESET that BELONGSTO tests. So how can BELONGSTO be false? That is, I would assume BELONGSTO is defined as follows:

BELONGSTO(e, S) º e ÎS

except that under this definition the expression above is always satisfied.

Any and all help appreciated. Thank you very much.

Specification of deletion semantics

I’m having trouble with the semantics of DELETE on p. 189 of the QVT Specification (v1.1). It reads in part:

FORALL OBJVAR IN MAKESET(<DOMAIN_K_VARIABLE_SET>) (
…
AND BELONGSTO(OBJVAR, MAKESET(<DOMAIN_K_VARIABLE_SET>))

I guess I don’t understand MAKESET and BELONGSTO. First of all, <DOMAIN_K_VARIABLE_SET> is already a set, so what’s the MAKESET function do? Second, the FORALL iterates OBJVAR over the results of the same MAKESET that BELONGSTO tests. So how can BELONGSTO be false? That is, I would assume BELONGSTO is defined as follows:

BELONGSTO(e, S) º e ÎS

except that under this definition the expression above is always satisfied.

Any and all help appreciated. Thank you very much.

Discussion

Well this is very embarrassing. I don't understand it all either, and I certainly do not understand why it is not written using OCL.

I'm not convinced that QVTr has any delete semantics since declaratively delete occurs as an absence of creation.

Must await the Eclipse QVTr prototype.