Issue 15886: Specification of deletion semantics (qvt-rtf) Source: Institute for Defense Analyses (Dr. Steven Wartik, swartik(at)ida.org) Nature: Uncategorized Issue Severity: Summary: 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. Resolution: 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. Revised Text: Actions taken: October 12, 2010: received issue December 22, 2015: Deferred March 29, 2016: closed issue Discussion: I see no justification for not using OCL to express the Annex B semantic. The OCL could then form part of real tests. I see little prospect of progress here till we have a conformant working QVTr implementation. Disposition: Deferred End of Annotations:===== m: "Wartik, Steven P \"Steve\"" To: "'qvt-rtf@omg.org'" Date: Tue, 12 Oct 2010 17:40:59 -0400 Subject: Specification of deletion semantics Thread-Topic: Specification of deletion semantics Thread-Index: ActqViieYwuH84aZT76Gqg5wavbcLQ== Accept-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: acceptlanguage: en-US Hi, 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() ( . AND BELONGSTO(OBJVAR, MAKESET()) I guess I don.t understand MAKESET and BELONGSTO. First of all, 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 ÃŽ except that under this definition the expression above is always satisfied. Any and all help appreciated. Thank you very much. Steve Wartik The Institute for Defense Analyses Arlington, Virginia swartik@ida.org From: "Rouquette, Nicolas F (313K)" To: Juergen Boldt CC: "Wartik, Steven P Steve" , "qvt-rtf@omg.org" Date: Mon, 27 Dec 2010 12:30:09 -0800 Subject: Re: Specification of deletion semantics Thread-Topic: Specification of deletion semantics Thread-Index: AcumBNs99o/9ghZ4SmOQhUM2LJvEYw== Accept-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: acceptlanguage: en-US X-Source-IP: altvirehtstap01.jpl.nasa.gov [128.149.137.72] X-Source-Sender: nicolas.f.rouquette@jpl.nasa.gov X-AUTH: Authorized Juergen, Definitely yes! Thanks Steven for catching this! Issue: The operators used in the predicate calculus descriptions of the semantics of QVT relations in Annex B need to be explicitly defined. Some operators like 'minus' and 'union' seem to correspond to the synonyms of OCL operators described in clause 8.3.2; however, it is unclear if this is intentional because clause 8 is about QVTo whereas Annex B is about QVTr. Steven caught one case where two operators, 'makeSet' and 'belongsTo' in clause B.5 are undefined. This issue applies to QVT1.0, formal/2008-04-03 and to SMSC review of QVT1.1, i.e., smsc/10-11-01. - Nicolas. On Dec 27, 2010, at 10:56 AM, Juergen Boldt wrote: issue? -Juergen At 04:40 PM 10/12/2010, Wartik, Steven P \"Steve\" wrote: Hi, 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() (ND BELONGSTO(OBJVAR, MAKESET()) I guess I don.t understand MAKESET and BELONGSTO. First of all, 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 ÃŽ except that under this definition the expression above is always satisfied. Any and all help appreciated. Thank you very much. Steve Wartik The Institute for Defense Analyses Arlington, Virginia swartik@ida.org