Back - User Guide Index | Previous - Editor Overview | Next - Printing - Microsoft Word

Entering Specifications - Examples

 

The following is some example fragments of Z together with a step by step guide how to enter them in the document editor.

Please note these are examples are for purely entering specifications and are not meant to be consistent.

Create a new document as described in "The Formaliser Library" and open it for editing in the document editor window. You should be presented with a blank document containing only one "<Paragraph>".

Each example will need a separate paragraph. To add more paragraphs, highlight the paragraph and select "Append Node" from the Edit menu, this will insert another paragraph after the current one. Repeat this for as many paragraphs as you need. Note - after adding the first one, CTRL-y repeats the last action and so is a quick way of adding several paragraphs.

Every action selected from the Edit menu can also be selected using the pop up menu.

You will see that entering some of the more complicated constructs requires quite a few steps, in these cases it will be easier to type in the details once the basic construct has been defined.

Inclusion

Parent Section: "Z2 Toolkit"
  1. Highlight <Paragraph>; choose Instantiate... from Edit menu and select Inclusion.
  2. Highlight <DocumentName>; choose Choose Terminal... from Edit menu and select Z2 Toolkit.

Definition

Scotland == {(Edinburgh,8),(Glasgow,7),(Aberdeen,6)}
  1. Highlight <Paragraph>; choose Instantiate... from Edit menu and select x==E.
  2. Highlight <DefLhs>; type in Scotland and press enter.
  3. Highlight <Expression>; choose Instantiate... from Edit menu and select {s,e,t}.
  4. Highlight <Expression>; choose Instantiate... from Edit menu and select (x,y,z).
  5. Highlight (<Expression>,<Expression>); choose Twin Node from Edit menu.
  6. Repeat this for the third tuple by typing CTRL-y.
  7. Highlight first <Expression>; type in Edinburgh and press enter.
  8. Highlight next <Expression>; type in 8 and press enter.
  9. Repeat the last two steps for the tuples for Glasgow and Aberdeen as above.

Given Sets

[SETTING,VALUE]
  1. Highlight <Paragraph>; choose Instantiate... from Edit menu and select [X,Y].
  2. Highlight <Stroke> and press enter to remove it.
  3. Highlight <Word> and choose Append Node from Edit menu.
  4. Remove <Stroke> as in step two.
  5. Highlight the first <Word>; type SETTING and press enter.
  6. Highlight the second <Word>; type VALUE and press enter.

Free Type Definition

BUTTON ::= accept | cancel
  1. Highlight <Paragraph>; choose Instantiate... from Edit menu and select F::=c|<<X>>.
  2. Highlight <Stroke> and press enter to remove it.
  3. Highlight <Branch> and select Insert Node from Edit menu.
  4. Highlight <Word>; type BUTTON and press enter.
  5. Highlight the first <Branch>; type accept and press enter.
  6. Highlight the second <Branch>; type cancel and press enter.

Schema Box

ÚÄExampleSchemaÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
new? : p1 p2
measured,prescribed : SETTING VALUE
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
" p1,p2 : dom queues | p1 p2 ran (queues p1) ran (queues p2) = í
display' = display Å {new? event}
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ
  1. Highlight <Paragraph>; choose Instantiate... from Edit menu and select SchemaBox.
  2. Highlight [<Word><Stroke>] and press enter to remove it.
  3. Highlight <BasicDecl>; choose Instantiate... from Edit menu and select x,y:E.
  4. Highlight <DeclName> : <Expression> and choose Twin Node from Edit menu.
  5. Highlight <Predicate> and choose Insert Node from Edit menu.

This gives us the basic outline of the schema. Now follows a guide to entering each line.

Line 1

  1. Highlignt <Expression>; choose Instantiate... from Edit menu and select XxYxZ.
  2. Highlight <DeclName>; type new? and press enter.
  3. Highlight the first <Expression2>; type p1 and press enter.
  4. Highlight the second <Expression2>; type p2 and press enter.

Line 2

  1. Highlignt <Expression>; choose Instantiate... from Edit menu and select X-->Y.
  2. Highlight <Stroke> and press enter to remove it.
  3. Highlight <DeclName> and choose Insert Node from Edit menu.
  4. Highlight <InGen>; choose Choose Terminal... from Edit menu and select .
  5. Highlight the first <DeclName>; type measured and press enter.
  6. Highlight the second <DeclName>; type prescribed and press enter.
  7. Highlight the first <Expression1>; type SETTING and press enter.
  8. Highlight the second <Expression1>; type VALUE and press enter.

Line 3

  1. Highlignt <Predicate>; choose Instantiate... from Edit menu and select forall.
  2. Highlignt <OptPredicate>; choose Instantiate... from Edit menu and select SchemaPredicate.
  3. Highlignt <BasicDecl>; click on <BasicDecl>+ in the production pane.
  4. Highlignt <BasicDecl>; choose Instantiate... from Edit menu and select x,y:E.
  5. Highlignt <DeclName> and choose Append Node from Edit menu.
  6. Highlight the first <DeclName>; type p1 and press enter.
  7. Highlight the second <DeclName>; type p2 and press enter.
  8. Highlight <Expression>; type dom queues and press enter.
  9. Highlignt the first <Predicate>; choose Instantiate... from Edit menu and select x=y.
  10. Highlight <Rel>; choose Instantiate... from Edit menu and select InRel.
  11. Highlight <InRel>; choose Choose Terminal... from Edit menu and select .
  12. Highlight <Stroke> and press enter to remove it.
  13. Highlight the first <Expression>; type p1 and press enter.
  14. Highlight the second <Expression>; type p2 and press enter.
  15. Highlignt <Predicate>; choose Instantiate... from Edit menu and select x=y.
  16. Highlight <Rel>; type = and press enter.
  17. Highlignt the first <Expression>; choose Instantiate... from Edit menu and select x+y.
  18. Highlight <Stroke> and press enter to remove it.
  19. Highlight <InFun>; choose Choose Terminal... from Edit menu and select Ç .
  20. Highlignt the first <Expression2>; type ran (queues p1) and press enter.
  21. Highlignt the second <Expression2>; type ran (queues p2) and press enter.
  22. Highlignt <Expression>; type Æ and press enter.

Line 4

  1. Highlignt <Predicate>; choose Instantiate... from Edit menu and select x=y.
  2. Highlight <InGen>; type = and press enter.
  3. Highlight the first <Expression>; type display' and press enter.
  4. Highlignt the second <Expression>; choose Instantiate... from Edit menu and select x+y.
  5. Highlight <Stroke> and press enter to remove it.
  6. Highlight <InFun>; choose Choose Terminal... from Edit menu and select Å .
  7. Highlignt the first <Expression2>; type display and press enter.
  8. Highlignt the second <Expression2>; choose Instantiate... from Edit menu and select {s,e,t}.
  9. Highlignt <Expression>; choose Instantiate... from Edit menu and select x+y.
  10. Highlight <Stroke> and press enter to remove it.
  11. Highlight <InFun>; choose Choose Terminal... from Edit menu and select .
  12. Highlignt the first <Expression2>; type new? and press enter.
  13. Highlignt the second <Expression2>; type event and press enter.

Schema Definition

RExampleSchema ExampleSchema <SchemaExp7>
  1. Highlight <Paragraph>; choose Instantiate... from Edit menu and select S=^=....
  2. Highlight [<Word><Stroke>] and press enter to remove it.
  3. Highlight <SchemaExp>; choose Instantiate... from Edit menu and select S\/S.
  4. Highlight <SchemaName>; type RexampleSchema and press enter.
  5. Highlight <SchemaExp6>; type ExampleSchema and press enter.

Note - <SchemaExp7> is left uninstantiated this is because these must be previously declared schemas and since we have no more that have been declared the parser will not allow anything to be entered here.