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: Revised Text: Actions taken: October 12, 2010: received issue Discussion: 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