[Z/EVES] A Relation domain checking problem (but FuzZ is ok)

Hi all !

I'm back again with some questions :)

I have the following (simplified) schemas:

\begin{syntax}
[A,B]
\end{syntax}
\begin{schema}{Entry}
a: A
\also
b: B
\end{schema}

\begin{schema}{MainComponent}
Map: \bag Entry
\also
Relation: A \rel B
\where
(\forall e: Entry | e \inbag Map @ Map \bcount e \leq 1)
\also
(\forall e1,e2 : Entry | e1 \neq e2 \land e1 \inbag Map \land e2
\inbag Map
@ \\
e1.a \neq e2.a \land e1.b \neq e2.b)
\also
Relation = \{e: Entry | e \in \dom Map @ (e.a, e.b)\}
\end{schema}


In the main component, I want to explicitly say that an Entry must not
be registered twice (this is the goal of the two first predicates),
and then build a relation upon the map (for convenience)

Then, in order to make a robust operation, I declare the following
operator schema:

\begin{schema}{UseRelation\_OK}
\Xi MainComponent
\also
x? : A
\also
ret! : B
\where
x? \in \dom Relation \land \\
ret! =
Relation(x?)
\end{schema}

I do not put here the UseRelation\_ERR and the final UseRelation
operator (there is no problem with)

The point: Z/EVES fails on the domain checking of UseRelation\_OK, and
ends with:

<many assertions>
\implies
\{ e\_\_5: Entry | e\_\_5 \in \dom Map @ (e\_\_5.a, e\_\_5.b) \}
applies\$to x?

Having a look into the Z Reference Manual and toolkit, I saw that
there was a disabled rule "appliesToDef[X,Y]"

I tried to use it as
=> use appliesToDef[A,B][Relation/R, x?/x];

But i only reach complicated goals, and couldn't really go further.

Does anyone have an idea to domain check this schema operator ? Or at
least what could be the problem ?
I will post any informations if needed.
Any suggestions / remarks / questions are welcome :-)

Thanks very much,

Xavier.

ps : I tried to domain check this with FuzZ, but there is no messages
nor errors...

.

Relevant Pages

  • Domain check : Express unicity in a relation definition
    ... Map: \bag Entry ... But i only reach complicated goals, ... Does anyone have an idea to domain check this schema operator? ...
    (comp.specification.z)
  • RE: Handling xml:lang attributes
    ... BizTalk produces the following XSLT code from the map: ... standard one for the "xml" prefix, ... but if the schema is re-saved in VS it ... Then create and use a BizTalk map with the "Custom XSL Path" ...
    (microsoft.public.biztalk.general)
  • Re: problem - get the @@identity in MAP
    ... this is my updategram schema structure(i.e Destination schema for Map) ... The adapter "SQL" raised an error message. ... The adapter failed to transmit message going to send port ...
    (microsoft.public.biztalk.general)
  • Re: No reference.xsd from Add Web Reference
    ... So you could either distinguish all the fields in the inbound message (for ... that you DON'T need a map. ... request schema is not generated and it does not show as an output ... Message Assignment shape to create the service request message. ...
    (microsoft.public.biztalk.general)
  • Re: problem - get the @@identity in MAP
    ... this is my updategram schema structure ... This my input schema structure(i.e Source Schema for Map) ... The adapter failed to transmit message going to send port ...
    (microsoft.public.biztalk.general)