Groups | Search | Server Info | Login | Register

Groups > comp.specification.z > #366

Re: assertions about parts of schema

Show all headers | View raw

On Saturday, March 30, 2013 8:02:31 PM UTC, David Lamb wrote:
> I have a situation that corresponds roughly to:
> 
> 
> 
> \begin{schema}{Small} x1: ...; xn: ... \end{schema}
> 
> \begin{schema}{Big}
> 
> Small \\
> 
> ... \end{schema}
> 
> 
> 
> \begin{schema}{Other}
> 
> v1: Big;
> 
> v2: Big
> 
> \where
> 
> % v1's variables defined in Small equal v2's variables defined in small
> 
> \end{schema}
> 
> 
> 
> However, I don't know how to write the assertion in the comment. It 
> 
> seems to me I ought to be able to use \project and perhaps \theta 
> 
> somehow but I've not understood those portions of Z well enough, and 
> 
> keep getting syntax errors in fuzz with various things I try. I'd rather 
> 
> not resort to
> 
> v1.x1 = v2.x2 \land ... \land v1.xn = v2.xn
> 
> 
> 
> Any suggestions?


Assuming you meant to say

  v1.x1 = v2.x1 \land ... \land v1.xn = v2.xn
              ^

(note difference indicated by ^) then how about just writing

  v1 = v2

Back to comp.specification.z | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

assertions about parts of schema David Lamb <dalamb@cs.queensu.ca> - 2013-03-30 16:02 -0400
  Re: assertions about parts of schema phil.clayton@lineone.net - 2013-04-02 14:01 -0700
    Re: assertions about parts of schema David Lamb <dalamb@cs.queensu.ca> - 2013-04-02 21:17 -0400
      Re: assertions about parts of schema phil.clayton@lineone.net - 2013-04-03 14:29 -0700
        Re: assertions about parts of schema phil.clayton@lineone.net - 2013-04-03 15:34 -0700
          Re: assertions about parts of schema phil.clayton@lineone.net - 2013-04-03 23:41 -0700
        Re: assertions about parts of schema David Lamb <dalamb@cs.queensu.ca> - 2013-04-04 17:08 -0400
          Re: assertions about parts of schema phil.clayton@lineone.net - 2013-04-04 15:01 -0700
            Re: assertions about parts of schema David Lamb <dalamb@cs.queensu.ca> - 2013-04-04 20:37 -0400

csiph-web