Legacy Issue Number: 15886
Source: Institute for Defense Analyses ( Steven Wartik)
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.
Reported: QVT 1.1 — Tue, 12 Oct 2010 04:00 GMT
Updated: Tue, 22 Dec 2015 15:31 GMT