--- /dev/null
+/**\r
+ * Action class\r
+ * Represents an action performed in response to a token\r
+ * Instance of command pattern\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/06/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.util.*;\r
+\r
+public /*abstract*/ class Action {\r
+ /**\r
+ * requires: iter is an iterator that just yielded this\r
+ * ensures: performs action for token, and may remove itself from iter\r
+ * default behaviour is equivalent to perform\r
+ */\r
+ public void perform (Token token, Iterator iter) {\r
+ perform (token);\r
+ }\r
+\r
+ public void perform (Token token) {\r
+ ;\r
+ }\r
+}\r
+\r
+public class ParagraphAction extends Action {\r
+ boolean first_para;\r
+\r
+ Generator generator;\r
+ StringBox current_para_style;\r
+ Numbering numbering;\r
+ public ParagraphAction( Generator g, \r
+ StringBox cps,\r
+ Numbering n) {\r
+ generator = g;\r
+ current_para_style = cps;\r
+ numbering = n;\r
+ first_para = true;\r
+ } \r
+\r
+ public void perform (Token t, Iterator iter) {\r
+ if (t.type != Token.PARASTYLECOMMAND()) {\r
+ if (!first_para) generator.linefeed ();\r
+ generator.new_para (current_para_style.string);\r
+ String numstr = numbering.get_numbering_string (current_para_style.string);\r
+ if (numstr.length() != 0) {\r
+ // display numbering as evidence of progress\r
+ System.out.println (numstr);\r
+ generator.plaintext (numstr);\r
+ }\r
+ \r
+ iter.remove ();\r
+ first_para = false;\r
+ }\r
+ }\r
+}\r
+\r
+public class PlaintextAction extends Action {\r
+ Generator generator;\r
+ public PlaintextAction( Generator g ) {\r
+ generator = g;\r
+ }\r
+\r
+ public void perform(Token t) {\r
+ generator.plaintext (t.arg);\r
+ }\r
+}\r
+\r
+public class NewlineAction extends Action {\r
+ Generator generator;\r
+ public NewlineAction( Generator g ) {\r
+ generator = g;\r
+ }\r
+\r
+ public void perform(Token t) {\r
+ generator.new_line ();\r
+ }\r
+}\r
+\r
+public class ApostropheAction extends Action {\r
+ Generator generator;\r
+ PropertyMap char_map;\r
+ public ApostropheAction( Generator g,\r
+ PropertyMap cm) {\r
+ generator = g;\r
+ char_map = cm;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ StandardEngine.put_special_char (generator, \r
+ char_map, \r
+ StandardEngine.apostrophe_char_name(), \r
+ t.line);\r
+ }\r
+}\r
+\r
+public class PrimeAction extends Action {\r
+ Generator generator;\r
+ PropertyMap char_map;\r
+ public PrimeAction( Generator g,\r
+ PropertyMap cm) {\r
+ generator = g;\r
+ char_map = cm;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ StandardEngine.put_special_char (generator, \r
+ char_map, \r
+ StandardEngine.prime_char_name(), \r
+ t.line);\r
+ } \r
+}\r
+\r
+public class OpenSingleQuoteAction extends Action {\r
+ Generator generator;\r
+ PropertyMap char_map;\r
+ public OpenSingleQuoteAction( Generator g,\r
+ PropertyMap cm) {\r
+ generator = g;\r
+ char_map = cm;\r
+ }\r
+ \r
+ public void perform (Token t) {\r
+ StandardEngine.put_special_char (generator, \r
+ char_map, \r
+ StandardEngine.opensinglequote_char_name(), \r
+ t.line);\r
+ } \r
+}\r
+\r
+public class CloseSingleQuoteAction extends Action {\r
+ Generator generator;\r
+ PropertyMap char_map;\r
+ public CloseSingleQuoteAction( Generator g,\r
+ PropertyMap cm) {\r
+ generator = g;\r
+ char_map = cm;\r
+ }\r
+ \r
+ public void perform (Token t) {\r
+ StandardEngine.put_special_char (generator, \r
+ char_map, \r
+ StandardEngine.closesinglequote_char_name(), \r
+ t.line);\r
+ } \r
+}\r
+\r
+public class OpenDoubleQuoteAction extends Action {\r
+ Generator generator;\r
+ PropertyMap char_map;\r
+ public OpenDoubleQuoteAction( Generator g,\r
+ PropertyMap cm) {\r
+ generator = g;\r
+ char_map = cm;\r
+ }\r
+ \r
+ public void perform (Token t) {\r
+ StandardEngine.put_special_char (generator, \r
+ char_map, \r
+ StandardEngine.opendoublequote_char_name(), \r
+ t.line);\r
+ } \r
+}\r
+\r
+public class CloseDoubleQuoteAction extends Action {\r
+ Generator generator;\r
+ PropertyMap char_map;\r
+ public CloseDoubleQuoteAction( Generator g,\r
+ PropertyMap cm) {\r
+ generator = g;\r
+ char_map = cm;\r
+ }\r
+ \r
+ public void perform (Token t) {\r
+ StandardEngine.put_special_char (generator, \r
+ char_map, \r
+ StandardEngine.closedoublequote_char_name(), \r
+ t.line);\r
+ } \r
+}\r
+\r
+public class HyphenAction extends Action {\r
+ Generator generator;\r
+ PropertyMap char_map;\r
+ public HyphenAction( Generator g,\r
+ PropertyMap cm ) {\r
+ generator = g;\r
+ char_map = cm;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ int len = t.arg.length ();\r
+ if (len == 1)\r
+ StandardEngine.put_special_char (generator, \r
+ char_map, \r
+ StandardEngine.hyphen_char_name(), \r
+ t.line);\r
+ else if (len == 2)\r
+ StandardEngine.put_special_char (generator, \r
+ char_map, \r
+ StandardEngine.endash_char_name(), \r
+ t.line);\r
+ else if (len == 3)\r
+ StandardEngine.put_special_char (generator, \r
+ char_map, \r
+ StandardEngine.emdash_char_name(),\r
+ t.line);\r
+ else\r
+ System.out.println (t.line + ": Too many hyphens: " + t.arg);\r
+ }\r
+}\r
+\r
+public class DotsAction extends Action {\r
+ Generator generator;\r
+ PropertyMap char_map;\r
+ public DotsAction( Generator g,\r
+ PropertyMap cm ) {\r
+ generator = g;\r
+ char_map = cm;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ int len = t.arg.length ();\r
+ if (len == 1)\r
+ generator.plaintext (".");\r
+ else if (len == 2)\r
+ StandardEngine.put_special_char (generator, \r
+ char_map, \r
+ StandardEngine.twodotleader_char_name(), \r
+ t.line);\r
+ else if (len == 3)\r
+ StandardEngine.put_special_char (generator, \r
+ char_map, \r
+ StandardEngine.ellipsis_char_name(), \r
+ t.line);\r
+ else\r
+ System.out.println (t.line + ": Too many dots: " + t.arg);\r
+ }\r
+}\r
+\r
+public class LoadCharMapCommandAction extends Action {\r
+ Generator generator;\r
+ PropertyMap char_map;\r
+ Numbering numbering;\r
+\r
+ public LoadCharMapCommandAction( Generator g,\r
+ PropertyMap cm,\r
+ Numbering n ) {\r
+ generator = g;\r
+ char_map = cm;\r
+ numbering = n;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ // open file with given name and load char map from it\r
+ String file_name = t.arg;\r
+ FileInputStream s = new FileInputStream (file_name);\r
+ PropertyParser p = new PropertyParser (s);\r
+ char_map.incorporate (p);\r
+ }\r
+}\r
+\r
+public class LoadStyleSheetCommandAction extends Action {\r
+ Generator generator;\r
+ PropertyMap style_map;\r
+ Numbering numbering;\r
+\r
+ public LoadStyleSheetCommandAction( Generator g,\r
+ PropertyMap sm,\r
+ Numbering n ) {\r
+ generator = g;\r
+ style_map = sm;\r
+ numbering = n;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ // open file with given name and load char map from it\r
+ String file_name = t.arg;\r
+ FileInputStream s = new FileInputStream (file_name);\r
+ PropertyParser p = new PropertyParser (s);\r
+ style_map.incorporate (p);\r
+ numbering.incorporate ();\r
+ }\r
+}\r
+\r
+public class UnsuppressAction extends Action {\r
+ Generator generator;\r
+ \r
+ public UnsuppressAction( Generator g ) {\r
+ generator = g;\r
+ }\r
+\r
+ public void perform (Token t, Iterator i) {\r
+ generator.suppress_off ();\r
+ i.remove ();\r
+ }\r
+}\r
+\r
+public class PreambleCommandAction extends Action {\r
+ Generator generator;\r
+ Action unsuppress_action;\r
+ StandardEngine engine;\r
+\r
+ public PreambleCommandAction( Generator g,\r
+ Action ua,\r
+ StandardEngine se ) {\r
+ generator = g;\r
+ unsuppress_action = ua;\r
+ engine = se;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ generator.suppress_on ();\r
+ engine.register_by_type (unsuppress_action, Token.PARABREAK());\r
+ }\r
+}\r
+\r
+public class ParaBreakAction extends Action {\r
+ Action paragraph_action;\r
+ StringBox current_para_style;\r
+ PropertyMap style_map;\r
+\r
+ public ParaBreakAction( Action pa,\r
+ StringBox cps,\r
+ PropertyMap sm ) {\r
+ paragraph_action = pa;\r
+ current_para_style = cps;\r
+ style_map = sm;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ String next_style = style_map.get_property (current_para_style.string, \r
+ StandardEngine.next_style_prop_name());\r
+ if (next_style == null) {\r
+ System.out.println (t.line + ": No next style property given for style: " + current_para_style.string);\r
+ return;\r
+ }\r
+ current_para_style.set (next_style);\r
+ StandardEngine.register_for_all (paragraph_action);\r
+ }\r
+}\r
+\r
+public class ParaStyleCommandAction extends Action {\r
+ StringBox current_para_style;\r
+\r
+ public ParaStyleCommandAction( StringBox cps ) {\r
+ current_para_style = cps;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ current_para_style.set (t.arg);\r
+ }\r
+}\r
+\r
+public class CharCommandAction extends Action {\r
+ Generator generator;\r
+ PropertyMap char_map;\r
+ \r
+ public CharCommandAction( Generator g,\r
+ PropertyMap cm ) {\r
+ generator = g;\r
+ char_map = cm;\r
+ }\r
+ \r
+ public void perform (Token t) {\r
+ String index = char_map.get_property (t.arg, \r
+ StandardEngine.index_prop_name());\r
+ if (index == null) {\r
+ System.out.println (t.line + ": No index property given for character: " + t.arg);\r
+ return;\r
+ }\r
+ String font = char_map.get_property (t.arg, \r
+ StandardEngine.font_prop_name());\r
+ // if no font is listed, generate special character in standard font\r
+ if (font == null)\r
+ generator.special_char (index);\r
+ else\r
+ generator.special_char (font, index);\r
+ } \r
+}\r
+\r
+public class UnderscoreAction extends Action {\r
+ Generator generator;\r
+ boolean italic_mode_on;\r
+ \r
+ public UnderscoreAction( Generator g ) {\r
+ generator = g;\r
+ italic_mode_on = false;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ if (italic_mode_on) {\r
+ italic_mode_on = false;\r
+ generator.pop_format ();\r
+ }\r
+ else {\r
+ italic_mode_on = true;\r
+ generator.push_format (Generator.ITALICS());\r
+ }\r
+ } \r
+}\r
+\r
+public class PushItalicsAction extends Action {\r
+ Generator generator;\r
+ \r
+ public PushItalicsAction( Generator g ) {\r
+ generator = g;\r
+ }\r
+\r
+ public void perform (Token t, Iterator iter) {\r
+ Assert.assert_ (t.type == Token.ALPHABETIC());\r
+ generator.push_format (Generator.ITALICS());\r
+ }\r
+}\r
+\r
+public class PopItalicsAction extends Action {\r
+ Generator generator;\r
+ \r
+ public PopItalicsAction( Generator g ) {\r
+ generator = g;\r
+ }\r
+\r
+ public void perform (Token t, Iterator iter) {\r
+ Assert.assert_ (t.type == Token.ALPHABETIC());\r
+ generator.pop_format ();\r
+ }\r
+}\r
+\r
+public class DollarAction extends Action {\r
+ Action push_italics_action;\r
+ Action pop_italics_action;\r
+ boolean math_mode_on;\r
+\r
+ public DollarAction( Action pushia, Action popia ) {\r
+ push_italics_action = pushia;\r
+ pop_italics_action = popia;\r
+ math_mode_on = false;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ if (math_mode_on) {\r
+ math_mode_on = false;\r
+ StandardEngine.unregister_by_type (push_italics_action, Token.ALPHABETIC());\r
+ StandardEngine.unregister_by_type (pop_italics_action, Token.ALPHABETIC());\r
+ }\r
+ else {\r
+ math_mode_on = true;\r
+ StandardEngine.register_by_type_back (pop_italics_action, Token.ALPHABETIC());\r
+ StandardEngine.register_by_type_front (push_italics_action, Token.ALPHABETIC());\r
+ }\r
+ } \r
+}\r
+\r
+public class FormatCommandAction extends Action {\r
+ Generator generator;\r
+\r
+ public FormatCommandAction( Generator g ) {\r
+ generator = g;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ if (t.arg.equals (StandardEngine.ROMAN_COMMANDNAME()))\r
+ generator.push_format (Generator.ROMAN());\r
+ else if (t.arg.equals (StandardEngine.BOLD_COMMANDNAME()))\r
+ generator.push_format (Generator.BOLD());\r
+ else if (t.arg.equals (StandardEngine.ITALICS_COMMANDNAME()))\r
+ generator.push_format (Generator.ITALICS());\r
+ else if (t.arg.equals (StandardEngine.SUBSCRIPT_COMMANDNAME()))\r
+ generator.push_format (Generator.SUBSCRIPT());\r
+ else if (t.arg.equals (StandardEngine.SUPERSCRIPT_COMMANDNAME()))\r
+ generator.push_format (Generator.SUPERSCRIPT());\r
+ }\r
+}\r
+\r
+public class PopFormatCommandAction extends Action {\r
+ Generator generator;\r
+\r
+ public PopFormatCommandAction( Generator g ) {\r
+ generator = g;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ generator.pop_format ();\r
+ }\r
+}\r
+\r
+public class OtherAction extends Action {\r
+ Generator generator;\r
+\r
+ public OtherAction( Generator g ) {\r
+ generator = g;\r
+ }\r
+\r
+ public void perform (Token t) {\r
+ generator.plaintext (t.arg);\r
+ }\r
+}\r
+\r
+public class EndOfStreamAction extends Action {\r
+ Generator generator;\r
+\r
+ public EndOfStreamAction( Generator g ) {\r
+ generator = g;\r
+ }\r
+ \r
+ public void perform (Token t) {\r
+ System.out.println ("... done");\r
+ }\r
+}\r
--- /dev/null
+/**\r
+ * Assert class\r
+ * Provides assertion checking\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/03/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+\r
+public class Assert {\r
+ //static PrintStream error_stream = Tagger.error_stream;\r
+\r
+ public static void assert_ (boolean cond) {\r
+ if (!cond) {\r
+ //error_stream.println ("Assertion failure");\r
+ System.out.println ("Assertion failure");\r
+ System.exit(-1);\r
+ // print stack trace\r
+ }\r
+ }\r
+\r
+ public static void unreachable () {\r
+ //error_stream.println ("Assertion failure");\r
+ System.out.println ("Assertion failure");\r
+ System.exit(-1);\r
+ }\r
+}\r
--- /dev/null
+/**\r
+ * Counter class\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/03/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+\r
+public class Counter {\r
+ private int count;\r
+ private int initial;\r
+ private int type;\r
+\r
+ static int NO_SUCH_TYPE() { return -1; }\r
+ static int ARABIC () { return 0; }\r
+ static int ROMAN_UPPER () { return 1; }\r
+ static int ROMAN_LOWER () { return 2; }\r
+ static int ALPHA_UPPER () { return 3; }\r
+ static int ALPHA_LOWER () { return 4; }\r
+\r
+ // eventually recognize counter_type and set initial count and output format\r
+ // takes style and stream for error reporting\r
+ /*\r
+ * requires: count_prop and style are non null\r
+ *\r
+ */\r
+ public Counter (String count_prop, String style) {\r
+ Assert.assert_ (count_prop != null);\r
+ Assert.assert_ (style != null);\r
+ type = get_type (count_prop);\r
+\r
+ //switch (type) {\r
+ if( type == NO_SUCH_TYPE() ) {\r
+ type = ARABIC();\r
+ initial = 0;\r
+\r
+ } else if( type == ALPHA_LOWER() ||\r
+ type == ALPHA_UPPER() ) {\r
+ if (count_prop.length () != 1) {\r
+ System.out.println ("Bad counter type for style " + style + ": " + count_prop);\r
+ initial = 0; \r
+ } else {\r
+ initial = count_prop.toLowerCase().charAt (0) - 'a';\r
+ }\r
+\r
+ } else if( type == ARABIC() ) {\r
+ initial = Integer.parseInt (count_prop) - 1;\r
+\r
+ } else if( type == ROMAN_LOWER() ||\r
+ type == ROMAN_UPPER() ) {\r
+ // not yet implemented\r
+ initial = 0;\r
+ type = ARABIC();\r
+ \r
+ } else {\r
+ Assert.unreachable ();\r
+ }\r
+\r
+ count = initial;\r
+ }\r
+ \r
+ /**\r
+ * ensures: increments counter\r
+ * returns true iff successful, false otherwise (eg, because alphabetic counter went past 'z')\r
+ */\r
+ public boolean increment () {\r
+ if ((type == ALPHA_UPPER() || type == ALPHA_LOWER()) && count == 26)\r
+ return false;\r
+ count++;\r
+ return true;\r
+ }\r
+ \r
+ public void reset () {\r
+ count = initial;\r
+ }\r
+ \r
+ public String unparse () {\r
+\r
+ //switch (type) {\r
+\r
+ if( type == ALPHA_LOWER() ) {\r
+ char c = (char) ('a' + count - 1);\r
+ return new Character (c).toString();\r
+ }\r
+\r
+ if( type == ALPHA_UPPER() ) {\r
+ char c = (char) ('A' + count - 1);\r
+ return new Character (c).toString();\r
+ }\r
+\r
+ if( type == ARABIC() ) {\r
+ return String.valueOf (count);\r
+ }\r
+\r
+ Assert.unreachable ();\r
+ return "DUMMY";\r
+ }\r
+ \r
+ /**\r
+ *\r
+ * ensures: returns counter type of counter given in the string counter_type\r
+ * as an int, being equal to one of the values of the constants declared in the Counter class.\r
+ * returns Counter.NO_SUCH_TYPE if the string is not well formed.\r
+ */\r
+ public static int get_type (String counter_type) {\r
+ if (counter_type.length() == 0) return NO_SUCH_TYPE();\r
+ char c = counter_type.charAt (0);\r
+ if (c >= 'a' && c <= 'z')\r
+ return ALPHA_LOWER();\r
+ if (c >= 'A' && c <= 'Z')\r
+ return ALPHA_UPPER();\r
+ if (c == 'i' || c == 'v' || c == 'x' ||c == 'l' || c == 'c' || c == 'm')\r
+ return ROMAN_LOWER();\r
+ if (c == 'I' || c == 'V' || c == 'X' ||c == 'L' || c == 'C' || c == 'M')\r
+ return ROMAN_LOWER();\r
+ if (c >= '0' && c <= '9')\r
+ return ARABIC();\r
+ return NO_SUCH_TYPE();\r
+ }\r
+}\r
--- /dev/null
+/**\r
+ * Engine class\r
+ * Maps token types to actions\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/06/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.util.*;\r
+\r
+public class Engine {\r
+ /**\r
+ * There are some very tricky concurrent modification issues with this class.\r
+ * Can't execute a register or unregister method during an execution of consume_token\r
+ * if the register or unregister affects the same list of actions associated with the token.\r
+ * This means that during a consume_token for some type, can't register or unregister for\r
+ * that type, or for the all types.\r
+ * Note that a version of the perform method of action takes an iterator argument to\r
+ * allow an action to remove itself.\r
+ */\r
+ \r
+ // array of Action lists indexed on token type\r
+ private LinkedList [] actions;\r
+\r
+ // actions performed for all token types\r
+ private LinkedList default_actions;\r
+\r
+ public Engine () {\r
+ actions = new LinkedList [Token.MAXTOKEN() + 1];\r
+ for (int i = 0; i < actions.length; i++)\r
+ actions[i] = disjoint llActions new LinkedList ();\r
+ default_actions = /*disjoint llDefault*/ new LinkedList ();\r
+ }\r
+\r
+ public void register_by_type (Action action, int type) {\r
+ register_by_type_front (action, type);\r
+ }\r
+\r
+ public void register_for_all (Action action) {\r
+ default_actions.addFirst (action);\r
+ }\r
+\r
+ public void unregister_for_all (Action action) {\r
+ default_actions.remove (action);\r
+ }\r
+\r
+ public void register_by_type_front (Action action, int type) {\r
+ Assert.assert_ (type >= 0);\r
+ Assert.assert_ (type <= Token.MAXTOKEN());\r
+ actions[type].addFirst (action);\r
+\r
+ }\r
+\r
+ public void register_by_type_back (Action action, int type) {\r
+ Assert.assert_ (type >= 0);\r
+ Assert.assert_ (type <= Token.MAXTOKEN());\r
+ actions[type].addLast (action);\r
+ }\r
+\r
+ public void unregister_by_type (Action action, int type) {\r
+ Assert.assert_ (type >= 0);\r
+ Assert.assert_ (type <= Token.MAXTOKEN());\r
+ actions[type].remove (action);\r
+ }\r
+\r
+ public void consume_token (Token token) {\r
+ perform_actions (default_actions, token);\r
+ perform_actions (actions[token.type], token);\r
+ }\r
+ \r
+ public static void perform_actions (LinkedList actions, Token token) {\r
+ Iterator i = actions.iterator ();\r
+ while (i.hasNext ()) {\r
+ Action a = (Action) i.next ();\r
+ a.perform (token, i);\r
+ }\r
+ }\r
+}\r
--- /dev/null
+/**\r
+ * Generator interface\r
+ * Generic backend tagged text generator\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/08/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+//import java.util.*;\r
+\r
+public /*interface*/ class Generator {\r
+ \r
+ // formats to pass to push_format\r
+ public static int ROMAN () { return 0; }\r
+ public static int ITALICS () { return 1; }\r
+ public static int BOLD () { return 2; }\r
+ public static int SUBSCRIPT () { return 3; }\r
+ public static int SUPERSCRIPT() { return 4; }\r
+ \r
+ // prints new line to output\r
+ void linefeed (){}\r
+ \r
+ void new_para (String style){}\r
+ \r
+ // inserts code for new line\r
+ void new_line (){}\r
+ \r
+ void special_char (String font, String index){}\r
+ \r
+ // for dashes, ellipses, etc\r
+ void special_char (String index){}\r
+ \r
+ void plaintext (String text){}\r
+ void push_format (int format){}\r
+ void pop_format (){}\r
+ \r
+ // turn output suppression on and off\r
+ void suppress_on (){}\r
+ void suppress_off (){}\r
+ \r
+}\r
--- /dev/null
+/**\r
+ * Numbering class\r
+ * Provides special navigations for numbering\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/03/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+//import java.util.*;\r
+\r
+public class Numbering {\r
+ private PropertyMap style_map;\r
+\r
+ public static String PARENT_PROPNAME () { return "parent"; }\r
+ public static String CHILD_PROPNAME () { return "child"; }\r
+ public static String ROOT_PROPNAME () { return "root"; }\r
+ public static String COUNTER_PROPNAME () { return "counter"; }\r
+ public static String SEPARATOR_PROPNAME() { return "separator";}\r
+ public static String LEADER_PROPNAME () { return "leader"; }\r
+ public static String TRAILER_PROPNAME () { return "trailer"; }\r
+\r
+ /*\r
+ * The graph structure of the numbering relations is represented using\r
+ * properties in the paragraph style property map.\r
+ * Each style is mapped to its root -- the ancestor with no parent in the\r
+ * numbering relationship -- and to its parent and child.\r
+ * The child and root properties are added; the parent property is given\r
+ * in the style sheet file.\r
+ *\r
+ * If a style is numbered, its ancestors must be also.\r
+ * This property is not currently checked.\r
+ */\r
+ \r
+ /*\r
+ * Representation invariant\r
+ *\r
+ * Definition: A style is numbered if it has a counter property.\r
+ * A numbered style has a root property.\r
+ * A root style has itself as root and has no parent.\r
+ * There is a bidirectional parent/child chain from a style to its root\r
+ *\r
+ * Checking that style sheet is well formed?\r
+ */\r
+ \r
+\r
+ // maps paragraph style names to counters\r
+ // styles that are not numbered are not mapped\r
+ private HashMap counter_map; // String -> Counter\r
+\r
+ /**\r
+ * ensures: constructs a Numbering\r
+ * not well formed until incorporate called\r
+ */\r
+ public Numbering (PropertyMap style_map) {\r
+ this.style_map = style_map;\r
+ counter_map = new HashMap ();\r
+ }\r
+ \r
+ /**\r
+ * ensures: constructs a Numbering\r
+ * modifies: property lists in style_map\r
+ */\r
+ /*\r
+ public Numbering (PropertyMap style_map) {\r
+ this.style_map = style_map;\r
+ add_extra_properties (style_map);\r
+ initialize_counters (style_map);\r
+ }\r
+ */\r
+ \r
+ /**\r
+ * ensures: constructs a Numbering using current entries in style_map\r
+ * modifies: property lists in style_map\r
+ */\r
+ public void incorporate () {\r
+ add_extra_properties ();\r
+ initialize_counters ();\r
+ }\r
+ \r
+ /*\r
+ * requires: all ancestor and descendant styles of style are numbered iff style is numbered\r
+ * ensures: returns the numbering string for a new paragraph whose style name is _style_\r
+ *\r
+ * format of numbering string is:\r
+ * <mytrailer><rootcounter><rootseparator>...<counter><separator>...<mycounter><mytrailer>\r
+ */\r
+ public String get_numbering_string (String style) {\r
+ // return empty string if style is not numbered\r
+ if (!style_has_property (style, COUNTER_PROPNAME())) return "";\r
+ \r
+ // initialize numbering string to leader\r
+ String leader = style_map.get_property (style, LEADER_PROPNAME());\r
+ String numbering = leader == null ? "" : leader;\r
+ \r
+ // append numbering for each style from root to this style\r
+ // each followed by its separator\r
+ String s = style_map.get_property (style, ROOT_PROPNAME());\r
+ Assert.assert_ (s != null);\r
+ while (! s.equals (style)) {\r
+ numbering += ((Counter) counter_map.get(s)).unparse ();\r
+ String separator = style_map.get_property (s, SEPARATOR_PROPNAME());\r
+ numbering += separator == null ? "" : separator;\r
+ s = style_map.get_property (s, CHILD_PROPNAME());\r
+ }\r
+ \r
+ // increment numbering for this style and append its string\r
+ Counter c = (Counter) counter_map.get (s);\r
+ boolean success = c.increment ();\r
+ if (!success)\r
+ System.out.println ("Counter overrun for style: " + style);\r
+ numbering += c.unparse ();\r
+ \r
+ // append trailer\r
+ String trailer = style_map.get_property (s, TRAILER_PROPNAME());\r
+ numbering += trailer == null ? "" : trailer;\r
+ \r
+ // reset counters for all descendant styles\r
+ s = style_map.get_property (s, CHILD_PROPNAME());\r
+ while (s != null) {\r
+ c = (Counter) counter_map.get (s);\r
+ c.reset ();\r
+ s = style_map.get_property (s, CHILD_PROPNAME());\r
+ }\r
+ return numbering;\r
+ }\r
+ \r
+ private void add_extra_properties () {\r
+ add_child_property ();\r
+ add_root_property ();\r
+ }\r
+ \r
+ // for each style with a counter property, insert into counter_map\r
+ private void initialize_counters () {\r
+ HashSet styles = style_map.get_items ();\r
+ Iterator iter = (Iterator) styles.iterator ();\r
+ while (iter.hasNext ()) {\r
+ String style = (String) iter.next ();\r
+ if (style_has_property (style, COUNTER_PROPNAME())) {\r
+ // get counter type (arabic, roman, etc)\r
+ String count_prop = style_map.get_property (style, COUNTER_PROPNAME());\r
+ int count_type = Counter.get_type (count_prop);\r
+ if (count_type == Counter.NO_SUCH_TYPE()) {\r
+ System.out.println ("Bad counter type for style " + style + ": " + count_prop);\r
+ // and insert into counter_map anyway to preserve rep invariant\r
+ // so must check counter type when counter is created and default if bad\r
+ }\r
+ counter_map.put (style, new Counter (count_prop, style));\r
+ }\r
+ }\r
+ }\r
+ \r
+ // add to each style that is a parent of another style a child property to it\r
+ private void add_child_property () {\r
+ HashSet styles = style_map.get_items ();\r
+ Iterator iter = (Iterator) styles.iterator ();\r
+ while (iter.hasNext ()) {\r
+ String style = (String) iter.next ();\r
+ String pstyle = (String) style_map.get_property (style, PARENT_PROPNAME());\r
+ // if parent exists, add child property to it\r
+ if (pstyle != null) {\r
+ LinkedList props = style_map.get_property_list (pstyle);\r
+ props.add (new Property (CHILD_PROPNAME(), style));\r
+ }\r
+ }\r
+ }\r
+ \r
+ // add root property to each numbered style\r
+ private void add_root_property () {\r
+ HashSet styles = style_map.get_items ();\r
+ Iterator iter = (Iterator) styles.iterator ();\r
+ while (iter.hasNext ()) {\r
+ String style = (String) iter.next ();\r
+ if (!style_has_property (style, PARENT_PROPNAME())) {\r
+ // if no parent, then it's a root, so add root property for it and all descendants\r
+ String root = style;\r
+ while (style != null) {\r
+ LinkedList props = style_map.get_property_list (style);\r
+ props.add (new Property (ROOT_PROPNAME(), root));\r
+ style = style_map.get_property (style, CHILD_PROPNAME());\r
+ }\r
+ }\r
+ }\r
+ }\r
+ \r
+ // ensures: returns true iff style has property prop_name\r
+ private boolean style_has_property (String style, String prop_name) {\r
+ String p = (String) style_map.get_property (style, prop_name);\r
+ return p != null;\r
+ }\r
+ \r
+ public String toString () {\r
+ return "UNIMPLEMENTED";\r
+ }\r
+}\r
--- /dev/null
+/**\r
+ * Property class\r
+ * <p>\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/02/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+//import java.util.*;\r
+\r
+public class Property {\r
+ public String property;\r
+ public String value;\r
+ \r
+ public Property (String p, String v) {\r
+ property = p;\r
+ value = v;\r
+ }\r
+\r
+ public String toString () {\r
+ return "<" + property + ":" + value + ">";\r
+ }\r
+}\r
--- /dev/null
+/**\r
+ * PropertyMap class\r
+ * Maps identifiers to property lists\r
+ * Used for stylesheets, character maps, etc\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/03/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+//import java.util.*;\r
+\r
+public class PropertyMap {\r
+ private HashMap map; // String -> LinkedList [Property]\r
+ private HashSet keys;\r
+\r
+ /**\r
+ * ensures: constructs an empty property map\r
+ */\r
+ public PropertyMap () {\r
+ map = new HashMap ();\r
+ keys = new HashSet();\r
+ }\r
+\r
+ /**\r
+ * ensures: constructs a property map using the parser <code>p</code>.\r
+ */\r
+ public PropertyMap (PropertyParser p) {\r
+ map = new HashMap ();\r
+ keys = new HashSet();\r
+ \r
+ while (p.has_more_properties ()) {\r
+ LinkedList props = p.get_property_list ();\r
+ Property prop = (Property) props.removeFirst ();\r
+ map.put (prop.value, props);\r
+ keys.add(prop.value);\r
+ }\r
+ }\r
+\r
+ /**\r
+ * ensures: incorporates properties using the parser <code>p</code>.\r
+ */\r
+ public void incorporate (PropertyParser p) {\r
+ \r
+ while (p.has_more_properties ()) {\r
+ LinkedList props = p.get_property_list ();\r
+ Property prop = (Property) props.removeFirst ();\r
+ map.put (prop.value, props);\r
+ keys.add(prop.value);\r
+ }\r
+ \r
+ }\r
+\r
+ /**\r
+ * @return the property list for item <code>item</code>. Returns null if no such item.\r
+ */\r
+ public LinkedList get_property_list (String item) {\r
+ return (LinkedList) map.get (item);\r
+ }\r
+\r
+ /**\r
+ * @return the value of property <code>prop</code> for item <code>item</code>\r
+ * or null if it does not exist\r
+ */\r
+ public String get_property (String item, String prop) {\r
+ LinkedList props = (LinkedList) map.get (item);\r
+ if (props == null) return null;\r
+ Iterator iter = props.iterator ();\r
+ while (iter.hasNext ()) {\r
+ Property p = (Property) iter.next ();\r
+ if (p.property.equals (prop))\r
+ return p.value;\r
+ }\r
+ return null;\r
+ }\r
+\r
+ /**\r
+ * @return the set of items with property lists in the map\r
+ */\r
+ public HashSet get_items () {\r
+ return keys; //map.keySet ();\r
+ }\r
+ \r
+ public String toString () {\r
+ return map.toString ();\r
+ }\r
+}\r
--- /dev/null
+/**\r
+ * PropertyParser class\r
+ * Parses property files\r
+ * <p>\r
+ * <code>int</code>.\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/02/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+//import java.util.*;\r
+\r
+public class PropertyParser {\r
+ private FileInputStream reader;\r
+ private String token;\r
+ private int next_char;\r
+\r
+ public PropertyParser (FileInputStream r) {\r
+ reader = r;\r
+ next_char = reader.read ();\r
+ consume_comments ();\r
+ }\r
+ \r
+ private void consume_comments () {\r
+ // consume lines that don't start with <\r
+ while (next_char != '<' && !is_eos (next_char)) {\r
+ if (!is_eol (next_char))\r
+ reader.readLine ();\r
+ consume_char ();\r
+ }\r
+ }\r
+ \r
+ private void consume_char () {\r
+ token += (char) next_char;\r
+ next_char = reader.read ();\r
+ //while(next_char == 13 || next_char==10) {\r
+ // next_char = reader.read ();\r
+ //}\r
+ //System.out.println( "next_char: "+(char)next_char );\r
+ }\r
+ \r
+ private void error (String msg) {\r
+ // correct to number from 1, not zero\r
+ //t line_number = reader.getLineNumber() + 1;\r
+ System.out.println (msg);\r
+ System.exit(-1);\r
+ }\r
+ \r
+ public boolean has_more_properties () {\r
+ return (!is_eos (next_char));\r
+ }\r
+ \r
+ /**\r
+ * requires: next_char contains next character in reader <p>\r
+ * ensures: returns list of properties until end of line or stream <p>\r
+ * according to the following syntax:\r
+ * property list is sequence of properties followed by eol of eos\r
+ * property is left-angle, property-name, colon, value, right-angle\r
+ * property-name is alphanumeric string, but value is any char sequence\r
+ * skips lines that do not start with <\r
+ * reports syntax errors on this.error_reporter\r
+ * Syntax\r
+ * @return list of properties until end of line or stream.\r
+ * Notes: chose LinkedList because it provides removeFirst, to support common\r
+ * case in which first property is removed (eg, because it's a style name)\r
+ */\r
+ public LinkedList get_property_list () {\r
+ LinkedList result = /*disjoint llPropList*/ new LinkedList ();\r
+ while (!is_eol (next_char) && !is_eos(next_char))\r
+ result.add (get_property ());\r
+ consume_char ();\r
+ consume_comments ();\r
+ return result;\r
+ }\r
+ \r
+ private Property get_property () { \r
+ if (next_char != '<')\r
+ error ("Found " + next_char + " when expecting <");\r
+ consume_char ();\r
+ token = "";\r
+ while (is_alphanumeric (next_char)) consume_char ();\r
+ String property = token;\r
+ if (next_char != ':')\r
+ error ("Found " + next_char + " following " + token + " when expecting :");\r
+ consume_char ();\r
+ token = "";\r
+ while (next_char != '>' && !is_eol(next_char) && !is_eos (next_char))\r
+ consume_char ();\r
+ String value = token;\r
+ if (next_char != '>')\r
+ error ("Found " + next_char + " following " + token + " when expecting >");\r
+ consume_char ();\r
+ return new Property (property, value);\r
+ }\r
+ \r
+ static boolean is_eol (int c) {return c == '\n';}\r
+ static boolean is_eos (int c) {return c == -1;}\r
+ static boolean is_alphabetic (int c) {\r
+ return c >= 'a' && c <= 'z' || c >= 'A' && c <= 'Z';\r
+ }\r
+ static boolean is_numeric (int c) {return c >= '0' && c <= '9';}\r
+ static boolean is_alphanumeric (int c) {\r
+ return is_numeric (c) || is_alphabetic (c);\r
+ }\r
+}\r
--- /dev/null
+/**\r
+ * QuarkGenerator interface\r
+ * Backend tagged text generator for QuarkXpress\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/08/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+//import java.util.*;\r
+\r
+public class QuarkGenerator extends Generator {\r
+ FileOutputStream output_stream;\r
+ LinkedList format_stack;\r
+ private boolean on;\r
+\r
+ public QuarkGenerator (FileOutputStream s) {\r
+ on = true;\r
+ output_stream = s;\r
+ \r
+ // stack holds strings used to terminate formats\r
+ format_stack = /*disjoint llQuarkGen*/ new LinkedList ();\r
+ }\r
+ \r
+ public void suppress_on () {\r
+ on = false;\r
+ }\r
+ \r
+ public void suppress_off () {\r
+ on = true;\r
+ }\r
+\r
+ private void print (String s) {\r
+ if (on) output_stream.write (s.getBytes());\r
+ }\r
+\r
+ public void linefeed () {\r
+ if (on) output_stream.write ('\n');\r
+ }\r
+\r
+ // print "@style:"\r
+ public void new_para (String style) {\r
+ print ("@" + style + ":");\r
+ }\r
+\r
+ // print "<\n>"\r
+ public void new_line () {\r
+ print ("<\\n>");\r
+ }\r
+\r
+ public void special_char (String font, String index) {\r
+ print ("<f\"" + font + "\"><\\#" + index + "><f$>");\r
+ }\r
+\r
+ public void special_char (String index) {\r
+ print ("<\\#" + index + ">");\r
+ }\r
+\r
+ public void plaintext (String text) {\r
+ print (text);\r
+ }\r
+\r
+ public void push_format (int format) {\r
+ //switch (format) {\r
+\r
+ if( format == Generator.ROMAN() ||\r
+ format == Generator.ITALICS() ) {\r
+ print ("<I>");\r
+ format_stack.push ("<I>");\r
+ return;\r
+ }\r
+\r
+ if( format == Generator.BOLD() ) {\r
+ print ("<B>");\r
+ format_stack.push ("<B>");\r
+ return;\r
+ }\r
+\r
+ if( format == Generator.SUBSCRIPT() ) {\r
+ print ("<->");\r
+ format_stack.push ("<->");\r
+ return;\r
+ }\r
+\r
+ if( format == Generator.SUPERSCRIPT() ) {\r
+ print ("<+>");\r
+ format_stack.push ("<+>");\r
+ return;\r
+ }\r
+ \r
+ Assert.unreachable ();\r
+ }\r
+ \r
+ public void pop_format () {\r
+ // for now, handle too many pops without report\r
+ if (format_stack.isEmpty ()) return;\r
+ print ((String) format_stack.pop ());\r
+ }\r
+}\r
--- /dev/null
+/**\r
+ * SourceParser class\r
+ * <p>\r
+ * <code>int</code>.\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/02/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+//import java.util.*;\r
+\r
+public class SourceParser {\r
+ public static String loadcharmapcommand_name () { return "loadchars"; }\r
+ public static String loadstylesheetcommand_name() { return "loadstyles";}\r
+ public static String preamblecommand_name () { return "preamble"; }\r
+ public static String refcommand_name () { return "ref"; }\r
+ public static String tagcommand_name () { return "tag"; }\r
+ public static String citecommand_name () { return "cite"; }\r
+ public static String separatorcommand_name () { return "sep"; }\r
+\r
+ private FileInputStream reader;\r
+\r
+ // holds set of strings recognized as paragraph styles\r
+ private HashSet parastyles;\r
+\r
+ // holds the previous value of next_char\r
+ private int last_char;\r
+ private int next_char;\r
+ private boolean within_single_quotes;\r
+ private boolean within_double_quotes;\r
+ private boolean at_start_of_line;\r
+ private String token;\r
+ \r
+ public SourceParser (FileInputStream reader, HashSet parastyles) {\r
+ this.reader = reader;\r
+ this.parastyles = parastyles;\r
+ next_char = reader.read ();\r
+ last_char = -1;\r
+ at_start_of_line = true;\r
+ }\r
+ \r
+ public boolean has_more_tokens () {\r
+ return (next_char != -1);\r
+ }\r
+ \r
+ private void consume_char () {\r
+ token += (char) next_char;\r
+ last_char = next_char;\r
+ next_char = reader.read ();\r
+ }\r
+\r
+ // consume until next close curly and return string excluding curly\r
+ private String consume_arg () {\r
+ consume_char (); // consume open curly\r
+ token = "";\r
+ consume_char ();\r
+ while (!is_close_curly (next_char) && !is_eol (next_char)) consume_char ();\r
+ String arg = token;\r
+ consume_char (); // consume close curly\r
+ return arg;\r
+ }\r
+ \r
+ /**\r
+ * requires: next_char contains next character in reader <p>\r
+ * ensures: returns next token according to one of these productions: <p>\r
+ * <blockquote><pre>\r
+ * char-sequence = alphanumeric+\r
+ * whitespace ::= (space | tab)+\r
+ * command ::= slash alphanum* [star]\r
+ * paragraph-break ::= <blank line>\r
+ * line-break ::= slash slash\r
+ * hyphen-sequence ::= hyphen+\r
+ * dot-sequence ::= dot+\r
+ * underscore ::= underscore\r
+ * </pre></blockquote>\r
+ * quote characters, disambiguated by context:\r
+ * open-single-quote: when not preceded by alphanumeric\r
+ * close-single-quote: when not followed by alphanumeric and preceded by\r
+ * open-single-quote\r
+ * open-double-quote: when not preceded by open-double-quote\r
+ * close-double-quote: when preceded by open-double-quote\r
+ * apostrophe: between alphanumerics, or when followed by numeric\r
+ * prime: after alphanumeric, when not followed by alphanumeric,\r
+ * and not preceded by open-single-quote\r
+ * @return the next token.\r
+ * explicitly returns end of stream token.\r
+ */\r
+ public Token get_token () {\r
+ token = new String ("");\r
+ if (is_eos (next_char))\r
+ return new Token (Token.ENDOFSTREAM(), 0);\r
+ if (at_start_of_line) {\r
+ if (is_eol (next_char)) {\r
+ consume_char ();\r
+ within_single_quotes = false;\r
+ within_double_quotes = false;\r
+ return new Token (Token.PARABREAK(), 0);\r
+ }\r
+ else if (is_hash (next_char)) {\r
+ String line = reader.readLine ();\r
+ consume_char ();\r
+ return new Token (Token.COMMENT(), line, 0);\r
+ }\r
+ else\r
+ at_start_of_line = false;\r
+ }\r
+ if (is_eol (next_char)) {\r
+ consume_char ();\r
+ at_start_of_line = true;\r
+ if (is_eol (next_char)) {\r
+ consume_char ();\r
+ within_single_quotes = false;\r
+ within_double_quotes = false;\r
+ return new Token (Token.PARABREAK(), 0);\r
+ }\r
+ // check this\r
+ return new Token (Token.WHITESPACE(), " ", 0);\r
+ }\r
+ if (is_slash (next_char)) {\r
+ consume_char ();\r
+ token = new String("");\r
+ if (is_slash (next_char)) {\r
+ consume_char ();\r
+ return new Token (Token.LINEBREAK(), 0);\r
+ }\r
+ if (!is_alphabetic (next_char)) {\r
+ // next character assumed prefixed with slash to avoid special treatment\r
+ // eg, \< for <, \$ for $\r
+ token = new Character ((char) next_char).toString ();\r
+ return new Token (Token.OTHER(), token, 0);\r
+ }\r
+ while (is_alphanumeric (next_char)) consume_char ();\r
+ String command_name = token;\r
+ if (is_star (next_char)) consume_char ();\r
+ if (command_name.equals (preamblecommand_name())) {\r
+ return new Token (Token.PREAMBLECOMMAND(), 0);\r
+ }\r
+ if (command_name.equals (separatorcommand_name())) {\r
+ // consume whitespace until next token\r
+ while (is_whitespace (next_char)) consume_char ();\r
+ return new Token (Token.SEPARATORCOMMAND(), 0);\r
+ }\r
+ if (is_less_than (next_char)) {\r
+ consume_char ();\r
+ return new Token (Token.FORMATCOMMAND(), command_name, 0);\r
+ }\r
+ if (is_open_curly (next_char)) {\r
+ String arg = consume_arg ();\r
+ if (command_name.equals (loadcharmapcommand_name())) {\r
+ return new Token (Token.LOADCHARMAPCOMMAND(), arg, 0);\r
+ }\r
+ if (command_name.equals (loadstylesheetcommand_name())) {\r
+ return new Token (Token.LOADSTYLESHEETCOMMAND(), arg, 0);\r
+ }\r
+ if (command_name.equals (refcommand_name())) {\r
+ return new Token (Token.REFCOMMAND(), arg, 0);\r
+ }\r
+ if (command_name.equals (tagcommand_name())) {\r
+ return new Token (Token.TAGCOMMAND(), arg, 0);\r
+ }\r
+ if (command_name.equals (citecommand_name())) {\r
+ return new Token (Token.CITECOMMAND(), arg, 0);\r
+ }\r
+ }\r
+ if (parastyles.contains (command_name)) {\r
+ while (is_whitespace (next_char)) consume_char ();\r
+ // paragraph style command consumes the first linebreak following it also\r
+ if (is_eol (next_char)) consume_char ();\r
+ return new Token (Token.PARASTYLECOMMAND(), command_name, 0);\r
+ }\r
+ else\r
+ // temporary\r
+ return new Token (Token.CHARCOMMAND(), command_name, 0);\r
+ }\r
+ if (is_alphabetic (next_char)) {\r
+ consume_char ();\r
+ while (is_alphabetic (next_char)) consume_char ();\r
+ return new Token (Token.ALPHABETIC(), token, 0);\r
+ }\r
+ if (is_numeric (next_char)) {\r
+ consume_char ();\r
+ while (is_numeric (next_char)) consume_char ();\r
+ return new Token (Token.NUMERIC(), token, 0);\r
+ }\r
+ if (is_whitespace (next_char)) {\r
+ consume_char ();\r
+ while (is_whitespace (next_char)) consume_char ();\r
+ if (is_eol (next_char)) {\r
+ consume_char ();\r
+ // check this\r
+ return new Token (Token.WHITESPACE(), " ", 0);\r
+ }\r
+ return new Token (Token.WHITESPACE(), token, 0);\r
+ }\r
+ if (is_hyphen (next_char)) {\r
+ consume_char ();\r
+ while (is_hyphen (next_char)) consume_char ();\r
+ return new Token (Token.HYPHENS(), token, 0);\r
+ }\r
+ if (is_dot (next_char)) {\r
+ consume_char ();\r
+ while (is_dot (next_char)) consume_char ();\r
+ return new Token (Token.DOTS(), token, 0);\r
+ }\r
+ if (is_underscore (next_char)) {\r
+ consume_char ();\r
+ return new Token (Token.UNDERSCORE(), 0);\r
+ }\r
+ if (is_dollar (next_char)) {\r
+ consume_char ();\r
+ return new Token (Token.DOLLAR(), 0);\r
+ }\r
+ if (is_greater_than (next_char)) {\r
+ consume_char ();\r
+ return new Token (Token.POPFORMATCOMMAND(), 0);\r
+ }\r
+ if (is_single_quote (next_char)) {\r
+ if (is_alphanumeric (last_char)) {\r
+ if (is_alphanumeric (next_char)) {\r
+ consume_char ();\r
+ return new Token (Token.APOSTROPHE(), 0);\r
+ }\r
+ else if (within_single_quotes) {\r
+ within_single_quotes = false;\r
+ consume_char ();\r
+ return new Token (Token.CLOSESINGLEQUOTE(), 0);\r
+ }\r
+ else {\r
+ consume_char ();\r
+ return new Token (Token.PRIME(), 0);\r
+ }\r
+ }\r
+ consume_char ();\r
+ if (is_numeric (next_char)) {\r
+ return new Token (Token.APOSTROPHE(), 0);\r
+ }\r
+ else {\r
+ within_single_quotes = true;\r
+ return new Token (Token.OPENSINGLEQUOTE(), 0);\r
+ }\r
+ }\r
+ if (is_double_quote (next_char)) {\r
+ consume_char ();\r
+ if (within_double_quotes) {\r
+ within_double_quotes = false;\r
+ return new Token (Token.CLOSEDOUBLEQUOTE(), 0);\r
+ }\r
+ else {\r
+ within_double_quotes = true;\r
+ return new Token (Token.OPENDOUBLEQUOTE(), 0);\r
+ }\r
+ }\r
+ consume_char ();\r
+ return new Token (Token.OTHER(), token, 0);\r
+ }\r
+\r
+ static boolean is_eol (int c) {return c == '\n';}\r
+ static boolean is_eos (int c) {return c == -1;}\r
+ static boolean is_star (int c) {return c == '*';}\r
+ static boolean is_hash (int c) {return c == '#';}\r
+ static boolean is_dot (int c) {return c == '.';}\r
+ static boolean is_slash (int c) {return c == '\\';}\r
+ static boolean is_hyphen (int c) {return c == '-';}\r
+ static boolean is_underscore (int c) {return c == '_';}\r
+ static boolean is_dollar (int c) {return c == '$';}\r
+ static boolean is_single_quote (int c) {return c == '\'';}\r
+ static boolean is_double_quote (int c) {return c == '\"';}\r
+ static boolean is_open_curly (int c) {return c == '{';}\r
+ static boolean is_close_curly (int c) {return c == '}';}\r
+ static boolean is_less_than (int c) {return c == '<';}\r
+ static boolean is_greater_than (int c) {return c == '>';}\r
+ \r
+ // should perhaps use Character.isLetter? not sure, because that allows Unicode chars for\r
+ // other languages that are outside the a-Z range.\r
+ static boolean is_alphabetic (int c) {\r
+ return c >= 'a' && c <= 'z' || c >= 'A' && c <= 'Z';\r
+ }\r
+ static boolean is_numeric (int c) {return c >= '0' && c <= '9';}\r
+ static boolean is_alphanumeric (int c) {\r
+ return is_numeric (c) || is_alphabetic (c);\r
+ }\r
+ static boolean is_whitespace (int c) {return c == ' ' || c == '\t';}\r
+}\r
--- /dev/null
+/**\r
+ * StandardEngine class\r
+ * Standard registration of actions\r
+ * Implemented as a subclass of Engine for no good reason\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/08/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+//import java.util.*;\r
+\r
+\r
+// a hack to work around lack of proper closures in Java\r
+// can't assign to local variable within actions\r
+class StringBox {\r
+ String string;\r
+ StringBox (String s) {string = s;}\r
+ void set (String s) {string = s;}\r
+}\r
+\r
+\r
+public class StandardEngine extends Engine {\r
+\r
+ //static Engine STANDARD;\r
+\r
+ // reserved words for property files\r
+\r
+ // character table\r
+ static public String index_prop_name () { return "index"; }\r
+ static public String font_prop_name () { return "font"; }\r
+ \r
+ static public String apostrophe_char_name () { return "quoteright"; }\r
+ static public String prime_char_name () { return "prime"; }\r
+ static public String opensinglequote_char_name () { return "quoteleft"; }\r
+ static public String closesinglequote_char_name() { return "quoteright"; }\r
+ static public String opendoublequote_char_name () { return "quotedblleft"; }\r
+ static public String closedoublequote_char_name() { return "quotedblright"; }\r
+ static public String hyphen_char_name () { return "hyphen"; }\r
+ static public String endash_char_name () { return "endash"; }\r
+ static public String emdash_char_name () { return "emdash"; }\r
+ static public String period_char_name () { return "period"; }\r
+ static public String twodotleader_char_name () { return "twodotleader"; }\r
+ static public String ellipsis_char_name () { return "ellipsis"; }\r
+ \r
+ static public String ROMAN_COMMANDNAME () { return "roman"; }\r
+ static public String BOLD_COMMANDNAME () { return "bold"; }\r
+ static public String ITALICS_COMMANDNAME () { return "italic"; }\r
+ static public String SUBSCRIPT_COMMANDNAME () { return "sub"; }\r
+ static public String SUPERSCRIPT_COMMANDNAME () { return "sup"; }\r
+ \r
+ // style sheet \r
+ static public String next_style_prop_name () { return "next"; }\r
+ static public String default_style_name () { return "body"; }\r
+\r
+ \r
+ public StandardEngine (\r
+ final Generator generator,\r
+ final PropertyMap style_map,\r
+ final FileOutputStream index_stream\r
+ ) {\r
+ Engine();\r
+ \r
+ final PropertyMap char_map = new PropertyMap ();\r
+ final Numbering numbering = new Numbering (style_map);\r
+ \r
+ final StringBox current_para_style = new StringBox (default_style_name());\r
+\r
+ // special action for start of paragraph\r
+ // created once, but dynamically inserted and removed\r
+ // so that it's performed once at the start of each paragraph\r
+ final Action paragraph_action = new ParagraphAction ( generator,\r
+ current_para_style,\r
+ numbering );\r
+ \r
+ Action a = new PlaintextAction (generator);\r
+ register_by_type (a,\r
+ Token.ALPHABETIC());\r
+ //register_by_type (a,\r
+ // Token.NUMERIC());\r
+\r
+ /*\r
+ register_by_type (new PlaintextAction (generator),\r
+ Token.NUMERIC());\r
+ \r
+ register_by_type (new PlaintextAction (generator),\r
+ Token.WHITESPACE());\r
+ \r
+ register_by_type (new NewlineAction (generator),\r
+ Token.LINEBREAK());\r
+ \r
+ register_by_type (new ApostropheAction (generator, char_map),\r
+ Token.APOSTROPHE());\r
+ \r
+ register_by_type (new PrimeAction (generator, char_map),\r
+ Token.PRIME());\r
+\r
+ register_by_type (new OpenSingleQuoteAction (generator, char_map),\r
+ Token.OPENSINGLEQUOTE());\r
+ \r
+ register_by_type (new CloseSingleQuoteAction (generator, char_map),\r
+ Token.CLOSESINGLEQUOTE());\r
+ \r
+ register_by_type (new OpenDoubleQuoteAction (generator, char_map),\r
+ Token.OPENDOUBLEQUOTE());\r
+ \r
+ register_by_type (new CloseDoubleQuoteAction (generator, char_map),\r
+ Token.CLOSEDOUBLEQUOTE());\r
+ \r
+ register_by_type (new HyphenAction (generator, char_map),\r
+ Token.HYPHENS());\r
+ \r
+ register_by_type (new DotsAction (generator, char_map),\r
+ Token.DOTS());\r
+ \r
+ register_by_type (new LoadCharMapCommandAction (generator,\r
+ char_map,\r
+ numbering),\r
+ Token.LOADCHARMAPCOMMAND());\r
+ \r
+ register_by_type (new LoadStyleSheetCommandAction (generator,\r
+ style_map,\r
+ numbering),\r
+ Token.LOADSTYLESHEETCOMMAND());\r
+ \r
+ final Action unsuppress_action = new UnsuppressAction (generator);\r
+ \r
+ // preamble command switches on output suppression\r
+ // registers action to turn suppression off with paragraph break command\r
+ register_by_type (new PreambleCommandAction (generator,\r
+ unsuppress_action,\r
+ this ),\r
+ Token.PREAMBLECOMMAND());\r
+ \r
+ register_by_type (new ParaBreakAction (paragraph_action,\r
+ current_para_style,\r
+ style_map),\r
+ Token.PARABREAK());\r
+ \r
+ register_by_type (new ParaStyleCommandAction (current_para_style),\r
+ Token.PARASTYLECOMMAND());\r
+ \r
+ register_by_type (new CharCommandAction (generator,\r
+ char_map),\r
+ Token.CHARCOMMAND());\r
+\r
+ register_by_type (new UnderscoreAction (generator) {},\r
+ Token.UNDERSCORE());\r
+ \r
+ // used to italicize alphabetic tokens in math mode\r
+ final Action push_italics_action = new PushItalicsAction (generator);\r
+ final Action pop_italics_action = new PopItalicsAction (generator);\r
+ \r
+ register_by_type (new DollarAction (push_italics_action,\r
+ pop_italics_action),\r
+ Token.DOLLAR());\r
+ \r
+ register_by_type (new FormatCommandAction (generator),\r
+ Token.FORMATCOMMAND());\r
+ \r
+ register_by_type (new PopFormatCommandAction (generator),\r
+ Token.POPFORMATCOMMAND());\r
+ \r
+ register_by_type (new OtherAction (generator),\r
+ Token.OTHER());\r
+ \r
+ register_by_type (new EndOfStreamAction (generator),\r
+ Token.ENDOFSTREAM());\r
+ \r
+ //STANDARD = this;\r
+ */\r
+ }\r
+\r
+\r
+ /* no actions for these token types:\r
+ COMMENT\r
+ SEPARATORCOMMAND\r
+ */\r
+ \r
+ /*\r
+ not yet coded:\r
+ \r
+ public static final int REFCOMMAND = 32;\r
+ public static final int TAGCOMMAND = 33;\r
+ public static final int CITECOMMAND = 34;\r
+ */\r
+ \r
+ \r
+ /* general form of action registration is this:\r
+ register_by_type (new Action () {\r
+ public void perform (Token t) {\r
+ // put code to be executed for token type here\r
+ }},\r
+ Token.TYPENAME);\r
+ */\r
+ \r
+ static public void put_special_char (Generator generator, \r
+ PropertyMap char_map,\r
+ String char_name, \r
+ int line) {\r
+ String index = char_map.get_property (char_name, index_prop_name());\r
+ if (index == null) {\r
+ System.out.println (line + ": Unresolved character: " + char_name);\r
+ }\r
+ else\r
+ generator.special_char (index);\r
+ }\r
+}\r
--- /dev/null
+/**\r
+ * Tagger class\r
+ * Main class of Tagger application\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/02/01\r
+ */\r
+\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+//import java.util.*;\r
+\r
+public class Tagger {\r
+\r
+ // holds mapping of token types to actions\r
+ //Engine engine;\r
+\r
+ /**\r
+ * The main method of the Tagger application.\r
+ * @param args The command line arguments, described in usage method\r
+ */\r
+ public static void main (String[] args) {\r
+ check_usage (args);\r
+\r
+ String base_name = args[0];\r
+ String source_file_name = base_name + ".txt";\r
+ String output_file_name = base_name + ".tag.txt";\r
+ String index_file_name = base_name + ".index.txt";\r
+ FileInputStream input_stream;\r
+ FileOutputStream output_stream;\r
+ FileOutputStream index_stream;\r
+ \r
+ \r
+ input_stream = new FileInputStream(source_file_name);\r
+ output_stream = new FileOutputStream(output_file_name);\r
+ index_stream = new FileOutputStream(index_file_name);\r
+\r
+ // for now, hardwire to Quark\r
+ Generator generator = new QuarkGenerator (output_stream);\r
+\r
+ PropertyMap style_map = new PropertyMap ();\r
+ Engine engine = new StandardEngine (generator, style_map, index_stream);\r
+\r
+ //consume_source (engine, style_map, input_stream);\r
+\r
+ output_stream.close ();\r
+ }\r
+ \r
+ public static void consume_source (Engine engine, \r
+ PropertyMap style_map,\r
+ FileInputStream source_reader) {\r
+ HashSet para_styles = style_map.get_items ();\r
+ SourceParser p = new SourceParser (source_reader, para_styles);\r
+ Token token;\r
+ while (p.has_more_tokens ()) {\r
+ token = p.get_token ();\r
+ String s = token.toString();\r
+ if( s == null ) {\r
+ System.out.println( "token: [null]" );\r
+ } else {\r
+ System.out.println( "token: ["+s+"]" );\r
+ }\r
+ engine.consume_token (token);\r
+ }\r
+ // consume end of stream token explicitly\r
+ // depends on get_token returning ENDOFSTREAM token when no more tokens\r
+ token = p.get_token ();\r
+ engine.consume_token (token);\r
+ }\r
+ \r
+ static void check_usage (String args []) {\r
+ if (args.length == 0) {\r
+ System.out.println ("one argument required, should be name of source file, excluding .txt extension");\r
+ }\r
+ } \r
+}\r
--- /dev/null
+/**\r
+ * Token class\r
+ * Represents tokens generated by lexer\r
+ * <p>\r
+ *\r
+ * @author Daniel Jackson\r
+ * @version 0, 07/06/01\r
+ */\r
+\r
+//package tagger;\r
+//import java.io.*;\r
+//import java.util.*;\r
+\r
+public class Token {\r
+ // may be null\r
+ public String arg;\r
+ public int line;\r
+ public int type;\r
+\r
+ public static final int COMMENT () { return 0; }\r
+ public static final int WHITESPACE () { return 1; }\r
+ public static final int ALPHABETIC () { return 2; }\r
+ public static final int NUMERIC () { return 3; }\r
+\r
+ public static final int PARABREAK () { return 4; }\r
+ public static final int LINEBREAK () { return 5; }\r
+\r
+ public static final int APOSTROPHE () { return 10; }\r
+ public static final int PRIME () { return 11; }\r
+ public static final int OPENSINGLEQUOTE () { return 12; }\r
+ public static final int CLOSESINGLEQUOTE () { return 13; }\r
+ public static final int OPENDOUBLEQUOTE () { return 14; }\r
+ public static final int CLOSEDOUBLEQUOTE () { return 15; }\r
+ public static final int HYPHENS () { return 16; }\r
+ public static final int DOTS () { return 17; }\r
+\r
+ public static final int PARASTYLECOMMAND () { return 20; }\r
+ public static final int FORMATCOMMAND () { return 21; }\r
+ public static final int POPFORMATCOMMAND () { return 22; }\r
+ public static final int REFCOMMAND () { return 23; }\r
+ public static final int TAGCOMMAND () { return 24; }\r
+ public static final int CITECOMMAND () { return 25; }\r
+ public static final int CHARCOMMAND () { return 26; }\r
+ public static final int LOADCHARMAPCOMMAND () { return 27; }\r
+ public static final int LOADSTYLESHEETCOMMAND() { return 28; }\r
+ public static final int PREAMBLECOMMAND () { return 29; }\r
+ public static final int SEPARATORCOMMAND () { return 30; }\r
+\r
+ public static final int UNDERSCORE () { return 31; }\r
+ public static final int DOLLAR () { return 32; }\r
+ public static final int OTHER () { return 33; }\r
+ public static final int ENDOFSTREAM () { return 34; }\r
+\r
+ public static final int MAXTOKEN () { return 34; }\r
+ \r
+ public Token (int type, String arg, int line) {\r
+ this.type = type;\r
+ this.arg = arg;\r
+ this.line = line;\r
+ }\r
+ \r
+ public Token (int type, int line) {\r
+ this.type = type;\r
+ this.line = line;\r
+ }\r
+\r
+ // temporary implementation\r
+ public String toString () {\r
+ return arg;\r
+ }\r
+}\r
--- /dev/null
+# basic characters\r
+<char:linebreak><index:22>\r
+\r
+# dots\r
+<char:cdot><index:22>\r
+\r
+# quotes\r
+<char:quote><index:22>\r
+<char:quoteleft><index:22>\r
+<char:quoteright><index:22>\r
+<char:quotedblleft><index:22>\r
+<char:quotedblright><index:22>\r
+\r
+#dashes\r
+<char:hyphen><index:22>\r
+<char:endash><index:22>\r
+<char:emdash><index:22>\r
+\r
+# math symbols\r
+<char:oplus><index:22>\r
+<char:langle><index:22>\r
+<char:rangle><index:22>\r
+<char:textarrow><index:22>\r
+<char:hat><index:22>\r
+<char:fatsemi><index:22>\r
+<char:forall><index:22>\r
+<char:fatdot><index:22>\r
+<char:fatsemi><index:22>\r
+<char:implies><index:22>\r
+<char:exists><index:22>\r
+<char:and><index:22>\r
--- /dev/null
+# character map for Lucida New Math Extended font\r
+\r
+<char:parenleftbig><font:LucidNewMatExtT><index:161>\r
+<char:parenrightbig><font:LucidNewMatExtT><index:162>\r
+<char:bracketleftbig><font:LucidNewMatExtT><index:163>\r
+<char:bracketrightbig><font:LucidNewMatExtT><index:164>\r
+<char:floorleftbig><font:LucidNewMatExtT><index:165>\r
+<char:floorrightbig><font:LucidNewMatExtT><index:166>\r
+<char:ceilingleftbig><font:LucidNewMatExtT><index:167>\r
+<char:ceilingrightbig><font:LucidNewMatExtT><index:168>\r
+<char:braceleftbig><font:LucidNewMatExtT><index:169>\r
+<char:bracerightbig><font:LucidNewMatExtT><index:170>\r
+<char:angbracketleftbig><font:LucidNewMatExtT><index:173>\r
+<char:angbracketrightbig><font:LucidNewMatExtT><index:174>\r
+<char:vextendsingle><font:LucidNewMatExtT><index:175>\r
+<char:vextenddouble><font:LucidNewMatExtT><index:176>\r
+<char:slashbig><font:LucidNewMatExtT><index:177>\r
+<char:backslashbig><font:LucidNewMatExtT><index:178>\r
+<char:parenleftBig><font:LucidNewMatExtT><index:179>\r
+<char:parenrightBig><font:LucidNewMatExtT><index:180>\r
+<char:parenleftbigg><font:LucidNewMatExtT><index:181>\r
+<char:parenrightbigg><font:LucidNewMatExtT><index:182>\r
+<char:bracketleftbigg><font:LucidNewMatExtT><index:183>\r
+<char:bracketrightbigg><font:LucidNewMatExtT><index:184>\r
+<char:floorleftbigg><font:LucidNewMatExtT><index:185>\r
+<char:floorrightbigg><font:LucidNewMatExtT><index:186>\r
+<char:ceilingleftbigg><font:LucidNewMatExtT><index:187>\r
+<char:ceilingrightbigg><font:LucidNewMatExtT><index:188>\r
+<char:braceleftbigg><font:LucidNewMatExtT><index:189>\r
+<char:bracerightbigg><font:LucidNewMatExtT><index:190>\r
+<char:angbracketleftbigg><font:LucidNewMatExtT><index:28>\r
+<char:angbracketrightbigg><font:LucidNewMatExtT><index:29>\r
+<char:slashbigg><font:LucidNewMatExtT><index:193>\r
+<char:backslashbigg><font:LucidNewMatExtT><index:194>\r
+<char:parenleftBigg><font:LucidNewMatExtT><index:195>\r
+<char:parenrightBigg><font:LucidNewMatExtT><index:33>\r
+<char:bracketleftBigg><font:LucidNewMatExtT><index:34>\r
+<char:bracketrightBigg><font:LucidNewMatExtT><index:35>\r
+<char:floorleftBigg><font:LucidNewMatExtT><index:36>\r
+<char:floorrightBigg><font:LucidNewMatExtT><index:37>\r
+<char:ceilingleftBigg><font:LucidNewMatExtT><index:38>\r
+<char:ceilingrightBigg><font:LucidNewMatExtT><index:39>\r
+<char:braceleftBigg><font:LucidNewMatExtT><index:40>\r
+<char:bracerightBigg><font:LucidNewMatExtT><index:41>\r
+<char:angbracketleftBigg><font:LucidNewMatExtT><index:42>\r
+<char:angbracketrightBigg><font:LucidNewMatExtT><index:43>\r
+<char:slashBigg><font:LucidNewMatExtT><index:44>\r
+<char:backslashBigg><font:LucidNewMatExtT><index:45>\r
+<char:slashBig><font:LucidNewMatExtT><index:46>\r
+<char:backslashBig><font:LucidNewMatExtT><index:47>\r
+<char:parenlefttp><font:LucidNewMatExtT><index:48>\r
+<char:parenrighttp><font:LucidNewMatExtT><index:49>\r
+<char:bracketlefttp><font:LucidNewMatExtT><index:50>\r
+<char:bracketrighttp><font:LucidNewMatExtT><index:51>\r
+<char:bracketleftbt><font:LucidNewMatExtT><index:52>\r
+<char:bracketrightbt><font:LucidNewMatExtT><index:53>\r
+<char:bracketleftex><font:LucidNewMatExtT><index:54>\r
+<char:bracketrightex><font:LucidNewMatExtT><index:55>\r
+<char:bracelefttp><font:LucidNewMatExtT><index:56>\r
+<char:bracerighttp><font:LucidNewMatExtT><index:57>\r
+<char:braceleftbt><font:LucidNewMatExtT><index:58>\r
+<char:bracerightbt><font:LucidNewMatExtT><index:59>\r
+<char:braceleftmid><font:LucidNewMatExtT><index:60>\r
+<char:bracerightmid><font:LucidNewMatExtT><index:61>\r
+<char:braceex><font:LucidNewMatExtT><index:62>\r
+<char:arrowvertex><font:LucidNewMatExtT><index:63>\r
+<char:parenleftbt><font:LucidNewMatExtT><index:64>\r
+<char:parenrightbt><font:LucidNewMatExtT><index:65>\r
+<char:parenleftex><font:LucidNewMatExtT><index:66>\r
+<char:parenrightex><font:LucidNewMatExtT><index:67>\r
+<char:angbracketleftBig><font:LucidNewMatExtT><index:68>\r
+<char:angbracketrightBig><font:LucidNewMatExtT><index:69>\r
+<char:unionsqtext><font:LucidNewMatExtT><index:70>\r
+<char:unionsqdisplay><font:LucidNewMatExtT><index:71>\r
+<char:contintegraltext><font:LucidNewMatExtT><index:72>\r
+<char:contintegraldisplay><font:LucidNewMatExtT><index:73>\r
+<char:circledottext><font:LucidNewMatExtT><index:74>\r
+<char:circledotdisplay><font:LucidNewMatExtT><index:75>\r
+<char:circleplustext><font:LucidNewMatExtT><index:76>\r
+<char:circleplusdisplay><font:LucidNewMatExtT><index:77>\r
+<char:circlemultiplytext><font:LucidNewMatExtT><index:78>\r
+<char:circlemultiplydisplay><font:LucidNewMatExtT><index:79>\r
+<char:summationtext><font:LucidNewMatExtT><index:80>\r
+<char:producttext><font:LucidNewMatExtT><index:81>\r
+<char:integraltext><font:LucidNewMatExtT><index:82>\r
+<char:uniontext><font:LucidNewMatExtT><index:83>\r
+<char:intersectiontext><font:LucidNewMatExtT><index:84>\r
+<char:unionmultitext><font:LucidNewMatExtT><index:85>\r
+<char:logicalandtext><font:LucidNewMatExtT><index:86>\r
+<char:logicalortext><font:LucidNewMatExtT><index:87>\r
+<char:summationdisplay><font:LucidNewMatExtT><index:88>\r
+<char:productdisplay><font:LucidNewMatExtT><index:89>\r
+<char:integraldisplay><font:LucidNewMatExtT><index:90>\r
+<char:uniondisplay><font:LucidNewMatExtT><index:91>\r
+<char:intersectiondisplay><font:LucidNewMatExtT><index:92>\r
+<char:unionmultidisplay><font:LucidNewMatExtT><index:93>\r
+<char:logicalanddisplay><font:LucidNewMatExtT><index:94>\r
+<char:logicalordisplay><font:LucidNewMatExtT><index:95>\r
+<char:coproducttext><font:LucidNewMatExtT><index:96>\r
+<char:coproductdisplay><font:LucidNewMatExtT><index:97>\r
+<char:hatwide><font:LucidNewMatExtT><index:98>\r
+<char:hatwider><font:LucidNewMatExtT><index:99>\r
+<char:hatwidest><font:LucidNewMatExtT><index:100>\r
+<char:tildewide><font:LucidNewMatExtT><index:101>\r
+<char:tildewider><font:LucidNewMatExtT><index:102>\r
+<char:tildewidest><font:LucidNewMatExtT><index:103>\r
+<char:bracketleftBig><font:LucidNewMatExtT><index:104>\r
+<char:bracketrightBig><font:LucidNewMatExtT><index:105>\r
+<char:floorleftBig><font:LucidNewMatExtT><index:106>\r
+<char:floorrightBig><font:LucidNewMatExtT><index:107>\r
+<char:ceilingleftBig><font:LucidNewMatExtT><index:108>\r
+<char:ceilingrightBig><font:LucidNewMatExtT><index:109>\r
+<char:braceleftBig><font:LucidNewMatExtT><index:110>\r
+<char:bracerightBig><font:LucidNewMatExtT><index:111>\r
+<char:radicalbig><font:LucidNewMatExtT><index:112>\r
+<char:radicalBig><font:LucidNewMatExtT><index:113>\r
+<char:radicalbigg><font:LucidNewMatExtT><index:114>\r
+<char:radicalBigg><font:LucidNewMatExtT><index:115>\r
+<char:radicalbt><font:LucidNewMatExtT><index:116>\r
+<char:radicalvertex><font:LucidNewMatExtT><index:117>\r
+<char:radicaltp><font:LucidNewMatExtT><index:118>\r
+<char:arrowvertexdbl><font:LucidNewMatExtT><index:119>\r
+<char:arrowtp><font:LucidNewMatExtT><index:120>\r
+<char:arrowbt><font:LucidNewMatExtT><index:121>\r
+<char:bracehtipdownleft><font:LucidNewMatExtT><index:122>\r
+<char:bracehtipdownright><font:LucidNewMatExtT><index:123>\r
+<char:bracehtipupleft><font:LucidNewMatExtT><index:124>\r
+<char:bracehtipupright><font:LucidNewMatExtT><index:125>\r
+<char:arrowdbltp><font:LucidNewMatExtT><index:126>\r
+<char:arrowdblbt><font:LucidNewMatExtT><index:196>\r
--- /dev/null
+# character map for Lucida Math Italic font\r
+\r
+<char:Gamma><font:LucidNewMatItaT><index:161>\r
+<char:Delta><font:LucidNewMatItaT><index:162>\r
+<char:Theta><font:LucidNewMatItaT><index:163>\r
+<char:Lambda><font:LucidNewMatItaT><index:164>\r
+<char:Xi><font:LucidNewMatItaT><index:165>\r
+<char:Pi><font:LucidNewMatItaT><index:166>\r
+<char:Sigma><font:LucidNewMatItaT><index:167>\r
+<char:Upsilon><font:LucidNewMatItaT><index:7>\r
+<char:Phi><font:LucidNewMatItaT><index:169>\r
+<char:Psi><font:LucidNewMatItaT><index:170>\r
+<char:Omega><font:LucidNewMatItaT><index:173>\r
+<char:alpha><font:LucidNewMatItaT><index:174>\r
+<char:beta><font:LucidNewMatItaT><index:175>\r
+<char:gamma><font:LucidNewMatItaT><index:176>\r
+<char:delta><font:LucidNewMatItaT><index:177>\r
+<char:epsilon1><font:LucidNewMatItaT><index:178>\r
+<char:zeta><font:LucidNewMatItaT><index:179>\r
+<char:eta><font:LucidNewMatItaT><index:180>\r
+<char:theta><font:LucidNewMatItaT><index:181>\r
+<char:iota><font:LucidNewMatItaT><index:182>\r
+<char:kappa><font:LucidNewMatItaT><index:183>\r
+<char:lambda><font:LucidNewMatItaT><index:184>\r
+<char:mu><font:LucidNewMatItaT><index:185>\r
+<char:nu><font:LucidNewMatItaT><index:186>\r
+<char:xi><font:LucidNewMatItaT><index:187>\r
+<char:pi><font:LucidNewMatItaT><index:188>\r
+<char:rho><font:LucidNewMatItaT><index:189>\r
+<char:sigma><font:LucidNewMatItaT><index:190>\r
+<char:tau><font:LucidNewMatItaT><index:191>\r
+<char:upsilon><font:LucidNewMatItaT><index:192>\r
+<char:phi><font:LucidNewMatItaT><index:193>\r
+<char:chi><font:LucidNewMatItaT><index:194>\r
+<char:psi><font:LucidNewMatItaT><index:195>\r
+<char:tie><font:LucidNewMatItaT><index:196>\r
+<char:omega><font:LucidNewMatItaT><index:33>\r
+<char:epsilon><font:LucidNewMatItaT><index:34>\r
+<char:theta1><font:LucidNewMatItaT><index:35>\r
+<char:pi1><font:LucidNewMatItaT><index:36>\r
+<char:rho1><font:LucidNewMatItaT><index:37>\r
+<char:sigma1><font:LucidNewMatItaT><index:38>\r
+<char:phi1><font:LucidNewMatItaT><index:39>\r
+<char:arrowlefttophalf><font:LucidNewMatItaT><index:40>\r
+<char:arrowleftbothalf><font:LucidNewMatItaT><index:41>\r
+<char:arrowrighttophalf><font:LucidNewMatItaT><index:42>\r
+<char:arrowrightbothalf><font:LucidNewMatItaT><index:43>\r
+<char:arrowhookleft><font:LucidNewMatItaT><index:44>\r
+<char:arrowhookright><font:LucidNewMatItaT><index:45>\r
+<char:triangleright><font:LucidNewMatItaT><index:46>\r
+<char:triangleleft><font:LucidNewMatItaT><index:47>\r
+<char:period><font:LucidNewMatItaT><index:58>\r
+<char:comma><font:LucidNewMatItaT><index:59>\r
+<char:less><font:LucidNewMatItaT><index:60>\r
+<char:slash><font:LucidNewMatItaT><index:61>\r
+<char:greater><font:LucidNewMatItaT><index:62>\r
+<char:star><font:LucidNewMatItaT><index:63>\r
+<char:partialdiff><font:LucidNewMatItaT><index:64>\r
+<char:flat><font:LucidNewMatItaT><index:91>\r
+<char:natural><font:LucidNewMatItaT><index:92>\r
+<char:sharp><font:LucidNewMatItaT><index:93>\r
+<char:slurbelow><font:LucidNewMatItaT><index:94>\r
+<char:slurabove><font:LucidNewMatItaT><index:95>\r
+<char:lscript><font:LucidNewMatItaT><index:96>\r
+<char:dotlessi><font:LucidNewMatItaT><index:123>\r
+<char:dotlessj><font:LucidNewMatItaT><index:124>\r
+<char:weierstrass><font:LucidNewMatItaT><index:125>\r
+<char:vector><font:LucidNewMatItaT><index:126>\r
--- /dev/null
+# mathematical characters for Lucida New Math Symbol font\r
+\r
+<char:minus><font:LucidNewMatSymT><index:161>\r
+<char:periodcentered><font:LucidNewMatSymT><index:162>\r
+<char:multiply><font:LucidNewMatSymT><index:163>\r
+<char:asteriskmath><font:LucidNewMatSymT><index:164>\r
+<char:divide><font:LucidNewMatSymT><index:165>\r
+<char:diamondmath><font:LucidNewMatSymT><index:166>\r
+<char:plusminus><font:LucidNewMatSymT><index:167>\r
+<char:minusplus><font:LucidNewMatSymT><index:168>\r
+<char:circleplus><font:LucidNewMatSymT><index:169>\r
+<char:circleminus><font:LucidNewMatSymT><index:170>\r
+<char:circlemultiply><font:LucidNewMatSymT><index:173>\r
+<char:circledivide><font:LucidNewMatSymT><index:174>\r
+<char:circledot><font:LucidNewMatSymT><index:175>\r
+<char:circlecopyrt><font:LucidNewMatSymT><index:176>\r
+<char:openbullet><font:LucidNewMatSymT><index:177>\r
+<char:bullet><font:LucidNewMatSymT><index:178>\r
+<char:equivasymptotic><font:LucidNewMatSymT><index:179>\r
+<char:equivalence><font:LucidNewMatSymT><index:180>\r
+<char:reflexsubset><font:LucidNewMatSymT><index:181>\r
+<char:reflexsuperset><font:LucidNewMatSymT><index:182>\r
+<char:lessequal><font:LucidNewMatSymT><index:183>\r
+<char:greaterequal><font:LucidNewMatSymT><index:184>\r
+<char:precedesequal><font:LucidNewMatSymT><index:185>\r
+<char:followsequal><font:LucidNewMatSymT><index:186>\r
+<char:similar><font:LucidNewMatSymT><index:187>\r
+<char:approxequal><font:LucidNewMatSymT><index:188>\r
+<char:propersubset><font:LucidNewMatSymT><index:189>\r
+<char:propersuperset><font:LucidNewMatSymT><index:190>\r
+<char:lessmuch><font:LucidNewMatSymT><index:191>\r
+<char:greatermuch><font:LucidNewMatSymT><index:192>\r
+<char:precedes><font:LucidNewMatSymT><index:193>\r
+<char:follows><font:LucidNewMatSymT><index:194>\r
+<char:arrowleft><font:LucidNewMatSymT><index:195>\r
+<char:spade><font:LucidNewMatSymT><index:196>\r
+<char:arrowright><font:LucidNewMatSymT><index:33>\r
+<char:arrowup><font:LucidNewMatSymT><index:34>\r
+<char:arrowdown><font:LucidNewMatSymT><index:35>\r
+<char:arrowboth><font:LucidNewMatSymT><index:36>\r
+<char:arrownortheast><font:LucidNewMatSymT><index:37>\r
+<char:arrowsoutheast><font:LucidNewMatSymT><index:38>\r
+<char:similarequal><font:LucidNewMatSymT><index:39>\r
+<char:arrowdblleft><font:LucidNewMatSymT><index:40>\r
+<char:arrowdblright><font:LucidNewMatSymT><index:41>\r
+<char:arrowdblup><font:LucidNewMatSymT><index:42>\r
+<char:arrowdbldown><font:LucidNewMatSymT><index:43>\r
+<char:arrowdblboth><font:LucidNewMatSymT><index:44>\r
+<char:arrownorthwest><font:LucidNewMatSymT><index:45>\r
+<char:arrowsouthwest><font:LucidNewMatSymT><index:46>\r
+<char:proportional><font:LucidNewMatSymT><index:47>\r
+<char:prime><font:LucidNewMatSymT><index:48>\r
+<char:infinity><font:LucidNewMatSymT><index:49>\r
+<char:element><font:LucidNewMatSymT><index:50>\r
+<char:owner><font:LucidNewMatSymT><index:51>\r
+<char:triangle><font:LucidNewMatSymT><index:52>\r
+<char:triangleinv><font:LucidNewMatSymT><index:53>\r
+<char:negationslash><font:LucidNewMatSymT><index:54>\r
+<char:mapsto><font:LucidNewMatSymT><index:55>\r
+<char:universal><font:LucidNewMatSymT><index:56>\r
+<char:existential><font:LucidNewMatSymT><index:57>\r
+<char:logicalnot><font:LucidNewMatSymT><index:58>\r
+<char:emptyset><font:LucidNewMatSymT><index:59>\r
+<char:Rfractur><font:LucidNewMatSymT><index:60>\r
+<char:Ifractur><font:LucidNewMatSymT><index:61>\r
+<char:latticetop><font:LucidNewMatSymT><index:62>\r
+<char:perpendicular><font:LucidNewMatSymT><index:63>\r
+<char:aleph><font:LucidNewMatSymT><index:64>\r
+<char:scriptA><font:LucidNewMatSymT><index:65>\r
+<char:scriptB><font:LucidNewMatSymT><index:66>\r
+<char:scriptC><font:LucidNewMatSymT><index:67>\r
+<char:scriptD><font:LucidNewMatSymT><index:68>\r
+<char:scriptE><font:LucidNewMatSymT><index:69>\r
+<char:scriptF><font:LucidNewMatSymT><index:70>\r
+<char:scriptG><font:LucidNewMatSymT><index:71>\r
+<char:scriptH><font:LucidNewMatSymT><index:72>\r
+<char:scriptI><font:LucidNewMatSymT><index:73>\r
+<char:scriptJ><font:LucidNewMatSymT><index:74>\r
+<char:scriptK><font:LucidNewMatSymT><index:75>\r
+<char:scriptL><font:LucidNewMatSymT><index:76>\r
+<char:scriptM><font:LucidNewMatSymT><index:77>\r
+<char:scriptN><font:LucidNewMatSymT><index:78>\r
+<char:scriptO><font:LucidNewMatSymT><index:79>\r
+<char:scriptP><font:LucidNewMatSymT><index:80>\r
+<char:scriptQ><font:LucidNewMatSymT><index:81>\r
+<char:scriptR><font:LucidNewMatSymT><index:82>\r
+<char:scriptS><font:LucidNewMatSymT><index:83>\r
+<char:scriptT><font:LucidNewMatSymT><index:84>\r
+<char:scriptU><font:LucidNewMatSymT><index:85>\r
+<char:scriptV><font:LucidNewMatSymT><index:86>\r
+<char:scriptW><font:LucidNewMatSymT><index:87>\r
+<char:scriptX><font:LucidNewMatSymT><index:88>\r
+<char:scriptY><font:LucidNewMatSymT><index:89>\r
+<char:scriptZ><font:LucidNewMatSymT><index:90>\r
+<char:union><font:LucidNewMatSymT><index:91>\r
+<char:intersection><font:LucidNewMatSymT><index:92>\r
+<char:unionmulti><font:LucidNewMatSymT><index:93>\r
+<char:logicaland><font:LucidNewMatSymT><index:94>\r
+<char:logicalor><font:LucidNewMatSymT><index:95>\r
+<char:turnstileleft><font:LucidNewMatSymT><index:96>\r
+<char:turnstileright><font:LucidNewMatSymT><index:97>\r
+<char:floorleft><font:LucidNewMatSymT><index:98>\r
+<char:floorright><font:LucidNewMatSymT><index:99>\r
+<char:ceilingleft><font:LucidNewMatSymT><index:100>\r
+<char:ceilingright><font:LucidNewMatSymT><index:101>\r
+<char:braceleft><font:LucidNewMatSymT><index:102>\r
+<char:braceright><font:LucidNewMatSymT><index:103>\r
+<char:angbracketleft><font:LucidNewMatSymT><index:104>\r
+<char:angbracketright><font:LucidNewMatSymT><index:105>\r
+<char:bar><font:LucidNewMatSymT><index:106>\r
+<char:bardbl><font:LucidNewMatSymT><index:107>\r
+<char:arrowbothv><font:LucidNewMatSymT><index:108>\r
+<char:arrowdblbothv><font:LucidNewMatSymT><index:109>\r
+<char:backslash><font:LucidNewMatSymT><index:110>\r
+<char:wreathproduct><font:LucidNewMatSymT><index:111>\r
+<char:radical><font:LucidNewMatSymT><index:112>\r
+<char:coproduct><font:LucidNewMatSymT><index:113>\r
+<char:nabla><font:LucidNewMatSymT><index:114>\r
+<char:integral><font:LucidNewMatSymT><index:115>\r
+<char:unionsq><font:LucidNewMatSymT><index:116>\r
+<char:intersectionsq><font:LucidNewMatSymT><index:117>\r
+<char:subsetsqequal><font:LucidNewMatSymT><index:118>\r
+<char:supersetsqequal><font:LucidNewMatSymT><index:119>\r
+<char:section><font:LucidNewMatSymT><index:120>\r
+<char:dagger><font:LucidNewMatSymT><index:121>\r
+<char:daggerdbl><font:LucidNewMatSymT><index:122>\r
+<char:paragraph><font:LucidNewMatSymT><index:123>\r
+<char:club><font:LucidNewMatSymT><index:124>\r
+<char:diamond><font:LucidNewMatSymT><index:125>\r
+<char:heart><font:LucidNewMatSymT><index:126>\r
--- /dev/null
+MAIN_CLASS=Tagger
+
+PROGRAM=test
+SOURCE_FILES=*.java
+
+BUILDSCRIPT=~/research/Robust/src/buildscript
+BSFLAGS= -debug -nooptimize -mainclass $(MAIN_CLASS) -justanalyze -ownership -ownallocdepth 1 -ownwritedots final -ownaliasfile aliases.txt -enable-assertions
+
+all: run
+
+run: $(PROGRAM).bin
+# $(PROGRAM).bin test
+
+view: PNGs
+ eog *.png &
+
+PNGs: DOTs
+ d2p *COMPLETE*.dot
+
+DOTs: $(PROGRAM).bin
+
+$(PROGRAM).bin: $(SOURCE_FILES)
+ $(BUILDSCRIPT) $(BSFLAGS) -o $(PROGRAM) $(SOURCE_FILES)
+
+clean:
+ rm -f $(PROGRAM).bin
+ rm -fr tmpbuilddirectory
+ rm -f *~
+ rm -f *.dot
+ rm -f *.png
+ rm -f aliases.txt
+ rm -f test.index.txt
+ rm -f test.tag.txt
--- /dev/null
+# character map for standard font\r
+\r
+<char:space><font:><index:32>\r
+<char:exclam><font:><index:33>\r
+<char:quotedbl><font:><index:34>\r
+<char:numbersign><font:><index:35>\r
+<char:dollar><font:><index:36>\r
+<char:percent><font:><index:37>\r
+<char:ampersand><font:><index:38>\r
+<char:quotesingle><font:><index:39>\r
+<char:parenleft><font:><index:40>\r
+<char:parenright><font:><index:41>\r
+<char:asterisk><font:><index:42>\r
+<char:plus><font:><index:43>\r
+<char:comma><font:><index:44>\r
+<char:hyphen><font:><index:45>\r
+<char:period><font:><index:46>\r
+<char:slash><font:><index:47>\r
+<char:zero><font:><index:48>\r
+<char:one><font:><index:49>\r
+<char:two><font:><index:50>\r
+<char:three><font:><index:51>\r
+<char:four><font:><index:52>\r
+<char:five><font:><index:53>\r
+<char:six><font:><index:54>\r
+<char:seven><font:><index:55>\r
+<char:eight><font:><index:56>\r
+<char:nine><font:><index:57>\r
+<char:colon><font:><index:58>\r
+<char:semicolon><font:><index:59>\r
+<char:less><font:><index:60>\r
+<char:equal><font:><index:61>\r
+<char:greater><font:><index:62>\r
+<char:question><font:><index:63>\r
+<char:at><font:><index:64>\r
+<char:A><font:><index:65>\r
+<char:B><font:><index:66>\r
+<char:C><font:><index:67>\r
+<char:D><font:><index:68>\r
+<char:E><font:><index:69>\r
+<char:F><font:><index:70>\r
+<char:G><font:><index:71>\r
+<char:H><font:><index:72>\r
+<char:I><font:><index:73>\r
+<char:J><font:><index:74>\r
+<char:K><font:><index:75>\r
+<char:L><font:><index:76>\r
+<char:M><font:><index:77>\r
+<char:N><font:><index:78>\r
+<char:O><font:><index:79>\r
+<char:P><font:><index:80>\r
+<char:Q><font:><index:81>\r
+<char:R><font:><index:82>\r
+<char:S><font:><index:83>\r
+<char:T><font:><index:84>\r
+<char:U><font:><index:85>\r
+<char:V><font:><index:86>\r
+<char:W><font:><index:87>\r
+<char:X><font:><index:88>\r
+<char:Y><font:><index:89>\r
+<char:Z><font:><index:90>\r
+<char:bracketleft><font:><index:91>\r
+<char:backslash><font:><index:92>\r
+<char:bracketright><font:><index:93>\r
+<char:asciicircum><font:><index:94>\r
+<char:underscore><font:><index:95>\r
+<char:grave><font:><index:96>\r
+<char:a><font:><index:97>\r
+<char:b><font:><index:98>\r
+<char:c><font:><index:99>\r
+<char:d><font:><index:100>\r
+<char:e><font:><index:101>\r
+<char:f><font:><index:102>\r
+<char:g><font:><index:103>\r
+<char:h><font:><index:104>\r
+<char:i><font:><index:105>\r
+<char:j><font:><index:106>\r
+<char:k><font:><index:107>\r
+<char:l><font:><index:108>\r
+<char:m><font:><index:109>\r
+<char:n><font:><index:110>\r
+<char:o><font:><index:111>\r
+<char:p><font:><index:112>\r
+<char:q><font:><index:113>\r
+<char:r><font:><index:114>\r
+<char:s><font:><index:115>\r
+<char:t><font:><index:116>\r
+<char:u><font:><index:117>\r
+<char:v><font:><index:118>\r
+<char:w><font:><index:119>\r
+<char:x><font:><index:120>\r
+<char:y><font:><index:121>\r
+<char:z><font:><index:122>\r
+<char:braceleft><font:><index:123>\r
+<char:bar><font:><index:124>\r
+<char:braceright><font:><index:125>\r
+<char:asciitilde><font:><index:126>\r
+<char:euro><font:><index:128>\r
+<char:quotesinglbase><font:><index:130>\r
+<char:florin><font:><index:131>\r
+<char:quotedblbase><font:><index:132>\r
+<char:ellipsis><font:><index:133>\r
+<char:dagger><font:><index:134>\r
+<char:daggerdbl><font:><index:135>\r
+<char:circumflex><font:><index:136>\r
+<char:perthousand><font:><index:137>\r
+<char:Scaron><font:><index:138>\r
+<char:guilsinglleft><font:><index:139>\r
+<char:OE><font:><index:140>\r
+<char:Zcaron><font:><index:142>\r
+<char:quoteleft><font:><index:145>\r
+<char:quoteright><font:><index:146>\r
+<char:quotedblleft><font:><index:147>\r
+<char:quotedblright><font:><index:148>\r
+<char:bullet><font:><index:149>\r
+<char:endash><font:><index:150>\r
+<char:emdash><font:><index:151>\r
+<char:tilde><font:><index:152>\r
+<char:trademark><font:><index:153>\r
+<char:scaron><font:><index:154>\r
+<char:guilsinglright><font:><index:155>\r
+<char:oe><font:><index:156>\r
+<char:zcaron><font:><index:158>\r
+<char:Ydieresis><font:><index:159>\r
+<char:nbspace><font:><index:160>\r
+<char:exclamdown><font:><index:161>\r
+<char:cent><font:><index:162>\r
+<char:sterling><font:><index:163>\r
+<char:currency><font:><index:164>\r
+<char:yen><font:><index:165>\r
+<char:brokenbar><font:><index:166>\r
+<char:section><font:><index:167>\r
+<char:dieresis><font:><index:168>\r
+<char:copyright><font:><index:169>\r
+<char:ordfeminine><font:><index:170>\r
+<char:guillemotleft><font:><index:171>\r
+<char:logicalnot><font:><index:172>\r
+<char:sfthyphen><font:><index:173>\r
+<char:registered><font:><index:174>\r
+<char:macron><font:><index:175>\r
+<char:degree><font:><index:176>\r
+<char:plusminus><font:><index:177>\r
+<char:twosuperior><font:><index:178>\r
+<char:threesuperior><font:><index:179>\r
+<char:acute><font:><index:180>\r
+<char:mu><font:><index:181>\r
+<char:paragraph><font:><index:182>\r
+<char:periodcentered><font:><index:183>\r
+<char:cedilla><font:><index:184>\r
+<char:onesuperior><font:><index:185>\r
+<char:ordmasculine><font:><index:186>\r
+<char:guillemotright><font:><index:187>\r
+<char:onequarter><font:><index:188>\r
+<char:onehalf><font:><index:189>\r
+<char:threequarters><font:><index:190>\r
+<char:questiondown><font:><index:191>\r
+<char:Agrave><font:><index:192>\r
+<char:Aacute><font:><index:193>\r
+<char:Acircumflex><font:><index:194>\r
+<char:Atilde><font:><index:195>\r
+<char:Adieresis><font:><index:196>\r
+<char:Aring><font:><index:197>\r
+<char:AE><font:><index:198>\r
+<char:Ccedilla><font:><index:199>\r
+<char:Egrave><font:><index:200>\r
+<char:Eacute><font:><index:201>\r
+<char:Ecircumflex><font:><index:202>\r
+<char:Edieresis><font:><index:203>\r
+<char:Igrave><font:><index:204>\r
+<char:Iacute><font:><index:205>\r
+<char:Icircumflex><font:><index:206>\r
+<char:Idieresis><font:><index:207>\r
+<char:Eth><font:><index:208>\r
+<char:Ntilde><font:><index:209>\r
+<char:Ograve><font:><index:210>\r
+<char:Oacute><font:><index:211>\r
+<char:Ocircumflex><font:><index:212>\r
+<char:Otilde><font:><index:213>\r
+<char:Odieresis><font:><index:214>\r
+<char:multiply><font:><index:215>\r
+<char:Oslash><font:><index:216>\r
+<char:Ugrave><font:><index:217>\r
+<char:Uacute><font:><index:218>\r
+<char:Ucircumflex><font:><index:219>\r
+<char:Udieresis><font:><index:220>\r
+<char:Yacute><font:><index:221>\r
+<char:Thorn><font:><index:222>\r
+<char:germandbls><font:><index:223>\r
+<char:agrave><font:><index:224>\r
+<char:aacute><font:><index:225>\r
+<char:acircumflex><font:><index:226>\r
+<char:atilde><font:><index:227>\r
+<char:adieresis><font:><index:228>\r
+<char:aring><font:><index:229>\r
+<char:ae><font:><index:230>\r
+<char:ccedilla><font:><index:231>\r
+<char:egrave><font:><index:232>\r
+<char:eacute><font:><index:233>\r
+<char:ecircumflex><font:><index:234>\r
+<char:edieresis><font:><index:235>\r
+<char:igrave><font:><index:236>\r
+<char:iacute><font:><index:237>\r
+<char:icircumflex><font:><index:238>\r
+<char:idieresis><font:><index:239>\r
+<char:eth><font:><index:240>\r
+<char:ntilde><font:><index:241>\r
+<char:ograve><font:><index:242>\r
+<char:oacute><font:><index:243>\r
+<char:ocircumflex><font:><index:244>\r
+<char:otilde><font:><index:245>\r
+<char:odieresis><font:><index:246>\r
+<char:divide><font:><index:247>\r
+<char:oslash><font:><index:248>\r
+<char:ugrave><font:><index:249>\r
+<char:uacute><font:><index:250>\r
+<char:ucircumflex><font:><index:251>\r
+<char:udieresis><font:><index:252>\r
+<char:yacute><font:><index:253>\r
+<char:thorn><font:><index:254>\r
+<char:ydieresis><font:><index:255>\r
--- /dev/null
+<style:title><next:author>\r
+<style:author><next:section>\r
+<style:section><next:noindent><counter:1><separator:.><trailer: >\r
+<style:opening><next:noindent>\r
+<style:noindent><next:body>\r
+<style:body><next:body>\r
+<style:subsection><next:noindent><parent:section><counter:1><separator:.><trailer: >\r
+<style:subsubsection><next:noindent><parent:subsection><counter:a><separator:.><trailer: >\r
+<style:geekmath><next:noindent>\r
+<style:point><next:noindent><counter:A><leader:\alpha >\r
+<style:ref><next:ref>\r
+\r
--- /dev/null
+# character map for Symbol font\r
+\r
+<char:Symbol><font:Symbol><index:for>\r
+<char:space><font:Symbol><index:32>\r
+<char:exclam><font:Symbol><index:33>\r
+<char:universal><font:Symbol><index:34>\r
+<char:numbersign><font:Symbol><index:35>\r
+<char:existential><font:Symbol><index:36>\r
+<char:percent><font:Symbol><index:37>\r
+<char:ampersand><font:Symbol><index:38>\r
+<char:suchthat><font:Symbol><index:39>\r
+<char:parenleft><font:Symbol><index:40>\r
+<char:parenright><font:Symbol><index:41>\r
+<char:asteriskmath><font:Symbol><index:42>\r
+<char:plus><font:Symbol><index:43>\r
+<char:comma><font:Symbol><index:44>\r
+<char:minus><font:Symbol><index:45>\r
+<char:period><font:Symbol><index:46>\r
+<char:slash><font:Symbol><index:47>\r
+<char:zero><font:Symbol><index:48>\r
+<char:one><font:Symbol><index:49>\r
+<char:two><font:Symbol><index:50>\r
+<char:three><font:Symbol><index:51>\r
+<char:four><font:Symbol><index:52>\r
+<char:five><font:Symbol><index:53>\r
+<char:six><font:Symbol><index:54>\r
+<char:seven><font:Symbol><index:55>\r
+<char:eight><font:Symbol><index:56>\r
+<char:nine><font:Symbol><index:57>\r
+<char:colon><font:Symbol><index:58>\r
+<char:semicolon><font:Symbol><index:59>\r
+<char:less><font:Symbol><index:60>\r
+<char:equal><font:Symbol><index:61>\r
+<char:greater><font:Symbol><index:62>\r
+<char:question><font:Symbol><index:63>\r
+<char:congruent><font:Symbol><index:64>\r
+<char:Alpha><font:Symbol><index:65>\r
+<char:Beta><font:Symbol><index:66>\r
+<char:Chi><font:Symbol><index:67>\r
+<char:Delta><font:Symbol><index:68>\r
+<char:Epsilon><font:Symbol><index:69>\r
+<char:Phi><font:Symbol><index:70>\r
+<char:Gamma><font:Symbol><index:71>\r
+<char:Eta><font:Symbol><index:72>\r
+<char:Iota><font:Symbol><index:73>\r
+<char:theta1><font:Symbol><index:74>\r
+<char:Kappa><font:Symbol><index:75>\r
+<char:Lambda><font:Symbol><index:76>\r
+<char:Mu><font:Symbol><index:77>\r
+<char:Nu><font:Symbol><index:78>\r
+<char:Omicron><font:Symbol><index:79>\r
+<char:Pi><font:Symbol><index:80>\r
+<char:Theta><font:Symbol><index:81>\r
+<char:Rho><font:Symbol><index:82>\r
+<char:Sigma><font:Symbol><index:83>\r
+<char:Tau><font:Symbol><index:84>\r
+<char:Upsilon><font:Symbol><index:85>\r
+<char:sigma1><font:Symbol><index:86>\r
+<char:Omega><font:Symbol><index:87>\r
+<char:Xi><font:Symbol><index:88>\r
+<char:Psi><font:Symbol><index:89>\r
+<char:Zeta><font:Symbol><index:90>\r
+<char:bracketleft><font:Symbol><index:91>\r
+<char:therefore><font:Symbol><index:92>\r
+<char:bracketright><font:Symbol><index:93>\r
+<char:perpendicular><font:Symbol><index:94>\r
+<char:underscore><font:Symbol><index:95>\r
+<char:radicalex><font:Symbol><index:96>\r
+<char:alpha><font:Symbol><index:97>\r
+<char:beta><font:Symbol><index:98>\r
+<char:chi><font:Symbol><index:99>\r
+<char:delta><font:Symbol><index:100>\r
+<char:epsilon><font:Symbol><index:101>\r
+<char:phi><font:Symbol><index:102>\r
+<char:gamma><font:Symbol><index:103>\r
+<char:eta><font:Symbol><index:104>\r
+<char:iota><font:Symbol><index:105>\r
+<char:phi1><font:Symbol><index:106>\r
+<char:kappa><font:Symbol><index:107>\r
+<char:lambda><font:Symbol><index:108>\r
+<char:mu><font:Symbol><index:109>\r
+<char:nu><font:Symbol><index:110>\r
+<char:omicron><font:Symbol><index:111>\r
+<char:pi><font:Symbol><index:112>\r
+<char:theta><font:Symbol><index:113>\r
+<char:rho><font:Symbol><index:114>\r
+<char:sigma><font:Symbol><index:115>\r
+<char:tau><font:Symbol><index:116>\r
+<char:upsilon><font:Symbol><index:117>\r
+<char:omega1><font:Symbol><index:118>\r
+<char:omega><font:Symbol><index:119>\r
+<char:xi><font:Symbol><index:120>\r
+<char:psi><font:Symbol><index:121>\r
+<char:zeta><font:Symbol><index:122>\r
+<char:braceleft><font:Symbol><index:123>\r
+<char:bar><font:Symbol><index:124>\r
+<char:braceright><font:Symbol><index:125>\r
+<char:similar><font:Symbol><index:126>\r
+<char:Euro><font:Symbol><index:160>\r
+<char:Upsilon1><font:Symbol><index:161>\r
+<char:minute><font:Symbol><index:162>\r
+<char:lessequal><font:Symbol><index:163>\r
+<char:fraction><font:Symbol><index:164>\r
+<char:infinity><font:Symbol><index:165>\r
+<char:florin><font:Symbol><index:166>\r
+<char:club><font:Symbol><index:167>\r
+<char:diamond><font:Symbol><index:168>\r
+<char:heart><font:Symbol><index:169>\r
+<char:spade><font:Symbol><index:170>\r
+<char:arrowboth><font:Symbol><index:171>\r
+<char:arrowleft><font:Symbol><index:172>\r
+<char:arrowup><font:Symbol><index:173>\r
+<char:arrowright><font:Symbol><index:174>\r
+<char:arrowdown><font:Symbol><index:175>\r
+<char:degree><font:Symbol><index:176>\r
+<char:plusminus><font:Symbol><index:177>\r
+<char:second><font:Symbol><index:178>\r
+<char:greaterequal><font:Symbol><index:179>\r
+<char:multiply><font:Symbol><index:180>\r
+<char:proportional><font:Symbol><index:181>\r
+<char:partialdiff><font:Symbol><index:182>\r
+<char:bullet><font:Symbol><index:183>\r
+<char:divide><font:Symbol><index:184>\r
+<char:notequal><font:Symbol><index:185>\r
+<char:equivalence><font:Symbol><index:186>\r
+<char:approxequal><font:Symbol><index:187>\r
+\r
+# seems to be a quarter fraction\r
+# <char:ellipsis><font:Symbol><index:188>\r
+\r
+<char:arrowvertex><font:Symbol><index:189>\r
+<char:arrowhorizex><font:Symbol><index:190>\r
+<char:carriagereturn><font:Symbol><index:191>\r
+<char:aleph><font:Symbol><index:192>\r
+<char:Ifraktur><font:Symbol><index:193>\r
+<char:Rfraktur><font:Symbol><index:194>\r
+<char:weierstrass><font:Symbol><index:195>\r
+<char:circlemultiply><font:Symbol><index:196>\r
+<char:circleplus><font:Symbol><index:197>\r
+<char:emptyset><font:Symbol><index:198>\r
+<char:intersection><font:Symbol><index:199>\r
+<char:union><font:Symbol><index:200>\r
+<char:propersuperset><font:Symbol><index:201>\r
+<char:reflexsuperset><font:Symbol><index:202>\r
+<char:notsubset><font:Symbol><index:203>\r
+<char:propersubset><font:Symbol><index:204>\r
+<char:reflexsubset><font:Symbol><index:205>\r
+<char:element><font:Symbol><index:206>\r
+<char:notelement><font:Symbol><index:207>\r
+<char:angle><font:Symbol><index:208>\r
+<char:gradient><font:Symbol><index:209>\r
+<char:registerserif><font:Symbol><index:210>\r
+<char:copyrightserif><font:Symbol><index:211>\r
+<char:trademarkserif><font:Symbol><index:212>\r
+<char:product><font:Symbol><index:213>\r
+<char:radical><font:Symbol><index:214>\r
+<char:dotmath><font:Symbol><index:215>\r
+<char:logicalnot><font:Symbol><index:216>\r
+<char:logicaland><font:Symbol><index:217>\r
+<char:logicalor><font:Symbol><index:218>\r
+<char:arrowdblboth><font:Symbol><index:219>\r
+<char:arrowdblleft><font:Symbol><index:220>\r
+<char:arrowdblup><font:Symbol><index:221>\r
+<char:arrowdblright><font:Symbol><index:222>\r
+<char:arrowdbldown><font:Symbol><index:223>\r
+<char:lozenge><font:Symbol><index:224>\r
+<char:angleleft><font:Symbol><index:225>\r
+<char:registersans><font:Symbol><index:226>\r
+<char:copyrightsans><font:Symbol><index:227>\r
+<char:trademarksans><font:Symbol><index:228>\r
+<char:summation><font:Symbol><index:229>\r
+<char:parenlefttp><font:Symbol><index:230>\r
+<char:parenleftex><font:Symbol><index:231>\r
+<char:parenleftbt><font:Symbol><index:232>\r
+<char:bracketlefttp><font:Symbol><index:233>\r
+<char:bracketleftex><font:Symbol><index:234>\r
+<char:bracketleftbt><font:Symbol><index:235>\r
+<char:bracelefttp><font:Symbol><index:236>\r
+<char:braceleftmid><font:Symbol><index:237>\r
+<char:braceleftbt><font:Symbol><index:238>\r
+<char:braceex><font:Symbol><index:239>\r
+<char:angleright><font:Symbol><index:241>\r
+<char:integral><font:Symbol><index:242>\r
+<char:integraltp><font:Symbol><index:243>\r
+<char:integralex><font:Symbol><index:244>\r
+<char:integralbt><font:Symbol><index:245>\r
+<char:parenrighttp><font:Symbol><index:246>\r
+<char:parenrightex><font:Symbol><index:247>\r
+<char:parenrightbt><font:Symbol><index:248>\r
+<char:bracketrighttp><font:Symbol><index:249>\r
+<char:bracketrightex><font:Symbol><index:250>\r
+<char:bracketrightbt><font:Symbol><index:251>\r
+<char:bracerighttp><font:Symbol><index:252>\r
+<char:bracerightmid><font:Symbol><index:253>\r
+<char:bracerightbt><font:Symbol><index:254>\r
--- /dev/null
+# character map for Lucida Math Italic font\r
+\r
+<char:Gamma><font:LucidNewMatItaT><index:161>\r
+<char:Delta><font:LucidNewMatItaT><index:162>\r
+<char:Theta><font:LucidNewMatItaT><index:163>\r
+<char:Lambda><font:LucidNewMatItaT><index:164>\r
+<char:Xi><font:LucidNewMatItaT><index:165>\r
+<char:Pi><font:LucidNewMatItaT><index:166>\r
+<char:Sigma><font:LucidNewMatItaT><index:167>\r
+<char:Upsilon><font:LucidNewMatItaT><index:7>\r
+<char:Phi><font:LucidNewMatItaT><index:169>\r
+<char:Psi><font:LucidNewMatItaT><index:170>\r
+<char:Omega><font:LucidNewMatItaT><index:173>\r
+<char:alpha><font:LucidNewMatItaT><index:174>\r
+<char:beta><font:LucidNewMatItaT><index:175>\r
+<char:gamma><font:LucidNewMatItaT><index:176>\r
+<char:delta><font:LucidNewMatItaT><index:177>\r
+<char:epsilon1><font:LucidNewMatItaT><index:178>\r
+<char:zeta><font:LucidNewMatItaT><index:179>\r
+<char:eta><font:LucidNewMatItaT><index:180>\r
+<char:theta><font:LucidNewMatItaT><index:181>\r
+<char:iota><font:LucidNewMatItaT><index:182>\r
+<char:kappa><font:LucidNewMatItaT><index:183>\r
+<char:lambda><font:LucidNewMatItaT><index:184>\r
+<char:mu><font:LucidNewMatItaT><index:185>\r
+<char:nu><font:LucidNewMatItaT><index:186>\r
+<char:xi><font:LucidNewMatItaT><index:187>\r
+<char:pi><font:LucidNewMatItaT><index:188>\r
+<char:rho><font:LucidNewMatItaT><index:189>\r
+<char:sigma><font:LucidNewMatItaT><index:190>\r
+<char:tau><font:LucidNewMatItaT><index:191>\r
+<char:upsilon><font:LucidNewMatItaT><index:192>\r
+<char:phi><font:LucidNewMatItaT><index:193>\r
+<char:chi><font:LucidNewMatItaT><index:194>\r
+<char:psi><font:LucidNewMatItaT><index:195>\r
+<char:tie><font:LucidNewMatItaT><index:196>\r
+<char:omega><font:LucidNewMatItaT><index:33>\r
+<char:epsilon><font:LucidNewMatItaT><index:34>\r
+<char:theta1><font:LucidNewMatItaT><index:35>\r
+<char:pi1><font:LucidNewMatItaT><index:36>\r
+<char:rho1><font:LucidNewMatItaT><index:37>\r
+<char:sigma1><font:LucidNewMatItaT><index:38>\r
+<char:phi1><font:LucidNewMatItaT><index:39>\r
+<char:arrowlefttophalf><font:LucidNewMatItaT><index:40>\r
+<char:arrowleftbothalf><font:LucidNewMatItaT><index:41>\r
+<char:arrowrighttophalf><font:LucidNewMatItaT><index:42>\r
+<char:arrowrightbothalf><font:LucidNewMatItaT><index:43>\r
+<char:arrowhookleft><font:LucidNewMatItaT><index:44>\r
+<char:arrowhookright><font:LucidNewMatItaT><index:45>\r
+<char:triangleright><font:LucidNewMatItaT><index:46>\r
+<char:triangleleft><font:LucidNewMatItaT><index:47>\r
+<char:period><font:LucidNewMatItaT><index:58>\r
+<char:comma><font:LucidNewMatItaT><index:59>\r
+<char:less><font:LucidNewMatItaT><index:60>\r
+<char:slash><font:LucidNewMatItaT><index:61>\r
+<char:greater><font:LucidNewMatItaT><index:62>\r
+<char:star><font:LucidNewMatItaT><index:63>\r
+<char:partialdiff><font:LucidNewMatItaT><index:64>\r
+<char:flat><font:LucidNewMatItaT><index:91>\r
+<char:natural><font:LucidNewMatItaT><index:92>\r
+<char:sharp><font:LucidNewMatItaT><index:93>\r
+<char:slurbelow><font:LucidNewMatItaT><index:94>\r
+<char:slurabove><font:LucidNewMatItaT><index:95>\r
+<char:lscript><font:LucidNewMatItaT><index:96>\r
+<char:dotlessi><font:LucidNewMatItaT><index:123>\r
+<char:dotlessj><font:LucidNewMatItaT><index:124>\r
+<char:weierstrass><font:LucidNewMatItaT><index:125>\r
+<char:vector><font:LucidNewMatItaT><index:126>\r
+\r
+\r
+# mathematical characters for Lucida New Math Symbol font\r
+\r
+<char:minus><font:LucidNewMatSymT><index:161>\r
+<char:periodcentered><font:LucidNewMatSymT><index:162>\r
+<char:multiply><font:LucidNewMatSymT><index:163>\r
+<char:asteriskmath><font:LucidNewMatSymT><index:164>\r
+<char:divide><font:LucidNewMatSymT><index:165>\r
+<char:diamondmath><font:LucidNewMatSymT><index:166>\r
+<char:plusminus><font:LucidNewMatSymT><index:167>\r
+<char:minusplus><font:LucidNewMatSymT><index:168>\r
+<char:circleplus><font:LucidNewMatSymT><index:169>\r
+<char:circleminus><font:LucidNewMatSymT><index:170>\r
+<char:circlemultiply><font:LucidNewMatSymT><index:173>\r
+<char:circledivide><font:LucidNewMatSymT><index:174>\r
+<char:circledot><font:LucidNewMatSymT><index:175>\r
+<char:circlecopyrt><font:LucidNewMatSymT><index:176>\r
+<char:openbullet><font:LucidNewMatSymT><index:177>\r
+<char:bullet><font:LucidNewMatSymT><index:178>\r
+<char:equivasymptotic><font:LucidNewMatSymT><index:179>\r
+<char:equivalence><font:LucidNewMatSymT><index:180>\r
+<char:reflexsubset><font:LucidNewMatSymT><index:181>\r
+<char:reflexsuperset><font:LucidNewMatSymT><index:182>\r
+<char:lessequal><font:LucidNewMatSymT><index:183>\r
+<char:greaterequal><font:LucidNewMatSymT><index:184>\r
+<char:precedesequal><font:LucidNewMatSymT><index:185>\r
+<char:followsequal><font:LucidNewMatSymT><index:186>\r
+<char:similar><font:LucidNewMatSymT><index:187>\r
+<char:approxequal><font:LucidNewMatSymT><index:188>\r
+<char:propersubset><font:LucidNewMatSymT><index:189>\r
+<char:propersuperset><font:LucidNewMatSymT><index:190>\r
+<char:lessmuch><font:LucidNewMatSymT><index:191>\r
+<char:greatermuch><font:LucidNewMatSymT><index:192>\r
+<char:precedes><font:LucidNewMatSymT><index:193>\r
+<char:follows><font:LucidNewMatSymT><index:194>\r
+<char:arrowleft><font:LucidNewMatSymT><index:195>\r
+<char:spade><font:LucidNewMatSymT><index:196>\r
+<char:arrowright><font:LucidNewMatSymT><index:33>\r
+<char:arrowup><font:LucidNewMatSymT><index:34>\r
+<char:arrowdown><font:LucidNewMatSymT><index:35>\r
+<char:arrowboth><font:LucidNewMatSymT><index:36>\r
+<char:arrownortheast><font:LucidNewMatSymT><index:37>\r
+<char:arrowsoutheast><font:LucidNewMatSymT><index:38>\r
+<char:similarequal><font:LucidNewMatSymT><index:39>\r
+<char:arrowdblleft><font:LucidNewMatSymT><index:40>\r
+<char:arrowdblright><font:LucidNewMatSymT><index:41>\r
+<char:arrowdblup><font:LucidNewMatSymT><index:42>\r
+<char:arrowdbldown><font:LucidNewMatSymT><index:43>\r
+<char:arrowdblboth><font:LucidNewMatSymT><index:44>\r
+<char:arrownorthwest><font:LucidNewMatSymT><index:45>\r
+<char:arrowsouthwest><font:LucidNewMatSymT><index:46>\r
+<char:proportional><font:LucidNewMatSymT><index:47>\r
+<char:prime><font:LucidNewMatSymT><index:48>\r
+<char:infinity><font:LucidNewMatSymT><index:49>\r
+<char:element><font:LucidNewMatSymT><index:50>\r
+<char:owner><font:LucidNewMatSymT><index:51>\r
+<char:triangle><font:LucidNewMatSymT><index:52>\r
+<char:triangleinv><font:LucidNewMatSymT><index:53>\r
+<char:negationslash><font:LucidNewMatSymT><index:54>\r
+<char:mapsto><font:LucidNewMatSymT><index:55>\r
+<char:universal><font:LucidNewMatSymT><index:56>\r
+<char:existential><font:LucidNewMatSymT><index:57>\r
+<char:logicalnot><font:LucidNewMatSymT><index:58>\r
+<char:emptyset><font:LucidNewMatSymT><index:59>\r
+<char:Rfractur><font:LucidNewMatSymT><index:60>\r
+<char:Ifractur><font:LucidNewMatSymT><index:61>\r
+<char:latticetop><font:LucidNewMatSymT><index:62>\r
+<char:perpendicular><font:LucidNewMatSymT><index:63>\r
+<char:aleph><font:LucidNewMatSymT><index:64>\r
+<char:scriptA><font:LucidNewMatSymT><index:65>\r
+<char:scriptB><font:LucidNewMatSymT><index:66>\r
+<char:scriptC><font:LucidNewMatSymT><index:67>\r
+<char:scriptD><font:LucidNewMatSymT><index:68>\r
+<char:scriptE><font:LucidNewMatSymT><index:69>\r
+<char:scriptF><font:LucidNewMatSymT><index:70>\r
+<char:scriptG><font:LucidNewMatSymT><index:71>\r
+<char:scriptH><font:LucidNewMatSymT><index:72>\r
+<char:scriptI><font:LucidNewMatSymT><index:73>\r
+<char:scriptJ><font:LucidNewMatSymT><index:74>\r
+<char:scriptK><font:LucidNewMatSymT><index:75>\r
+<char:scriptL><font:LucidNewMatSymT><index:76>\r
+<char:scriptM><font:LucidNewMatSymT><index:77>\r
+<char:scriptN><font:LucidNewMatSymT><index:78>\r
+<char:scriptO><font:LucidNewMatSymT><index:79>\r
+<char:scriptP><font:LucidNewMatSymT><index:80>\r
+<char:scriptQ><font:LucidNewMatSymT><index:81>\r
+<char:scriptR><font:LucidNewMatSymT><index:82>\r
+<char:scriptS><font:LucidNewMatSymT><index:83>\r
+<char:scriptT><font:LucidNewMatSymT><index:84>\r
+<char:scriptU><font:LucidNewMatSymT><index:85>\r
+<char:scriptV><font:LucidNewMatSymT><index:86>\r
+<char:scriptW><font:LucidNewMatSymT><index:87>\r
+<char:scriptX><font:LucidNewMatSymT><index:88>\r
+<char:scriptY><font:LucidNewMatSymT><index:89>\r
+<char:scriptZ><font:LucidNewMatSymT><index:90>\r
+<char:union><font:LucidNewMatSymT><index:91>\r
+<char:intersection><font:LucidNewMatSymT><index:92>\r
+<char:unionmulti><font:LucidNewMatSymT><index:93>\r
+<char:logicaland><font:LucidNewMatSymT><index:94>\r
+<char:logicalor><font:LucidNewMatSymT><index:95>\r
+<char:turnstileleft><font:LucidNewMatSymT><index:96>\r
+<char:turnstileright><font:LucidNewMatSymT><index:97>\r
+<char:floorleft><font:LucidNewMatSymT><index:98>\r
+<char:floorright><font:LucidNewMatSymT><index:99>\r
+<char:ceilingleft><font:LucidNewMatSymT><index:100>\r
+<char:ceilingright><font:LucidNewMatSymT><index:101>\r
+<char:braceleft><font:LucidNewMatSymT><index:102>\r
+<char:braceright><font:LucidNewMatSymT><index:103>\r
+<char:angbracketleft><font:LucidNewMatSymT><index:104>\r
+<char:angbracketright><font:LucidNewMatSymT><index:105>\r
+<char:bar><font:LucidNewMatSymT><index:106>\r
+<char:bardbl><font:LucidNewMatSymT><index:107>\r
+<char:arrowbothv><font:LucidNewMatSymT><index:108>\r
+<char:arrowdblbothv><font:LucidNewMatSymT><index:109>\r
+<char:backslash><font:LucidNewMatSymT><index:110>\r
+<char:wreathproduct><font:LucidNewMatSymT><index:111>\r
+<char:radical><font:LucidNewMatSymT><index:112>\r
+<char:coproduct><font:LucidNewMatSymT><index:113>\r
+<char:nabla><font:LucidNewMatSymT><index:114>\r
+<char:integral><font:LucidNewMatSymT><index:115>\r
+<char:unionsq><font:LucidNewMatSymT><index:116>\r
+<char:intersectionsq><font:LucidNewMatSymT><index:117>\r
+<char:subsetsqequal><font:LucidNewMatSymT><index:118>\r
+<char:supersetsqequal><font:LucidNewMatSymT><index:119>\r
+<char:section><font:LucidNewMatSymT><index:120>\r
+<char:dagger><font:LucidNewMatSymT><index:121>\r
+<char:daggerdbl><font:LucidNewMatSymT><index:122>\r
+<char:paragraph><font:LucidNewMatSymT><index:123>\r
+<char:club><font:LucidNewMatSymT><index:124>\r
+<char:diamond><font:LucidNewMatSymT><index:125>\r
+<char:heart><font:LucidNewMatSymT><index:126>\r
+\r
+\r
+\r
+# character map for Symbol font\r
+\r
+<char:Symbol><font:Symbol><index:for>\r
+<char:space><font:Symbol><index:32>\r
+<char:exclam><font:Symbol><index:33>\r
+<char:universal><font:Symbol><index:34>\r
+<char:numbersign><font:Symbol><index:35>\r
+<char:existential><font:Symbol><index:36>\r
+<char:percent><font:Symbol><index:37>\r
+<char:ampersand><font:Symbol><index:38>\r
+<char:suchthat><font:Symbol><index:39>\r
+<char:parenleft><font:Symbol><index:40>\r
+<char:parenright><font:Symbol><index:41>\r
+<char:asteriskmath><font:Symbol><index:42>\r
+<char:plus><font:Symbol><index:43>\r
+<char:comma><font:Symbol><index:44>\r
+<char:minus><font:Symbol><index:45>\r
+<char:period><font:Symbol><index:46>\r
+<char:slash><font:Symbol><index:47>\r
+<char:zero><font:Symbol><index:48>\r
+<char:one><font:Symbol><index:49>\r
+<char:two><font:Symbol><index:50>\r
+<char:three><font:Symbol><index:51>\r
+<char:four><font:Symbol><index:52>\r
+<char:five><font:Symbol><index:53>\r
+<char:six><font:Symbol><index:54>\r
+<char:seven><font:Symbol><index:55>\r
+<char:eight><font:Symbol><index:56>\r
+<char:nine><font:Symbol><index:57>\r
+<char:colon><font:Symbol><index:58>\r
+<char:semicolon><font:Symbol><index:59>\r
+<char:less><font:Symbol><index:60>\r
+<char:equal><font:Symbol><index:61>\r
+<char:greater><font:Symbol><index:62>\r
+<char:question><font:Symbol><index:63>\r
+<char:congruent><font:Symbol><index:64>\r
+<char:Alpha><font:Symbol><index:65>\r
+<char:Beta><font:Symbol><index:66>\r
+<char:Chi><font:Symbol><index:67>\r
+<char:Delta><font:Symbol><index:68>\r
+<char:Epsilon><font:Symbol><index:69>\r
+<char:Phi><font:Symbol><index:70>\r
+<char:Gamma><font:Symbol><index:71>\r
+<char:Eta><font:Symbol><index:72>\r
+<char:Iota><font:Symbol><index:73>\r
+<char:theta1><font:Symbol><index:74>\r
+<char:Kappa><font:Symbol><index:75>\r
+<char:Lambda><font:Symbol><index:76>\r
+<char:Mu><font:Symbol><index:77>\r
+<char:Nu><font:Symbol><index:78>\r
+<char:Omicron><font:Symbol><index:79>\r
+<char:Pi><font:Symbol><index:80>\r
+<char:Theta><font:Symbol><index:81>\r
+<char:Rho><font:Symbol><index:82>\r
+<char:Sigma><font:Symbol><index:83>\r
+<char:Tau><font:Symbol><index:84>\r
+<char:Upsilon><font:Symbol><index:85>\r
+<char:sigma1><font:Symbol><index:86>\r
+<char:Omega><font:Symbol><index:87>\r
+<char:Xi><font:Symbol><index:88>\r
+<char:Psi><font:Symbol><index:89>\r
+<char:Zeta><font:Symbol><index:90>\r
+<char:bracketleft><font:Symbol><index:91>\r
+<char:therefore><font:Symbol><index:92>\r
+<char:bracketright><font:Symbol><index:93>\r
+<char:perpendicular><font:Symbol><index:94>\r
+<char:underscore><font:Symbol><index:95>\r
+<char:radicalex><font:Symbol><index:96>\r
+<char:alpha><font:Symbol><index:97>\r
+<char:beta><font:Symbol><index:98>\r
+<char:chi><font:Symbol><index:99>\r
+<char:delta><font:Symbol><index:100>\r
+<char:epsilon><font:Symbol><index:101>\r
+<char:phi><font:Symbol><index:102>\r
+<char:gamma><font:Symbol><index:103>\r
+<char:eta><font:Symbol><index:104>\r
+<char:iota><font:Symbol><index:105>\r
+<char:phi1><font:Symbol><index:106>\r
+<char:kappa><font:Symbol><index:107>\r
+<char:lambda><font:Symbol><index:108>\r
+<char:mu><font:Symbol><index:109>\r
+<char:nu><font:Symbol><index:110>\r
+<char:omicron><font:Symbol><index:111>\r
+<char:pi><font:Symbol><index:112>\r
+<char:theta><font:Symbol><index:113>\r
+<char:rho><font:Symbol><index:114>\r
+<char:sigma><font:Symbol><index:115>\r
+<char:tau><font:Symbol><index:116>\r
+<char:upsilon><font:Symbol><index:117>\r
+<char:omega1><font:Symbol><index:118>\r
+<char:omega><font:Symbol><index:119>\r
+<char:xi><font:Symbol><index:120>\r
+<char:psi><font:Symbol><index:121>\r
+<char:zeta><font:Symbol><index:122>\r
+<char:braceleft><font:Symbol><index:123>\r
+<char:bar><font:Symbol><index:124>\r
+<char:braceright><font:Symbol><index:125>\r
+<char:similar><font:Symbol><index:126>\r
+<char:Euro><font:Symbol><index:160>\r
+<char:Upsilon1><font:Symbol><index:161>\r
+<char:minute><font:Symbol><index:162>\r
+<char:lessequal><font:Symbol><index:163>\r
+<char:fraction><font:Symbol><index:164>\r
+<char:infinity><font:Symbol><index:165>\r
+<char:florin><font:Symbol><index:166>\r
+<char:club><font:Symbol><index:167>\r
+<char:diamond><font:Symbol><index:168>\r
+<char:heart><font:Symbol><index:169>\r
+<char:spade><font:Symbol><index:170>\r
+<char:arrowboth><font:Symbol><index:171>\r
+<char:arrowleft><font:Symbol><index:172>\r
+<char:arrowup><font:Symbol><index:173>\r
+<char:arrowright><font:Symbol><index:174>\r
+<char:arrowdown><font:Symbol><index:175>\r
+<char:degree><font:Symbol><index:176>\r
+<char:plusminus><font:Symbol><index:177>\r
+<char:second><font:Symbol><index:178>\r
+<char:greaterequal><font:Symbol><index:179>\r
+<char:multiply><font:Symbol><index:180>\r
+<char:proportional><font:Symbol><index:181>\r
+<char:partialdiff><font:Symbol><index:182>\r
+<char:bullet><font:Symbol><index:183>\r
+<char:divide><font:Symbol><index:184>\r
+<char:notequal><font:Symbol><index:185>\r
+<char:equivalence><font:Symbol><index:186>\r
+<char:approxequal><font:Symbol><index:187>\r
+\r
+# seems to be a quarter fraction\r
+# <char:ellipsis><font:Symbol><index:188>\r
+\r
+<char:arrowvertex><font:Symbol><index:189>\r
+<char:arrowhorizex><font:Symbol><index:190>\r
+<char:carriagereturn><font:Symbol><index:191>\r
+<char:aleph><font:Symbol><index:192>\r
+<char:Ifraktur><font:Symbol><index:193>\r
+<char:Rfraktur><font:Symbol><index:194>\r
+<char:weierstrass><font:Symbol><index:195>\r
+<char:circlemultiply><font:Symbol><index:196>\r
+<char:circleplus><font:Symbol><index:197>\r
+<char:emptyset><font:Symbol><index:198>\r
+<char:intersection><font:Symbol><index:199>\r
+<char:union><font:Symbol><index:200>\r
+<char:propersuperset><font:Symbol><index:201>\r
+<char:reflexsuperset><font:Symbol><index:202>\r
+<char:notsubset><font:Symbol><index:203>\r
+<char:propersubset><font:Symbol><index:204>\r
+<char:reflexsubset><font:Symbol><index:205>\r
+<char:element><font:Symbol><index:206>\r
+<char:notelement><font:Symbol><index:207>\r
+<char:angle><font:Symbol><index:208>\r
+<char:gradient><font:Symbol><index:209>\r
+<char:registerserif><font:Symbol><index:210>\r
+<char:copyrightserif><font:Symbol><index:211>\r
+<char:trademarkserif><font:Symbol><index:212>\r
+<char:product><font:Symbol><index:213>\r
+<char:radical><font:Symbol><index:214>\r
+<char:dotmath><font:Symbol><index:215>\r
+<char:logicalnot><font:Symbol><index:216>\r
+<char:logicaland><font:Symbol><index:217>\r
+<char:logicalor><font:Symbol><index:218>\r
+<char:arrowdblboth><font:Symbol><index:219>\r
+<char:arrowdblleft><font:Symbol><index:220>\r
+<char:arrowdblup><font:Symbol><index:221>\r
+<char:arrowdblright><font:Symbol><index:222>\r
+<char:arrowdbldown><font:Symbol><index:223>\r
+<char:lozenge><font:Symbol><index:224>\r
+<char:angleleft><font:Symbol><index:225>\r
+<char:registersans><font:Symbol><index:226>\r
+<char:copyrightsans><font:Symbol><index:227>\r
+<char:trademarksans><font:Symbol><index:228>\r
+<char:summation><font:Symbol><index:229>\r
+<char:parenlefttp><font:Symbol><index:230>\r
+<char:parenleftex><font:Symbol><index:231>\r
+<char:parenleftbt><font:Symbol><index:232>\r
+<char:bracketlefttp><font:Symbol><index:233>\r
+<char:bracketleftex><font:Symbol><index:234>\r
+<char:bracketleftbt><font:Symbol><index:235>\r
+<char:bracelefttp><font:Symbol><index:236>\r
+<char:braceleftmid><font:Symbol><index:237>\r
+<char:braceleftbt><font:Symbol><index:238>\r
+<char:braceex><font:Symbol><index:239>\r
+<char:angleright><font:Symbol><index:241>\r
+<char:integral><font:Symbol><index:242>\r
+<char:integraltp><font:Symbol><index:243>\r
+<char:integralex><font:Symbol><index:244>\r
+<char:integralbt><font:Symbol><index:245>\r
+<char:parenrighttp><font:Symbol><index:246>\r
+<char:parenrightex><font:Symbol><index:247>\r
+<char:parenrightbt><font:Symbol><index:248>\r
+<char:bracketrighttp><font:Symbol><index:249>\r
+<char:bracketrightex><font:Symbol><index:250>\r
+<char:bracketrightbt><font:Symbol><index:251>\r
+<char:bracerighttp><font:Symbol><index:252>\r
+<char:bracerightmid><font:Symbol><index:253>\r
+<char:bracerightbt><font:Symbol><index:254>\r
+\r
+\r
+# character map for Lucida New Math Extended font\r
+\r
+<char:parenleftbig><font:LucidNewMatExtT><index:161>\r
+<char:parenrightbig><font:LucidNewMatExtT><index:162>\r
+<char:bracketleftbig><font:LucidNewMatExtT><index:163>\r
+<char:bracketrightbig><font:LucidNewMatExtT><index:164>\r
+<char:floorleftbig><font:LucidNewMatExtT><index:165>\r
+<char:floorrightbig><font:LucidNewMatExtT><index:166>\r
+<char:ceilingleftbig><font:LucidNewMatExtT><index:167>\r
+<char:ceilingrightbig><font:LucidNewMatExtT><index:168>\r
+<char:braceleftbig><font:LucidNewMatExtT><index:169>\r
+<char:bracerightbig><font:LucidNewMatExtT><index:170>\r
+<char:angbracketleftbig><font:LucidNewMatExtT><index:173>\r
+<char:angbracketrightbig><font:LucidNewMatExtT><index:174>\r
+<char:vextendsingle><font:LucidNewMatExtT><index:175>\r
+<char:vextenddouble><font:LucidNewMatExtT><index:176>\r
+<char:slashbig><font:LucidNewMatExtT><index:177>\r
+<char:backslashbig><font:LucidNewMatExtT><index:178>\r
+<char:parenleftBig><font:LucidNewMatExtT><index:179>\r
+<char:parenrightBig><font:LucidNewMatExtT><index:180>\r
+<char:parenleftbigg><font:LucidNewMatExtT><index:181>\r
+<char:parenrightbigg><font:LucidNewMatExtT><index:182>\r
+<char:bracketleftbigg><font:LucidNewMatExtT><index:183>\r
+<char:bracketrightbigg><font:LucidNewMatExtT><index:184>\r
+<char:floorleftbigg><font:LucidNewMatExtT><index:185>\r
+<char:floorrightbigg><font:LucidNewMatExtT><index:186>\r
+<char:ceilingleftbigg><font:LucidNewMatExtT><index:187>\r
+<char:ceilingrightbigg><font:LucidNewMatExtT><index:188>\r
+<char:braceleftbigg><font:LucidNewMatExtT><index:189>\r
+<char:bracerightbigg><font:LucidNewMatExtT><index:190>\r
+<char:angbracketleftbigg><font:LucidNewMatExtT><index:28>\r
+<char:angbracketrightbigg><font:LucidNewMatExtT><index:29>\r
+<char:slashbigg><font:LucidNewMatExtT><index:193>\r
+<char:backslashbigg><font:LucidNewMatExtT><index:194>\r
+<char:parenleftBigg><font:LucidNewMatExtT><index:195>\r
+<char:parenrightBigg><font:LucidNewMatExtT><index:33>\r
+<char:bracketleftBigg><font:LucidNewMatExtT><index:34>\r
+<char:bracketrightBigg><font:LucidNewMatExtT><index:35>\r
+<char:floorleftBigg><font:LucidNewMatExtT><index:36>\r
+<char:floorrightBigg><font:LucidNewMatExtT><index:37>\r
+<char:ceilingleftBigg><font:LucidNewMatExtT><index:38>\r
+<char:ceilingrightBigg><font:LucidNewMatExtT><index:39>\r
+<char:braceleftBigg><font:LucidNewMatExtT><index:40>\r
+<char:bracerightBigg><font:LucidNewMatExtT><index:41>\r
+<char:angbracketleftBigg><font:LucidNewMatExtT><index:42>\r
+<char:angbracketrightBigg><font:LucidNewMatExtT><index:43>\r
+<char:slashBigg><font:LucidNewMatExtT><index:44>\r
+<char:backslashBigg><font:LucidNewMatExtT><index:45>\r
+<char:slashBig><font:LucidNewMatExtT><index:46>\r
+<char:backslashBig><font:LucidNewMatExtT><index:47>\r
+<char:parenlefttp><font:LucidNewMatExtT><index:48>\r
+<char:parenrighttp><font:LucidNewMatExtT><index:49>\r
+<char:bracketlefttp><font:LucidNewMatExtT><index:50>\r
+<char:bracketrighttp><font:LucidNewMatExtT><index:51>\r
+<char:bracketleftbt><font:LucidNewMatExtT><index:52>\r
+<char:bracketrightbt><font:LucidNewMatExtT><index:53>\r
+<char:bracketleftex><font:LucidNewMatExtT><index:54>\r
+<char:bracketrightex><font:LucidNewMatExtT><index:55>\r
+<char:bracelefttp><font:LucidNewMatExtT><index:56>\r
+<char:bracerighttp><font:LucidNewMatExtT><index:57>\r
+<char:braceleftbt><font:LucidNewMatExtT><index:58>\r
+<char:bracerightbt><font:LucidNewMatExtT><index:59>\r
+<char:braceleftmid><font:LucidNewMatExtT><index:60>\r
+<char:bracerightmid><font:LucidNewMatExtT><index:61>\r
+<char:braceex><font:LucidNewMatExtT><index:62>\r
+<char:arrowvertex><font:LucidNewMatExtT><index:63>\r
+<char:parenleftbt><font:LucidNewMatExtT><index:64>\r
+<char:parenrightbt><font:LucidNewMatExtT><index:65>\r
+<char:parenleftex><font:LucidNewMatExtT><index:66>\r
+<char:parenrightex><font:LucidNewMatExtT><index:67>\r
+<char:angbracketleftBig><font:LucidNewMatExtT><index:68>\r
+<char:angbracketrightBig><font:LucidNewMatExtT><index:69>\r
+<char:unionsqtext><font:LucidNewMatExtT><index:70>\r
+<char:unionsqdisplay><font:LucidNewMatExtT><index:71>\r
+<char:contintegraltext><font:LucidNewMatExtT><index:72>\r
+<char:contintegraldisplay><font:LucidNewMatExtT><index:73>\r
+<char:circledottext><font:LucidNewMatExtT><index:74>\r
+<char:circledotdisplay><font:LucidNewMatExtT><index:75>\r
+<char:circleplustext><font:LucidNewMatExtT><index:76>\r
+<char:circleplusdisplay><font:LucidNewMatExtT><index:77>\r
+<char:circlemultiplytext><font:LucidNewMatExtT><index:78>\r
+<char:circlemultiplydisplay><font:LucidNewMatExtT><index:79>\r
+<char:summationtext><font:LucidNewMatExtT><index:80>\r
+<char:producttext><font:LucidNewMatExtT><index:81>\r
+<char:integraltext><font:LucidNewMatExtT><index:82>\r
+<char:uniontext><font:LucidNewMatExtT><index:83>\r
+<char:intersectiontext><font:LucidNewMatExtT><index:84>\r
+<char:unionmultitext><font:LucidNewMatExtT><index:85>\r
+<char:logicalandtext><font:LucidNewMatExtT><index:86>\r
+<char:logicalortext><font:LucidNewMatExtT><index:87>\r
+<char:summationdisplay><font:LucidNewMatExtT><index:88>\r
+<char:productdisplay><font:LucidNewMatExtT><index:89>\r
+<char:integraldisplay><font:LucidNewMatExtT><index:90>\r
+<char:uniondisplay><font:LucidNewMatExtT><index:91>\r
+<char:intersectiondisplay><font:LucidNewMatExtT><index:92>\r
+<char:unionmultidisplay><font:LucidNewMatExtT><index:93>\r
+<char:logicalanddisplay><font:LucidNewMatExtT><index:94>\r
+<char:logicalordisplay><font:LucidNewMatExtT><index:95>\r
+<char:coproducttext><font:LucidNewMatExtT><index:96>\r
+<char:coproductdisplay><font:LucidNewMatExtT><index:97>\r
+<char:hatwide><font:LucidNewMatExtT><index:98>\r
+<char:hatwider><font:LucidNewMatExtT><index:99>\r
+<char:hatwidest><font:LucidNewMatExtT><index:100>\r
+<char:tildewide><font:LucidNewMatExtT><index:101>\r
+<char:tildewider><font:LucidNewMatExtT><index:102>\r
+<char:tildewidest><font:LucidNewMatExtT><index:103>\r
+<char:bracketleftBig><font:LucidNewMatExtT><index:104>\r
+<char:bracketrightBig><font:LucidNewMatExtT><index:105>\r
+<char:floorleftBig><font:LucidNewMatExtT><index:106>\r
+<char:floorrightBig><font:LucidNewMatExtT><index:107>\r
+<char:ceilingleftBig><font:LucidNewMatExtT><index:108>\r
+<char:ceilingrightBig><font:LucidNewMatExtT><index:109>\r
+<char:braceleftBig><font:LucidNewMatExtT><index:110>\r
+<char:bracerightBig><font:LucidNewMatExtT><index:111>\r
+<char:radicalbig><font:LucidNewMatExtT><index:112>\r
+<char:radicalBig><font:LucidNewMatExtT><index:113>\r
+<char:radicalbigg><font:LucidNewMatExtT><index:114>\r
+<char:radicalBigg><font:LucidNewMatExtT><index:115>\r
+<char:radicalbt><font:LucidNewMatExtT><index:116>\r
+<char:radicalvertex><font:LucidNewMatExtT><index:117>\r
+<char:radicaltp><font:LucidNewMatExtT><index:118>\r
+<char:arrowvertexdbl><font:LucidNewMatExtT><index:119>\r
+<char:arrowtp><font:LucidNewMatExtT><index:120>\r
+<char:arrowbt><font:LucidNewMatExtT><index:121>\r
+<char:bracehtipdownleft><font:LucidNewMatExtT><index:122>\r
+<char:bracehtipdownright><font:LucidNewMatExtT><index:123>\r
+<char:bracehtipupleft><font:LucidNewMatExtT><index:124>\r
+<char:bracehtipupright><font:LucidNewMatExtT><index:125>\r
+<char:arrowdbltp><font:LucidNewMatExtT><index:126>\r
+<char:arrowdblbt><font:LucidNewMatExtT><index:196>\r
--- /dev/null
+\preamble\r\loadchars{charmap.txt}\r\loadchars{standard-charmap.txt}\r\loadchars{lucmathsym-charmap.txt}\r\loadchars{lucmathit-charmap.txt}\r\loadchars{lucmathext-charmap.txt}\r\loadchars{symbol-charmap.txt}\r\loadstyles{styles.txt}\r\r\title A Micromodularity Mechanism\r\r\section Testing\r\rThis is gamma: \gamma.\\\rThis is Delta: \Delta.\\\rThis is oplus: \oplus.\r\scriptA \arrowdblright \scriptA\r\rThis is a subscripted variable: A\sub<\bold<hello>\italics<there>>.\rMath mode: $x + 2 = y, and && x\sub<2> = y\sub<3> = x\sub<ijk>$\r\r\author Daniel Jackson, Ilya Shlyakhter and Manu Sridharan\\\rLaboratory for Computer Science\\\rMassachusetts Institute of Technology\\\rCambridge, Massachusetts, USA\\\rdnj@mit.edu\r\r\opening Abstract\r\rA simple mechanism for structuring specifications is described. By modelling structures as atoms, it remains entirely first-order and thus amenable to automatic analysis. And by interpreting fields of structures as relations, it allows the same relational operators used in the formula language to be used for dereferencing. An extension feature allows structures to be developed incrementally, but requires no textual inclusion nor any notion of subtyping. The paper demonstrates the flexibility of the mechanism by application in a variety of common idioms.\r\r\subsection* Categories and Subject Descriptors\r\rD.2.1 Requirements/Specifications---Languages; D.2.4 Software/Program Verification---Formal methods, Model checking; F.3.1 Specifying and Verifying and Reasoning about Programs---Assertions, Invariants, Specification techniques.\r\r\subsection* General Terms\r\rDesign; Documentation; Languages; Verification.\r\r\subsection* Keywords\r\rModeling languages; formal specification; first-order logic; relational calculus; Alloy language; Z specification language; schema calculus.\r\r\section* Introduction\r\r\quote I am neither crazy nor a micromaniac.\\\r(A micromaniac is someone obsessed with\\\rreducing things to their smallest possible form.\\\rThis word, by the way, is not in the dictionary.)\\\r--_Edouard de Pomiane, French Cooking in Ten Minutes, 1930_\r\r\noindent Most specification languages provide mechanisms that allow larger specifications to be built from smaller ones. These mechanisms are often the most complicated part of the language, and present obstacles to analysis. This paper presents a simple mechanism that seems to be expressive enough for a wide variety of uses, without compromising analyzability.\r\rThis work is part of a larger project investigating the design of a "micro modelling language". Our premise is that lightweight application of formal methods [6] demands an unusually small and simple language that is amenable to fully automatic semantic analysis. The Alloy language is the result to date of our efforts to design such a language. Based on our experiences with the language [4] and its analyzer [5], we have recently developed a revision of Alloy that overcomes many of its limitations. This paper describes the key feature of the revised language: the _signature_, a new modularity mechanism.\r\rThe mechanism allows our existing analysis scheme [3] to be applied to specifications involving structures. This is not achieved by treating the structuring mechanism as a syntactic sugar, which would limit the power of the notation (ruling out, for example, quantification over structures) and would complicate the analysis tool and make output harder for users to interpret. Because of the mechanism's generality, it has also enabled us to simplify the language as a whole, making it more uniform and eliminating some ad hoc elements.\r\rOur mechanism has a variety of applications. It can express inherent structure in the system being modelled, and can be used to organize a specification in which details are added incrementally. It can be used to construct a library of datatypes, or to describe a system as an instantiation of a more general system. And it can express state invariants, transitions, and sequences, despite the lack of any special syntax for state machines.\r\rIn this last respect, the new language differs most markedly from its predecessor [4], which provided built-in notions of state invariants and operations. We now think this was a bad idea, because it made the language cumbersome for problems (such as the analysis of security policies or architectural topology constraints) in which temporal behaviour can be fruitfully ignored, and too inflexible for many problems in which temporal behaviour is important.\r\r#Because the notation as a whole is small, simple and analyzable, and free of bias towards any particular domain of application, it may be suitable as an intermediate language. A tool for architectural design, for example, might translate a more domain-specific notation into our language, allowing analyses that such tools do not currently support (such as automatic generation of sample configurations from style rules, and checking of consistency).\r#\rOur paper begins by explaining our motivations---the requirements our mechanism is designed to meet. The mechanism is then presented first informally in a series of examples, and then slightly more rigorously feature-by-feature. We discuss related work, especially the schema calculus of Z, and close with a summary of the merits and deficiences of our notation as a whole.\r\r\section Requirements\r\rThe goal of this work was to find a single structuring mechanism that would support a variety of common specification idioms:\r\r\point \cdot _States_: description of complex state as a collection of named components; incremental description both by hierarchy, in which a complex state becomes a component of a larger state, and by extension, in which new components are added; declaration of invariants and definitions of derived components;\r\r\point \cdot _Datatypes_: separate description of a library of polymorphic datatypes, such as lists, sequences, trees and orders, along with their operators;\r\r\point \cdot _Transitions_: specification of state transitions as operations described implicitly as formulas relating pre- and post-state; composition of operations from previously defined invariants and operations; sequential composition of operations; description of traces as sequences of states;\r\r\point \cdot _Abstractions_: description of abstraction relations between state spaces;\r\r\point \cdot _Assertions_: expression of properties intended to be redundant, to be checked by analysis, including: relationships amongst invariants; wellformedness of definitions (eg, that an implicit definition is functional); establishment and preservation of invariants by operations; properties of states reachable along finite traces; and simulation relationships between abstract and concrete versions of an operation.\r\r\noindent We wanted additionally to meet some more general criteria:\r\r\point \cdot _Simplicity_. The language as a whole should be exceptionally small and simple.\r\r\point \cdot _Flexibility_. Support for the particular idioms of state-machine specification should not be a straitjacket; the language should not dictate how state machines are expressed, and should not make it hard to describe structures that are not state machines (such as security models and architectural styles).\r\r\point \cdot _Analyzability_. A fully automatic semantic analysis should be possible. In the present work, this has been achieved by requiring that the modularity mechanism be first order, and expressible in the kernel of the existing language.\r\r\noindent Finally, our language design decisions have been influenced by some principles that we believe contribute to these goals, make the language easier to use, and analysis tools easier to build:\r\r\point \cdot _Explicitness_. The language should be fully explicit, with as few implicit constraints, coercions, etc, as possible.\r\r\point \cdot _Minimal mathematics_. The basic theory of sets and relations should suffice; it should not be necessary to introduce domains, fixed points, infinities or special logical values.\r\r\point \cdot _Minimal syntax_. There should be very few keywords or special symbols, and no need for special typography or layout.\r\r\point \cdot _Uniformity_. A small and general set of constructs should be applied uniformly, independent of context.\r\r\point \cdot _Lack of novelty_. Whenever possible, notions and syntax should follow standard usage of conventional mathematics and programming.\r\r\section Informal Description\r\rAs a running example, we will specify a simple memory system involving a cache and a main memory. The memory has a fixed set of addresses and associates a data value with each address. The cache, in contrast, associates data values with some subset of addresses that varies over time. The cache is updated by a "write-back scheme", which means that updates need not be reflected to main memory immediately. The cache may therefore hold a more current value for an address than the main memory; the two are brought into alignment when the address is flushed from the cache and its value is written to main memory.\r\r\subsection States\r\rWe start by declaring the existence of addresses and data values:\r\r\geekmath sig Addr {}\\\rsig Data {}\r\rEach line declares a _signature_, and introduces a set of atoms: _Addr_ for the set of addresses, and _Data_ for the set of data values. Like 'given types' in Z, these sets are disjoint from one another, and their atoms are unstructured and uninterpreted. Signature names can be used as expressions denoting sets, but they are also treated as types, so the expression _Addr+Data_, for example, is ill-typed, since the union operator (+) requires the types of its operands to match.\r\rThe signature declaration\r\r\geekmath sig Memory {\\\r addrs: set Addr,\\\r map: addrs ->! Data\\\r }\r\rlikewise declares a set of atoms, _Memory_, corresponding to the set of all possible memories. In addition, it declares two fields: _addrs_ and _map_ which associate with a memory a set of addresses and a mapping from addresses to data values respectively. Thus, given a memory _m_, the expression _m.addrs_ will be a set of addresses, _m.map_ will be a relation from addresses to data values. The memory, addresses and data values should be viewed as distinct atoms in their own right; fields don't decompose an atom, but rather relate one atom to others. The exclamation mark in the declaration of the field _map_ is a 'multiplicity marking': it says that _m.map_ associates exactly one data value with each address in the set _m.addrs_. The use of _addrs_ rather than _Addr_ on the left side of the arrow indicates that _m.map_ does not associate a data value with an address that is not in the set _m.addrs_.\r\rIn these expressions, the dot is simply relational image. More precisely, when we say that _m_ is a memory, we mean that the expression _m_ denotes a set consisting of a single atom. The field _addrs_ is a relation from _Memory_ to _Addr_, and _m.addrs_ denotes the image of the singleton set under this relation. So for a set of memories _ms_, the expression _ms.addrs_ will denote the union of the sets of addresses that belong to the individual memories. Given an address _a_, the expression _a.(m.map)_ denotes the set of data values associated with address _a_ in memory _m_, which will either be empty (when the address is not mapped) or a singleton. For convenience, we allow the relational image _s.r_ to be written equivalently as _r_[_s_], where [] binds more loosely than dot, so this expression may be written as _m.map_[_a_] instead.\r\rLike objects of an object-oriented language, two distinct atoms can have fields of the same value. Unlike objects, however, atoms are immutable. Each field is fixed, and cannot map an atom to one value at one time and another value at another time. To describe an operation that changes the state of a memory, therefore, we will use two distinct atoms in the set _Memory_ to represent the memory's state before and after.\r\r\subsection Extension\r\rA signature declaration can introduce a set as a subset of one previously declared, in which case we call it a _subsignature_. In this case, the set does not correspond to a type, but rather its atoms take on the type of the superset. For example, the declaration\r\r\geekmath sig MainMemory extends Memory {}\r\rintroduces a set of atoms _MainMemory_ representing main memories, which is constrained to be a subset of the set _Memory_. Likewise\r\r\geekmath sig Cache extends Memory {\\\r dirty: set addrs\\\r }\r\rintroduces a set of atoms _Cache_ representing those memories that can be regarded as caches. It also introduces a field _dirty_ that associates with a cache the set of addresses that is dirty; later, we will use this to represent those addresses for which a cache and main memory differ. Because _Cache_ is a subset of _Memory_, and _m.addrs_ (for any memory _m_) is a subset of _Addr_, the field denotes a relation whose type is from _Memory_ to _Addr_. Expressions such as _m.dirty_ are therefore type-correct for a memory _m_, whether or not _m_ is a cache. But since declaration of the field _dirty_ within the signature _Cache_ constrains _dirty_ to be a relation that maps only caches, _m.dirty_ will always denote the empty set when _m_ is not a cache.\r\rThis approach avoids introducing a notion of subtyping. Subtypes complicate the language, and tend to make it more difficult to use. In OCL [17], which models extension with subtypes rather than subsets, an expression such as _m.dirty_ would be illegal, and would require a coercion of _m_ to the subtype _Cache_. Coercions do not fit smoothly into the relational framework; they interfere with the ability to take the image of a set under a relation, for example. Moreover, subtypes are generally disjoint, whereas our approach allows the sets denoted by subsignatures to overlap. In this case, we'll add a constraint (in Section 2.4 below) to ensure that _MainMemory_ and _Cache_ are in fact disjoint.\r\rDeclaring _Cache_ and _MainMemory_ as subsignatures of _Memory_ serves to factor out their common properties. Extension can be used for a different purpose, in which a single signature is developed by repeated extensions along a chain. In this case, the supersignatures may not correspond to entities in the domain being modelled, but are simply artifacts of specification---fragments developed along the way. Z specifications are typically developed in this style.\r\r\subsection Hierarchy\r\rThe signature declaration also supports hierarchical structuring. We can declare a signature for systems each consisting of a cache and a main memory:\r\r\geekmath sig System {\\\r cache: Cache,\\\r main: MainMemory\\\r }\r\rAgain, _System_ introduces a set of atoms, and each field represents a relation. The omission of the keyword _set_ indicates that a relation is a total function. So for a system _s_, the expression _s.cache_ denotes one cache---that is, a set consisting of a single cache. This is one of very few instances of implicit constraints in our language, which we introduced in order to make declaration syntax conventional.\r\rSince signatures denote sets of atoms, apparently circular references are allowed. Linked lists, for example, may be modelled like this, exactly as they might be implemented in a language like Java:\r\r\geekmath sig List {}\\\rsig NonEmptyList extends List {elt: Elt, rest: List}\r \rThere is no recursion here; the field _rest_ is simply a homogeneous relation of type _List_ to _List_, with its domain restricted to the subset _NonEmptyList_.\r\r\subsection State Properties\r\rProperties of signature atoms are recorded as logical formulas. To indicate that such a property always holds, we package it as a _fact_. To say that, for any memory system, the addresses in a cache are always addresses within the main memory, we might write:\r\r\geekmath fact {all s: System | s.cache.addrs in s.main.addrs}\r\ror, using a shorthand that allows facts about atoms of a signature to be appended to it:\r\r\geekmath sig System {cache: Cache, main: MainMemory}\\\r {cache.addrs in main.addrs}\r\rThe appended fact is implicitly prefixed by\r\r\geekmath all this: System | with this |\r\rin which the _with_ construct, explained in Sectiom 3.6 below, causes the fields implicitly to be dereferences of the atom _this_.\r\rA fact can constrain atoms of arbitrary signatures; to say that no main memory is a cache we might write:\r\r\geekmath fact {no (MainMemory & Cache)}\r\rwhere _no e_ means that the expression _e_ has no elements, and & is intersection.\r\r#Again, this is common enough that we provide a shorthand. Declaring a subsignature as _disjoint_ indicates that it shares no atoms with any other subsignatures of the same supersignature. So the fact can be replaced by changing our declaration of _MainMemory_ to:\r#\r#\geekmath disjoint sig MainMemory extends Memory {}\r#\rMost descriptions have more interesting facts. We can express the fact that linked lists are acyclic, for example:\r\r\geekmath fact {no p: List | p in p.\hat @sep rest}\r\rThe expression _\hat @sep rest_ denotes the transitive closure of the relation _rest_, so that _p.^rest_ denotes the set of lists reachable from _p_ by following the field _rest_ once or more. This illustrates a benefit of treating a field as a relation---that we can apply standard relational operators to it---and is also an example of an expression hard to write in a language that treats extension as subtyping (since each application of _rest_ would require its own coercion).\r\rOften we want to define a property without imposing it as a permanent constraint. In that case, we declare it as a _function_. Here, for example, is the invariant that the cache lines not marked as dirty are consistent with main memory:\r\r\geekmath fun DirtyInv (s: System) {\\\r all a !: s.cache.dirty | s.cache.map[a] = s.main.map[a]\\\r }\r \r(The exclamation mark negates an operator, so the quantification is over all addresses that are _not_ dirty.) Packaging this as a function that can be applied to a particular system, rather than as a fact for all systems, will allow us to express assertions about preservation of the invariant (Section 2.8).\r\rBy default, a function returns a boolean value---the value of the formula in its body. The value of _DirtyInv(s)_ for a system _s_ is therefore true or false. A function may return non-boolean values. We might, for example, define the set of bad addresses to be those for which the cache and main memory differ:\r\r\geekmath fun BadAddrs (s: System): set Addr {\\\r result = {a: Addr | s.cache.map[a] != s.main.map[a]}\\\r }\r\rand then write our invariant like this:\r\r\geekmath fun DirtyInv (s: System) {BadAddrs(s) in s.cache.dirty}\r\rIn this case, _BadAddrs(s)_ denotes a set of addresses, and is short for the expression on the right-hand side of the equality in the definition of the function _BadAddrs_. The use of the function application as an expression does not in fact depend on the function being defined explicitly. Had we written\r\r\geekmath fun BadAddrs (s: System): set Addr {\\\r all a: Addr | a in result iff s.cache.map[a] != s.main.map[a]\\\r }\r \rthe application would still be legal; details are explained in Section 3.7.\r# \r# \geekmath BadAddrs(s) in s.cache.dirty\r# \r# would be treated as short for \r# \r# \geekmath all result: set Addr |\\\r# (all a: Addr | a in result iff s.cache.map[a] != s.main.map[a])\\\r# => result in s.cache.dirty\r# \r# This desugaring is explained in more detail in Section 99 below.\r\r\subsection Operations\r\rFollowing Z, we can specify operations as formulas that constrain pre- and post-states. An operation may be packaged as a single function (or as two functions if we want to separate pre- and post-conditions in the style of VDM or Larch).\r\rThe action of writing a data value to an address in memory might be specified like this:\r\r\geekmath fun Write (m,m': Memory, d: Data, a: Addr) {\\\r m'.map = m.map ++ (a->d)\\\r }\r\rThe formula in the body of the function relates _m_, the value of the memory before, to _m'_, the value after. These identifers are just formal arguments, so the choice of names is not significant. Moreover, the prime mark plays no special role akin to decoration in Z---it's a character like any other. The operator ++ is relational override, and the arrow forms a cross product. As mentioned above, scalars are represented as singleton sets, so there is no distinction between a tuple and a relation. The arrows in the expressions _a->d_ here and _addrs->Data_ in the declaration of the _map_ field of _Memory_ are one and the same. \r\rThe action of reading a data value can likewise be specified as a function, although since it has no side-effect we omit the _m'_ parameter:\r\r\geekmath fun Read (m: Memory, d: Data, a: Addr) {\\\r d = m.map[a]\\\r }\r \rActions on the system as a whole can be specified using these primitive operations; in Z, this idiom is called 'promotion'. A read on the system is equivalent to reading the cache:\r\r\geekmath fun SystemRead (s: System, d: Data, a: Addr) {\\\r Read (s.cache, d, a)\\\r }\r\rThe _Read_ operation has an implicit precondition. Since the data parameter _d_ is constrained (implicitly by its declaration) to be scalar---that is, a singleton set---the relation _m.map_ must include a mapping for the address parameter _a_, since otherwise the expression _m.map[a]_ will evaluate to the empty set, and the formula will not be satisfiable. This precondition is inherited by _SystemRead_. If the address _a_ is not in the cache, the operation cannot proceed, and it will be necessary first to load the data from main memory. It is convenient to specify this action as a distinct operation:\r\r\geekmath fun Load (s,s': System, a: Addr) {\\\r a !in s.cache.addrs\\\r s'.cache.map = s.cache.map + (a->s.main.map[a])\\\r s'.main = s.main\\\r }\r\rThe + operator is just set union (in this case, of two binary relations, the second consisting of a single tuple). A write on the system involves a write to the cache, and setting the dirty bit. Again, this can be specified using a primitive memory operation:\r\r\geekmath fun SystemWrite (s,s': System, d: Data, a: Addr) {\\\r Write (s.cache, s'.cache, d, a)\\\r s'.cache.dirty = s.cache.dirty + a\\\r s'.main = s.main\\\r }\r\rA cache has much smaller capacity than main memory, so it will occasionally be necessary (prior to loading or writing) to flush lines from the cache back to main memory. We specify flushing as a non-deterministic operation that picks some subset of the cache addrs and writes them back to main memory:\r\r\geekmath fun Flush (s,s': System) {\\\r some x: set s.cache.addrs {\\\r s'.cache.map = s'.cache.map - (x->Data)\\\r s'.cache.dirty = s.cache.dirty - x\\\r s'.main.map = s.main.map ++ \\\r {a: x, d: Data | d = s.cache.map[a]}\\\r }\r\rThe - operator is set difference; note that it is applied to sets of addresses (in the third line) and to binary relations (in the second). The comprehension expression creates a relation of pairs _a_->_d_ satisfying the condition.\r\rFinally, it is often useful to specify the initial conditions of a system. To say that the cache initially has no addresses, we might write a function imposing this condition on a memory system:\r\r\geekmath fun Init (s: System) {no s.cache.addrs}\r\r\subsection Traces\r\rTo support analyses of behaviours consisting of sequences of states, we declare two signatures, for ticks of a clock and traces of states:\r\r\geekmath sig Tick {}\\\rsig SystemTrace {\\\r ticks: set Tick,\\\r first, last: ticks,\\\r next: (ticks - last) !->! (ticks - first)\\\r state: ticks ->! System}\\\r {\\\r first.*next = ticks\\\r Init (first.state)\\\r all t: ticks - last | \\\r some s = t.state, s' = t.next.state |\\\r Flush (s,s')\\\r || (some a: Addr | Load (s,s',a))\\\r || (some d: Data, a: Addr | SystemWrite (s,s',d,a))\\\r }\r\rEach trace consists of a set of _ticks_, a _first_ and _last_ tick, an ordering relation _next_ (whose declaration makes it a bijection from all ticks except the last to all ticks except the first), and a relation _state_ that maps each tick to a system state.\r\rThe fact appended to the signature states first a generic property of traces: that the ticks of a trace are those reachable from the first tick. It then imposes the constraints of the operations on the states in the trace. The initial condition is required to hold in the first state. Any subsequent pair of states is constrained to be related by one of the three side-effecting operations. The existential quantifier plays the role of a _let_ binding, allowing _s_ and _s'_ in place of _t.state_ and _t.next.state_, representing the state for tick _t_ and the state for its successor _t.next_. Note that this formulation precludes stuttering; we could admit it simply by adding the disjunct _s_=_s'_ allowing a transition that corresponds to no operation occurring.\r\rBear in mind that this fact is a constraint on all atoms in the set _SystemTrace_. As a free standing fact, the second line of the fact---the initial condition--- would have been written:\r\r\geekmath fact {all x: SystemTrace | Init ((x.first).(x.state))}\r\r\subsection Abstraction\r\rAbstraction relationships are easily expressed using our function syntax. To show that our memory system refines a simple memory without a cache, we define an abstraction function _Alpha_ saying that a system corresponds to a memory that is like the system's memory, overwritten by the entries of the system's cache:\r\r\geekmath fun Alpha (s: System, m: Memory) {\\\r m.map = s.main.map ++ s.cache.map\\\r }\r \rAs another example, if our linked list were to represent a set, we might define the set corresponding to a given list as that containing the elements reachable from the start:\r\r\geekmath fun ListAlpha (p: List, s: set Elt) {\\\r s = p.*rest.elt\\\r }\r\r\subsection Assertions\r\rTheorems about a specification are packaged as _assertions_. An assertion is simply a formula that is intended to hold. A tool can check an assertion by searching for a counterexample---that is, a model of the formula's negation.\r\rThe simplest kinds of assertion record consequences of state properties. For example,\r\r\geekmath assert {\\\r all s: System | DirtyInv (s) && no s.cache.dirty\\\r => s.cache.map in s.main.map\\\r }\r\rasserts that if the dirtiness invariant holds,and there are no dirty addresses, then the mapping of addresses to data in the cache is a subset of the mapping in the main memory.\r\rAn assertion can express consequences of operations. For example,\r\r\geekmath assert {\\\r all s: System, d: Data, a: Addr |\\\r SystemRead (s,d,a) => a in s.cache.addrs\\\r }\r\rembodies the claim made above that _SystemRead_ has an implicit precondition; it asserts that whenever _SystemRead_ occurs for an address, that address must be in the cache beforehand. An assertion can likewise identify a consequence in the post-state; this assertion\r\r\geekmath assert {\\\r all s,s': System, d: Data, a: Addr |\\\r SystemWrite (s,s',d,a) => s'.cache.map[a] = d\\\r }\r \rsays that after a _SystemWrite_, the data value appears in the cache at the given address. \r\rPreservation of an invariant by an operation is easily recorded as an assertion. To check that our dirtiness invariant is preserved when writes occur, we would assert\r\r\geekmath assert {\\\r all s,s': System, d: Data, a: Addr |\\\r SystemWrite (s,s',d,a) && DirtyInv (s) => DirtyInv (s')\\\r }\r\rInvariant preservation is not the only consequence of an operation that we would like to check that relates pre- and post-states. We might, for example, want to check that operations on the memory system do not change the set of addresses of the main memory. For the _Flush_ operation, for example, the assertion would be\r\r\geekmath assert {\\\r all s,s': System | Flush(s,s') => s.main.addrs = s'.main.addrs\\\r }\r \rwhich holds only because the cache addresses are guaranteed to be a subset of the main memory addresses (by the fact associated with the _System_ signature).\r\rThe effect of a sequence of operations can be expressed by quantifying appropriately over states. For example, \r\r\geekmath assert {\\\r all s, s': System, a: Addr, d,d': Data | \\\r SystemWrite (s,s',d,a) && SystemRead (s',d',a) => d = d'\\\r }\r\rsays that when a write is followed by a read of the same address, the read returns the data value just written.\r\rTo check that a property holds for all reachable states, we can assert that the property is an invariant of every operation, and is established by the initial condition. This strategy can be shown (by induction) to be sound, but it is not complete. A property may hold for all reachable states, but may not be preserved because an operation breaks the property when executed in a state that happens not to be reachable.\r\rTraces overcome this incompleteness. Suppose, for example, that we want to check the (rather contrived) property that, in every reachable state, if the cache contains an address that isn't dirty, then it agrees with the main memory on at least one address:\r\r\geekmath fun DirtyProp (s: System) {\\\r some (s.cache.addrs - s.cache.dirty)\\\r => some a: Addr | s.cache.map[a] = s.main.map[a]\\\r }\r\rWe can assert that this property holds in the last state of every trace:\r\r\geekmath assert {\\\r all t: SystemTrace | with t | DirtyProp (last.state)\\\r }\r \rThis assertion is valid, even though _DirtyProp_ is not an invariant. A write invoked in a state in which all clean entries but one had non-matching values can result in a state in which there are still clean entries but none has a matching value.\r\rFinally, refinements are checked by assertions involving abstraction relations. We can assert that a _SystemWrite_ refines a basic _Write_ operation on a simple memory:\r\r\geekmath assert {\\\r all s,s': System, m,m': Memory, a: Addr, d: Data |\\\r Alpha (s,m) && Alpha (s',m') && SystemWrite (s,s',a,d)\\\r => Write (m,m',a,d)\\\r }\r\ror that the _Flush_ operation is a no-op when viewed abstractly:\r\r\geekmath assert {\\\r all s,s': System, m,m': Memory |\\\r Alpha (s,m) && Alpha (s',m') && Flush (s,s')\\\r => m.map = m'.map\\\r }\r\rNote the form of the equality; _m = m'_ would be wrong, since two distinct memories may have the same mapping, and the abstraction _Alpha_ constrains only the mapping and not the memory atom itself.\r\rMany of the assertions shown here can be made more succinct by the function shorthand explained in Section 3.7 below. For example, the assertion that a read following a write returns the value just written becomes:\r\r\geekmath assert {\\\r all s: System, a: Addr, d: Data | \\\r SystemRead (SystemWrite (s,d,a),a) = d\\\r }\r\rand the assertion that _Flush_ is a no-op becomes:\r\r\geekmath assert {\\\r all s: System | Alpha (s).map = Alpha (Flush (s)).map\\\r }\r\r\subsection Polymorphism\r\rSignatures can be parameterized by signature types. Rather than declaring a linked list whose elements belong to a particular type _Elt_, as above, we would prefer to declare a generic list:\r\r\geekmath sig List [T] {}\\\rsig NonEmptyList [T] extends List [T] {elt: T, rest: List [T]}\r\rFunctions and facts may be parameterized in the same way, so we can define generic operators, such as:\r\r\geekmath fun first [T] (p: List [T]): T {result = p.elt}\\\rfun last [T] (p: List [T]): T {some q: p.*rest | result = q.elt && no q.rest}\\\rfun elements [T] (p: List [T]): set T {result = p.*rest.elt}\r\rIn addition, let's define a generic function that determines whether two elements follow one another in a list:\r\r\geekmath fun follows [T] (p: List[T], a,b: T) {\\\r some x: p.*rest | x.elt = a && x.next.elt = b\\\r }\r\rTo see how a generic signature and operators are used, consider replacing the traces of Section 2.6 with lists of system states. Define a function that determines whether a list is a trace:\r\r\geekmath fun isTrace (t: List [System]) {\\\r Init (first(t))\\\r all s, s': System | follows (t,s,s') => {\\\r Flush (s,s')\\\r || (some a: Addr | Load (s,s',a))\\\r || (some d: Data, a: Addr | SystemWrite (s,s',d,a))\\\r }\\\r }\r\rNow our assertion that every reachable system state satisfies _DirtyProp_ can now be written:\r\r\geekmath assert {\\\r all t: List[System] | isTrace(t) => DirtyProp (last(t))\\\r }\r\r\subsection Variants\r\rTo illustrate the flexibility of our notation, we sketch a different formulation of state machines oriented around transitions rather than states.\r\rLet's introduce a signature representing state transitions of our memory system:\r\r\geekmath sig SystemTrans {pre,post: System}\\\r {pre.main.addrs = post.main.addrs}\r\rDeclaring the transitions as a signature gives us the opportunity to record properties of all transitions---in this case requiring that the set of addresses of the main memory is fixed.\r\rNow we introduce a subsignature for the transitions of each operation. For example, the transitions that correspond to load actions are given by:\r\r\geekmath sig LoadTrans extends SystemTrans {a: Addr}\\\r {Load (pre, post, a)}\r# } {\r# a !in pre.cache.addrs\\\r# post.cache.map = pre.cache.map ++ (a->pre.main.map[a])\\\r# post.main = pre.main\\\r# }\r# \r# The formula here is actually identical to the one declared above, but with _pre_ and _post_ for # _s_ and _s'_ ; we could in fact replace it by the function application _Load(pre,post,a)_.\r\rFor each invariant, we define a set of states. For the states satisfying the dirty invariant, we might declare\r\r\geekmath sig DirtyInvStates extends System {}\r\ralong with the fact\r\r\geekmath fact {DirtyInvStates = {s: System | DirtyInv(s)}}\r\rTo express invariant preservation, it will be handy to declare a function that gives the image of a set of states under a set of transitions:\r\r\geekmath fun postimage (ss: set System, tt: set SystemTrans): set System {\\\r result = {s: System | some t: tt | t.pre in ss && s = t.post}\\\r }\r\rso that we can write the assertion like this:\r\r\geekmath assert {postimage (DirtyInvStates, LoadTrans) in DirtyInvStates}\r\rFor an even more direct formulation of state machine properties, wemight have defined a transition relation instead:\r\r\geekmath fun Trans (r: System -> System) {\\\r all s, s' : System | \\\r s->s' in r => Flush (s,s') || ...\\\r }\r\rThen, using transitive closure, we can express the set of states reachable from an initial state, and assert that this set belongs to the set characterized by some property:\r\r\geekmath assert {all r: System -> System, s: System |\\\r Init (s) && Trans(r) => s.*r in DirtyPropStates\\\r }\r\rwhere _DirtyPropStates_ is defined analogously to _DirtyInvStates_.\r\r\subsection Definitions\r\rInstead of declaring the addresses of a memory along with its mapping, as we did before:\r\r\geekmath sig Memory {\\\r addrs: set Addr,\\\r map: addrs ->! Data\\\r }\r\rwe could instead have declared the mapping alone:\r\r\geekmath sig Memory {\\\r map: Addr ->? Data\\\r }\r\rand then _defined_ the addresses using a subsignature:\r\r\geekmath sig MemoryWithAddrs extends Memory {\\\r addrs: set Addr}\\\r {addrs = {a: Addr | some a.map}}\r \rNow by making the subsignature subsume all memories:\r\r\geekmath fact {Memory in MemoryWithAddrs}\r\rwe have essentially 'retrofitted' the field. Any formula involving memory atoms now implicitly constrains the _addrs_ field. For example, we can assert that _Read_ has an implicit precondition requiring that the argument be a valid address:\r\r\geekmath assert {all m: Memory, a: Addr, d: Data | Read (m,d,a) => a in m.addrs}\r\reven though the specification of _Read_ was written when the field _addrs_ did not even exist.\r\r\section Semantics\r\rFor completeness, we give an overview of the semantics of the language. The novelties with respect to the original version of Alloy [4] are (1) the idea of organizing relations around basic types as signatures, (2) the treatment of extension as subsetting, and (3) the packaging of formulas in a more explicit (and conventional) style. The semantic basis has been made cleaner, by generalizing relations to arbitrary arity, eliminating 'indexed relations' and the need for a special treatment of sets.\r\r\subsection Types\r\rWe assume a universe of atoms. The standard notion of a mathematical relation gives us our only composite datatype. The value of an expression will always be a relation---that is, a collection of tuples of atoms. Relations are first order: the elements of a tuple are themselves atoms and never relations.\r\rThe language is strongly typed. We partition the universe into subsets each associated with a _basic_ type, and write (T_1, T_2, ..., T_n) for the type of a relation whose tuples each consist of _n_ atoms, with types T_1, T_2, etc.\r\rA set is represented semantically as a unary relation, namely a relation whose tuples each contain one atom. A tuple is represented as a singleton relation, namely a relation containing exactly one tuple. A scalar is represented as a unary, singleton relation. We use the terms 'set', 'tuple' and 'scalar' to describe relations with the appropriate properties. Basic types are used only to construct relation types, and every expression that appears in a specification has a relational type. Often we will say informally that an expression has a type _T_ where _T_ is the name of a basic type when more precisely we mean that the expression has the type (_T_).\r\rSo, in contrast to traditional mathematical style, we do not make distinctions amongst the atom _a_, the tuple (_a_), the set {_a_} containing just the atom, or the set {(_a_)} containing the tuple, and represent all of these as the last. This simplifies the semantics and gives a more succinct and uniform syntax.\r# Because the language is first order (and has no sets of sets, for example), it requires no coercions, and seems not to cause confusion even for novice specifiers.\r\r\subsection Expression Operators\r\rExpressions can be formed using the standard set operators written as ASCII characters: union (+), intersection (&) and difference (-). Some standard relational operators, such as transpose (~) and transitive closure (^), can be applied to expressions that denote binary relations. Relational override (++) has its standard meaning for binary relations but can applied more broadly.\r#The type rules and semantics are completely standard. For example, if _e_ has the type (S,T), then ~_e_ has the type (T,S) and denotes the collection of pairs obtained by reversing each pair in _e_; if _p_ and _q_ both have the type (T_1, T_2, ..., T_n), then the union _p+q_, intersection _p_&_q_, and difference _p-q_ also have that type, and denote respectively the relations whose tuples are those that appear in either of _p_ and _q_, both of _p_ and _q_, and _p_ but not _q_.\r\rThere are two special relational operators, dot and arrow. The dot operator is a generalized relational composition. Given expressions $p$ and $q$, the expression $p.q$ contains the tuple\r$\angleleft\sep p\sub<1>, ... p\sub<m-1>, q\sub<2>, ..., q\sub<n>\angleright$\rwhen _p_ contains \r@math \langle@sep p_1, ..., p_{m}\rangle,\r_q_ contains\r@math \langle@sep q_1, ... q_n\rangle,\rand\r@math p_m = q_1. The last type of _p_ and the first type of _q_ must match, and _m_ + _n_, the sum of the arities of _p_ and _q_, must be three or more so that the result is not degenerate. When _p_ is a set and _q_ is a binary relation, the composition _p.q_ is the standard relational image of _p_ under _q_; when _p_ and _q_ are both binary relations, _p.q_ is standard relational composition. In all of the examples above, the dot operator is used only for relational image.\r\rThe arrow operator is cross product: _p \textarrow q_ is the relation containing the tuple\r@math \langle@sep p_1, ..., p_{m}, q_1, ... q_n\rangle\rwhen _p_ contains \r@math \langle@sep p_1, ..., p_{m}\rangle,\rand _q_ contains\r@math \langle@sep q_1, ... q_n\rangle.\rIn all the examples in this paper, _p_ and _q_ are sets, and _p \textarrow q_ is their standard cross product.\r\r\subsection Formula Operators\r\rElementary formulas are formed from the subset operator, written _in_. Thus _p in q_ is true when every tuple in _p_ is in _q_. The formula _p : q_ has the same meaning, but when _q_ is a set, adds an implicit constraint that _p_ be scalar (ie, a singleton). This constraint is overridden by writing _p: option q_ (which lets _p_ to be empty or a scalar) or _p: set q_ (which eliminates the constraint entirely). Equality is just standard set equality, and is short for a subset constraint in each direction.\r\rAn arrow that appears as the outermost expression operator on the right-hand side of a subset formula can be annotated with _multiplicity markings_: + (one or more), ? (zero or one) and ! (exactly one). The formula\r\r\geekmath r: S m \textarrow n T\r\rwhere _m_ and _n_ are multiplicity markings constrains the relation _r_ to map each atom of _S_ to _n_ atoms of _T_, and to map _m_ atoms of _S_ to each atom of _T_. _S_ and _T_ may themselves be product expressions, but are usually variables denoting sets. For example,\r\r\geekmath r: S \textarrow ! T\\\rr: S ? \textarrow ! T\r\rmake _r_ respectively a total function on _S_ and an injection.\r\rLarger formulas are obtained using the standard logical connectives: && (and), || (or), ! (not), => (implies), _iff_ (bi-implication). The formula _if b then f else g_ is short for _b_ => _f_ && !_b_ => _g_. Within curly braces, consecutive formulas are implicitly conjoined.\r\rQuantifications take their usual form:\r\r\geekmath all x: e | F\r\ris true when the formula _F_ holds under every binding of the variable _x_ to a member of the set _e_. In addition to the standard quantifiers, _all_ (universal) and _some_ (existential), we have _no_, _sole_ and _one_ meaning respectively that there are no values, at most one value, and exactly one value satisfying the formula. For a quantifier _Q_ and expression _e_, the formula _Q e_ is short for _Q x: T | e_ (where _T_ is the type of _e_), so _no e_, for example, says that _e_ is empty.\r\rThe declaration of a quantified formula is itself a formula---an elementary formula in which the left-hand side is a variable. Thus\r\r\geekmath some x = e | F\r\ris permitted, and is a useful way to express a _let_ binding. Quantifiers may be higher-order; the formula\r\r\geekmath all f: s ->! t | F\r\ris true when _F_ holds for every binding of a total function from _s_ to _t_ to the variable _f_. Our analysis tool cannot currently handle higher-order quantifiers, but many uses of higher-order quantifiers that arise in practice can be eliminated by skolemization.\r\rFinally, we have relational comprehensions; the expression\r\r\geekmath {x_1: e_1, x_2: e_2, ... | F}\r\rconstructs a relation of tuples with elements _x_1_, _x_2_, etc., drawn from set expressions _e_1_, _e_2_, etc., whose values satisfy _F_.\r\r# \subsection Choice of Operator Symbols\r# \r# The choice of symbols, especially the arrow, may seem unconventional, but results in familiar-# looking formulas. The dot operator generalizes the 'navigation expressions' of Syntropy# [CD94], now adopted by UML's Object Constraint Language [17], and is intended to be fa# miliar to programmers by resembling object dereferencing. Thus, _x.f_ can be viewed as dere# ferencing the object _x_ with field _f_ when _x_ is a scalar and _f_ is a binary relation. The cho# ice of relational composition rather than function application allows such an expression to be wr# itten without concern for whether _f_ is a function. It also gives a simple and workable treatmen# t of partiality. When _x_ is not in the domain of _f_, _x.f_ is the empty set, and _x.f = y_ will be# false if _y_ is a scalar.\r# \r# The arrow notation is designed to allow declarations to be written in a familiar way, but to be # given a simple, first-order interpretation. For example, if _S_ and _T_ denote sets,\r# \r# \geekmath f: S \textarrow T\r# \r# declares _f_ to be a binary relation from _S_ to _T_. A conventional interpretation would have # the arrow construct a set of relations---a higher-order notion. Instead, we interpret the arrow # as cross product and the colon as subset, with the same result. The choice of arrow is also # convenient for constructing tuples; when _x_ and _y_ are scalars, the formula# \r# \r# \geekmath r' = r + (x \textarrow y)\r# \r# makes _r'_ the relation containing the tuples of _r_, and additionally, a mapping from _x_ to # _y_. # \r\subsection Signatures\r\rA _signature_ declaration introduces a basic type, along with a collection of relations called _fields_. The declaration\r\r\geekmath sig S {f: E}\r\rdeclares a basic type _S_, and a relation _f_. If _E_ has the type (T_1, T_2, ..., T_n), the relation _f_ will have the type (S, T_1, T_2, ..., T_n), and if _x_ has the type _S_, the expression _x.f_ will have the same type as _E_. When there are several fields, field names already declared may appear in expressions on the right-hand side of declarations; in this case, a field _f_ is typed as if it were the expression _this.f_, where _this_ denotes an atom of the signature type (see Section 3.6).\r\rThe meaning of a specification consisting of a collection of signature declarations is an assignment of values to global constants-- the signatures and the fields. For example, the specification\r\r\geekmath sig Addr {}\\\rsig Data {}\\\rsig Memory {map: Addr -> Data}\r\rhas 4 constants---the three signatures and one field---with assignments such as:\r\r\geekmath Addr = {a0, a1}\\\rData = {d0, d1, d2}\\\rMemory = {m0, m1}\\\rmap = {(m0,a0,d0), (m1,a0,d1), (m1,a0,d2)}\r\rcorresponding to a world in which there are 2 addresses, 3 data values and 2 memories, with the first memory (_m0_) mapping the first address (_a0_) to the first data value (_d0_), and the second memory (_m1_) mapping the first address (_a0_) both to the second (_d1_) and third (_d2_) data values.\r\rA fact is a formula that constrains the constants of the specification, and therefore tends to reduce the set of assignments denoted by the specification. For example,\r\r\geekmath fact {all m: Memory | all a: Addr | sole m.map[a]}\r\rrules out the above assignment, since it does not permit a memory (such as _m1_) to map an address (such as _a0_) to more than one data value. \r\rThe meaning of a function is a set of assignments, like the meaning of the specification as a whole, but these include bindings to parameters. For example, the function\r\r\geekmath fun Read (m: Memory, d: Data, a: Addr) {\\\r d = m.map[a]\\\r }\r\rhas assignments such as:\r\r\geekmath Addr = {a0, a1}\\\rData = {d0, d1, d2}\\\rMemory = {m0, m1}\\\rmap = {(m0,a0,d1)}\\\rm = {m0}\\\rd = {d1}\\\ra = {a0}\r\rThe assignments of a function representing a state invariant correspond to states satisfying the invariant; the functions of a function representing an operation (such as _Read_) correspond to executions of the operation.\r\rAn assertion is a formula that is claimed to be _valid_: that is, true for every assignment that satisfies the facts of the specification. To check an assertion, one can search for a _counterexample_: an assignment that makes the formula false.\rFor example, the assertion\r\r\geekmath assert {\\\r all m,m': Memory, d: Data, a: Addr | Read (m,d,a) => Read (m',d,a)}\r\rwhich claims, implausibly, that if a read of memory _m_ returns _d_ at _a_, then so does a read at memory _m'_, has the counterexample\r\r\geekmath Addr = {a0}\\\rData = {d0,d1}\\\rMemory = {m0, m1}\\\rmap = {(m0,a0,d0), (m1,a0,d1)}\r\rTo find a counterexample, a tool should negate the formula and then skolemize away the bound variables, treating them like the parameters of a function, with values to be determined as part of the assignment. In this case, the assignment might include:\r\r\geekmath m = {m0}\\\rm' = {m1}\\\rd = {d0}\\\ra = {a0}\r\r\subsection Extension\r\rNot every signature declaration introduces a new basic type. A signature declared without an extension clause is a _type signature_, and creates both a basic type and a set constant of the same name. A signature _S_ declared as an extension is a _subsignature_, and creates only a set constant, along with a constraint making it a subset of each _supersignature_ listed in the extension clause. The subsignature takes on the type of the supersignatures, so if there is more than one, they must therefore have the same type, by being direct or indirect subsignatures of the same type signature.\r\rA field declared in a subsignature is as if declared in the corresponding type signature, with the constraint that the domain of the field is the subsignature. For example,\r\r\geekmath sig List {}\\\rsig NonEmptyList extends List {elt: Elt,rest: List}\r\rmakes _List_ a type signature, and _NonEmptyList_ a subset of _List_. The fields _elt_ and _rest_ map atoms from the type _List_, but are constrained to have domain _NonEmptyList_. Semantically, it would have been equivalent to declare them as fields of _List_, along with facts constraining their domains:\r\r\geekmath sig List {elt: Elt,rest: List}\\\rsig NonEmptyList extends List {}\\\rfact {elt.Elt in NonEmptyList}\\\rfact {rest.List in NonEmptyList}\r\r(exploiting our dot notation to write the domain of a relation _r_ from _S_ to _T_ as _r.T_).\r\r\subsection Overloading and Implicit Prefixing\r\rWhenever a variable is declared, its type can be easily obtained from its declaration (from the type of the expression on the right-hand side of the declaration), and every variable appearing in an expression is declared in an enclosing scope. The one complication to this rule is the typing of fields.\r\rFor modularity, a signature creates a local namespace. Two fields with the name _f_ appearing in different signatures do not denote the same relational constant. Interpreting an expression therefore depends on first resolving any field names that appear in it. \r#We have devised a simple resolution scheme whose details are beyond the scope of this paper.\rIn an expression of the form _e.f_, the signature to which _f_ belongs is determined according to the type of _e_. To keep the scheme simple, we require that sometimes the specifier resolve the overloading explicitly by writing the field _f_ of signature _S_ as _S$f_. (At the end of the previous section, for example, the reference in the fact to _rest_ should actually be to _List$rest_, since the context does not indicate which signature _rest_ belongs to.)\r\rIn many formulas, a single expression is dereferenced several times with different fields. A couple of language features are designed to allow these formulas to be written more succinctly, and, if used with care, more comprehensibly. First, we provide two syntactic variants of the dot operator. Both _p_::_q_ and _q_[_p_] are equivalent to _p.q_, but have different precedence: the double colon binds more tightly than the dot, and the square brackets bind more loosely than the dot. Second, we provide a _with_ construct similar to Pascal's that makes dereferencing implicit.\r\rConsider, for example, the following simplified signature for a trace:\r\r\geekmath sig Trace {\\\r ticks: set Tick,\\\r first: Tick,\\\r next: Tick -> Tick,\\\r state: Tick -> State\\\r }\r\rEach trace _t_ has a set of ticks _t.ticks_, a first tick _t.first_, an ordering _t.next_ that maps ticks to ticks, and a relation _t.state_ mapping each tick to a state. For a trace _t_ and tick _k_, the state is _k_.(_t.state_); the square brackets allow this expression to be written instead as _t.state_[_k_]. To constrain _t.ticks_ to be those reachable from _t. first_ we might write:\r\r\geekmath fact {all t: Trace | (t.first).*(t.next ) = t.ticks}\r\rRelying on the tighter binding of the double colon, we can eliminate the parentheses:\r\r\geekmath fact {all t: Trace | t::first.*t::next = t.ticks}\r\rUsing _with_, we can make the _t_ prefixes implicit:\r\r\geekmath fact {all t: Trace | with t | first.*next = ticks}\r\rIn general, _with e | F_ is like _F_, but with _e_ prefixed wherever appropriate to a field name. Appropriateness is determined by type: _e_ is matched to any field name with which it can be composed using the dot operator.\r#Fields that are prefixed using a double colon operator are not automatically prefixed, so one can use _with_ to prefix some fields of a given signature but not others. There is a corresponding _with_ construct for expressions also, so that _with e | E_ is like the expression _E_, with _e_ prefixed as appropriate.\rA fact attached to a signature _S_ is implicitly enclosed by _all this: S | with this |_, and the declarations of a signature are interpreted as constraints as if they had been declared within this scope. Consequently, the declaration of _first_ above should be interpreted as if it were the formula:\r\r\geekmath all this: Trace | with this | first: ticks\r\rwhich is equivalent to\r\r\geekmath all this: Trace | this.first: this.ticks\r\rand should be typed accordingly.\r# \r# So, in the following fuller version of the above signature:\r# \r# \geekmath sig Trace {\\\r# ticks: set Tick\\\r# first: ticks,\\\r# next: (ticks - first) ->? ticks\\\r# state: ticks ->! State\\\r# } {first.*next = ticks}\r# \r# the declaration of the field _first_, for example, includes the constraint\r# \r# \geekmath all this: Trace | with this | first: ticks\r# \r# which is equivalent to\r# \r# \geekmath all this: Trace | this.first: this.ticks\r\r\subsection Function Applications\r\rA function may be applied by binding its parameters to expressions. The resulting application may be either an expression or a formula, but in both cases the function body is treated as a formula. The formula case is simple: the application is simply short for the body with the formal parameters replaced by the actual expressions (and bound variables renamed where necessary to avoid clashes).\r\rThe expression case is more interesting. The application is treated as a syntactic sugar. Suppose we have a function application expression, _e_ say, of the form\r\r\geekmath f(a_1, a_2, ..., a_n)\r\rthat appears in an elementary formula _F_. The declaration of the function _f_ must list _n_ + 1 formal arguments, of which the _second_ will be treated as the result. The entire elementary formula is taken to be short for\r\r\geekmath all result: D | f (a_1, result, a_2, ..., a_n) => F [result/e]\r\rwhere _D_ is the right-hand side of the declaration of the missing argument, and _F_ [_result_/_e_] is _F_ with the fresh variable _result_ substituted for the application expression _e_. The application of _f_ in this elaborated formula is now a formula, and is treated simply as an inlining of the formula of _f_.\r\r#Type checking will thus require that the actual arguments match the formals that are listed first, third, fourth, fifth, etc. (This choice of the second argument, incidentally, is one concession we make to specifying state machines; function applications can be used to model operation invocations in which it is convenient to declare the pre- and post- states as the first and second arguments of the operation.)\r#\rTo see how this works, consider the definition of a function _dom_ that gives the domain of a relation over signature _X_:\r\r\geekmath fun dom (r: X -> X, d: set X) {d = r.X}\r\r(We have defined the function monomorphically for a homogeneous relation. In practice, one would define a polymorphic function, but we want to avoid conflating two unrelated issues.) Here is a trivial assertion that applies the function as an expression:\r\r\geekmath assert {all p: X \textarrow X | (dom (p)).p in X}\r\rDesugaring the formula, we get\r\r\geekmath all p: X \textarrow X | all result: set X | dom (p, result) => result.p in X\r\rand then inlining\r\r\geekmath all p: X \textarrow X | all result: set X | result = p.X => result.p in X\r\rThis formula can be reduced (by applying a universal form of the One Point Rule) to\r\r\geekmath all p: X \textarrow X | (p.X).p in X\r\rwhich is exactly what would have been obtained had we just replaced the application expression by the expression on the right-hand side of the equality in the function's definition!\r#\r# If there is more than one application expression in an elementary formula, a fresh quantification is # generated for each. For example,# \r# \r# \geekmath assert {all p, q: X \textarrow X | dom (p.q) in dom (p)}\r# \r# becomes\r# \r# \geekmath all p,q: X \textarrow X | all result1, result2: set X | \\\r# dom (p.q, result1) => dom (p, result2) => result1 in result2\r# \r# which can again be reduced by inlining and the One Point Rule to \r# \r# \geekmath all p,q: X \textarrow X | (p.q).X in p.X\r\rNow let's consider an implicit definition. Suppose we have a signature _X_ with an ordering _lte_, so that _e.lte_ is the set of elements that _e_ is less than or equal to, and a function _min_ that gives the minimum of a set, defined implicitly as the element that is a member of the set, and less than or equal to all members of the set:\r\r\geekmath sig X {lte: set X}\\\rfun min (s: set X, m: option X) {\\\r m in s && s in m.lte\\\r }\r\rBecause the set may be empty, _min_ is partial. Depending on the properties of _lte_ it may also fail to be deterministic. A formula that applies this function\r\r\geekmath assert {all s: set X | min (s) in s}\r\rcan as before be desugared\r\r\geekmath all s: set X | all result: option X | min (s, result) => result in s\r\rand expanded by inlining\r\r\geekmath all s: set X | all result: option X |\\\r (result in s) && s in result.lte => result in s\r\rbut in this case the One Point Rule is not applicable.\r\rAs a convenience, our language allows the result argument of a function to be declared anonymously in a special position, and given the name _result_. The domain function, for example, can be defined as:\r\r\geekmath fun dom (r: X -> X): set X {result = r.X}\r\rHow the function is defined has no bearing on how it is used; this definition is entirely equivalent to the one above, and can also be applied as a formula with two arguments.\r\r\subsection Polymorphism\r\rPolymorphism is treated as a syntactic shorthand. Lack of space does not permit a full discussion here.\r\r\section Related Work\r\rWe have shown how a handful of elements can be assembled into a rather simple but flexible notation. The elements themselves are far from novel---indeed, we hope that their familiarity will make the notation easy to learn and use---but their assembly into a coherent whole results in a language rather different from existing specification languages.\r\r\subsection New Aspects\r\rThe more novel aspects of our work are:\r\r\point \cdot _Objectification of state_. Most specification languages represent states as cartesian products of components; in our approach, a state, like a member of any signature, is an individual---a distinct atom with identity. A similar idea is used in the situation calculus [11], whose 'relational fluents' add a situation variable to each time-varying relation. The general idea of objectifying all values is of course the foundation of object-oriented programming languages, and was present in LISP. Interestingly, object-oriented variants of Z (such as [1]) do not objectify schemas. The idea of representing structures in first-order style as atoms is present also in algebraic specifications such as Larch [2], which treat even sets and relations in this manner.\r\r\point \cdot _Components as relations_. Interpreting fields of a structure as functions goes back to early work on verification, and is widely used (for example, by Leino and Nelson [10]). We are not aware, however, of specification languages that use this idea, or that flatten fields to relations over atoms.\r\r\point \cdot _Extension by global axioms_. The 'facts' of our notation allow the properties of a signature to be extended monotonically. The idea of writing axioms that constrain the members of a set constant declared globally is hardly remarkable, but it appears not to have been widely exploited in specification languages.\r\r\point \cdot _Extension by subset_. Treating the extension of a structure as a refinement modelled by subset results in a simple semantics, and melds well with the use of global axioms. Again, this seems to be an unremarkable idea, but one whose power has not been fully recognized.\r\r\subsection Old Aspects\r\rThe aspects of our work that are directly taken from existing languages are:\r\r\point \cdot _Formulas_. The idea of treating invariants, definitions, operations, etc, uniformly as logical formulas is due to Z [14].\r\r\point \cdot _Assertions_. Larch [2] provides a variety of constructs for adding intentional redundancy to a specification in order to provide error-detection opportunities. \r\r\point \cdot _Parameterized formulas_. The 'functional' style we have adopted, in which all formulas are explicitly parameterized, in contrast to the style of most specification languages, is used also by languages for theorem provers, such as PVS [13]. VDM [8] offers a mechanism called 'operation quotation' in which pre- and post conditions are reused by interpreting them as functions similar to ours.\r\r\point \cdot _Parametric Polymorphism_. The idea of parameterizing descriptions by types was developed in the programming languages community, most notably in the context of ML [12].\r\r\point \cdot _Implicit Prefixing_. Our 'with' operator is taken from Pascal [9].\r\r\point \cdot _Relational operators_. The dot operator, and the treament of scalars as singletons, comes from the earlier version of Alloy [4].\r#\r#\point \cdot _Function shorthands_. The idea of desugaring function applications by quantifying over the result is present in Beth's extensionality theorem [Beth].\r\r\subsection Z's Schema Calculus\r\rZ has been a strong influence on our work; indeed, this paper may be viewed as an attempt to achieve some of the power and flexibility of Z's schema calculus in a first-order setting. Readers unfamiliar with Z can find an excellent presentation of the schema calculus in [16]. The current definitive reference is [15], although Spivey's manual [14] is more accessible for practioners.\r\rA _schema_ consists of a collection of variable declarations and a formula constraining the variables. Schemas can be anonymous. When a name has been bound to a schema, it can be used in three different ways, distinguished according to context. First, it can be used as a _declaration_, in which case it introduces its variables into the local scope, constraining them with its formula. Second, where the variables are already in scope, it can be used as a _predicate_, in which case the formula applies and no new declarations are added. Both of these uses are syntactic; the schema can be viewed as a macro.\r\rIn the third use, the schema is semantic. Its name represents a set of _bindings_, each binding being a finite function from variables names to values. The bindings denoted by the schema name are the models of the schema's formula: those bindings of variable names to values that make the formula true.\r\rHow a schema is being applied is not always obvious; in the set comprehension {_S_}, for example, _S_ represents a declaration, so that the expression as a whole denotes the same set of bindings as _S_ itself. Given a binding _b_ for a schema with component variable _x_, the expression _b.x_ denotes the value assigned to _x_ in _b_. Unlike Alloy's dot, this dot is a function application, so for a set of bindings _B_, the expression _B.x_ is not well formed.\r\rOperations in Z are expressed using the convention that primed variables denote components of the post-state. A mechanism known as _decoration_ allows one to write _S'_ for the schema that is like _S_, but whose variable names have been primed. Many idioms, such as promotion, rely on being able to manipulate the values of a schema's variables in aggregate. To support this, Z provides the theta operator: \theta @sep _S_ is an expression that denotes a binding in which each variable _x_ that belongs to _S_ is bound to a variable of the same name _x_ declared in the local scope. Theta and decoration interact subtly: \theta @sep _S'_ is not a binding of _S'_, but rather binds each variable _x_ of _S_ to a variable _x'_ declared locally. So where we would write _s=s'_ to say that pre- and post-states _s_ and _s'_ are the same, a Z specifier would write \theta @sep _S_ = \theta @sep _S'_. This formula equates each component _x_ of _S_ to its matching component _x'_ of _S'_, because _x_ and _x'_ are the respective values bound to _x_ by \theta @sep _S_ and \theta @sep _S'_ respectively.\r\rOur 'fact' construct allows the meaning of a signature name to be constrained subsequent to its declaration. A schema, in contrast, is 'closed': a new schema name must be introduced for each additional constraint. This can produce an undesirable proliferation of names for a system's state, but it does make it easier to track down those formulas that affect a schema's meaning.\r\rThe variables of a schema can be renamed, but cannot be replaced by arbitrary expressions (since this would make nonsense of declarations).This requires the introduction of existential quantifiers where in our notation an expression is passed as an actual. On the other hand, when no renaming is needed, it is more succinct.\r\rZ's sequential composition operator is defined by a rather complicated transformation, and relies on adherence to particular conventions. The schema _P_ @sep \fatsemi @sep _Q_ is obtained by collecting primed variables in _P_ that match unprimed variables in _Q_; renaming these in both _P_ and _Q_ with a new set of variable names; and then existentially quantifying the new names away. For example, to say that a read following a write to the same address yields the value written, we would write:\r\r\geekmath\rall m: Memory, a: Addr, d, d': Data | Read (Write(m,a,d),d') => d = d'\r\rwhich is short for\r\r\geekmath all m: Memory, a: Addr, d, d': Data |\\\r all m': Memory | Write (m,m',a,d) => Read (m,a,d') => d = d'\r\rIn Z, assuming appropriate declarations of a schema _Memory_ and a given type _Data_, the formula would be:\r\r\geekmath\r\forall Memory; Memory'; x!: Data \fatdot Write \fatsemi Read [x!/d!] \implies x! = d!\r\rwhich is short for\r\r\geekmath\r\forall Memory; Memory'; x!: Data \fatdot \\\r \exists Memory'' \fatdot \\\r \exists Memory' \fatdot Write \and \theta @sep Memory' = \theta @sep Memory''\\\r \exists Memory'; d!: Data \fatdot \\\r Read \and \theta @sep Memory = \theta @sep Memory'' \and d! = x!\\\r \implies x! = d!\r\rThe key semantic difference between signatures and schemas is this. A signature is a set of atoms; its fields are relational constants declared in global scope. A schema, on the other hand, denotes a higher-order object: a set of functions from field names to values. Our approach was motivated by the desire to remain first order, so that the analysis we have developed [3] can be applied. Not surprisingly, there is a cost in expressiveness. We cannot express higher-order formulas, most notably those involving preconditions. Suppose we want to assert that our write operation has no implicit precondition. In Z, such an assertion is easily written:\r\r\geekmath\r\forall Memory; a?: Addr \fatdot \exists Memory'; d!: Data \fatdot Write\r\rWe might attempt to formulate such an assertion in our notation as follows:\r\r\geekmath assert {\\\r all m: Memory, a: Addr, d: Data | some m': Memory | Write (m,m',d,a)\r }\r\rUnfortunately, this has counterexamples such as\r\r\geekmath Addr = {a0}\\\rData = {d0}\\\rMemory = {m0, m1}\\\rmap = {}\r\rin which the _map_ relation lacks an appropriate tuple. Intuitively, the assertion claims that there is no context in which a write cannot proceed; a legitimate counterexample---but one we certainly did not intend---simply gives a context in which a memory with the appropriate address-value mapping is not available.\r\rWe have focused in this discussion on schemas. It is worth noting that Z is expressive enough to allow a style of structuring almost identical to ours, simply by declaring signatures as given types, fields and functions as global variables, and by writing facts, and the bodies of functions, as axioms. Field names would have to be globally unique, and the resulting specification would likely be less succinct than if expressed in our notation.\r\r\subsection Phenomenology\r\rPamela Zave and Michael Jackson have developed an approach to composing descriptions [18] that objectifies states, events and time intervals, and constrains their properties with global axioms. Objectification allows descriptions to be reduced to a common phenomenology, so that descriptions in different languages, and even in different paradigms can be combined. Michael Jackson has argued separately for the importance of objectification as a means of making a more direct connection between a formal description and the informal world: as he puts it, "domain phenomena are facts about individuals" [7]. It is reassuring that the concerns of language design and tractability of analysis that motivated our notation are not in conflict with sound method, and it seems that our notation would be a good choice for expressing descriptions in the form that Zave and Jackson have proposed.\r\r\section Evaluation\r\r\subsection Merits\r\rThe key motivations of the design of our mechanism have been minimality and flexibility. It is worth noting how this has been achived by the _omission_ of certain features:\r\r\point \cdot There is only one form of semantic structuring; our opinion is that adding extra mechanisms, for example to group operations into classes, does not bring enough benefit to merit the additional complexity, and tends to be inflexible. (Our language does provide some namespace control for signature and paragraph names in the style of Java packages, but this is trivial and does not interact with the basic mechanism).\r\r\point \cdot There is no subtyping; subsignatures are just subsets of their supersignatures, and have the same type. There are only two types: basic types (for signatures), and relational types (for expressions). Types are not nested.\r\r\point \cdot There is only one way that formulas are packaged for reuse. The same function syntax is used for observers, operations, refinement relations, etc. The function shorthand syntax unifies the syntax of both declaration and use for explicit and implicit function definitions.\r\r\point \cdot The values of a signature with fields are just like the values of any basic type; there is nothing like Z's notion of a schema binding.\r\rOur interpretation of a subsignature as a subset of the supersignature appears to be novel as a mechanism for structuring in a specification language. It has three nice consequences:\r\r\point \cdot _Elimination of type coercions_. If _x_ belongs to a signature _S_ whose extension _S'_ defines a field _f_, the expression _x.f_ will just denote an empty set if _x_ does not belong to _S'_. Contrast this with the treatment of subclasses in the Object Constraint Language [17], for example, which results in pervasive coercions and often prevents the use of set and relation operators (since elements must be coerced one at a time).\r\r\point \cdot _Ease of extension_. Constraints can be added to the subsignature simply by writing a constraint that is universally quantified over elements of that subset.\r\r\point \cdot _Definitional extension_. We can declare an extension _S'_ of a signature _S_ with additional fields, relate these fields to the fields declared explicitly for _S_, and then record the fact that _S=S'_ (as illustrated in Section 2.11). The effect is that every atom of _S_ has been extended with appropriately defined fields, which can be accessed whenever an expression denoting such an atom is in scope! We expect to find this idiom especially useful for defining additional fields for visualization purposes.\r\r\subsection Deficiencies\r\rOne might wonder whether, having encoded structures using atoms, and having provided quantifiers over those atoms, one can express arbitrary properties of higher-order structures. Unfortunately, but not surprisingly, this is not possible. The catch is that fields are treated in any formulas as global variables that are existentially quantified. To simulate higher-order logic, it would be necessary to allow quantifications over these variables, and since they have relational type, that would imply higher-order quantification. The practical consequence is that properties requiring higher-order logic cannot be expressed. One cannot assert that the precondition of an operation is no stronger than some predicate; one cannot in general specify operations by minimization; and one cannot express certain forms of refinement check. An example of this problem is given in Section 4.3 above. Whether the problem is fundamental or can be partially overcome remains to be seen.\r\rThe treatment of subsignatures as subsets has a nasty consequence. Since a field declared in a subsignature becomes implicitly a field of the supersignature, two subsignatures cannot declare fields of the same name. The extension mechanism is therefore not properly modular, and a specification should use hierarchical structure instead where this matters.\r\rModelling a set of states as atoms entails a certain loss of abstraction. In this specification\r\r\geekmath sig A {}\\\rsig S {a: A}\\\rfun op (s,s': S) {s.a = s'.a}\r\rthe operation _op_ has executions in which the pre- and post-states are equal (that is, the same atom in _S_), and executions in which only their _a_ components are equal. One might object that this distinction is not observable. Moreover, replacing the formula by _s=s'_ would arguably be an overspecification---a 'bias' in VDM terminology [8]. The situation calculus [11] solves this problem by requiring every operation to produce a state change: _s_ and _s'_ are thus regarded as distinct situations by virtue of occurring at different points in the execution. The dual of this solution is to add an axiom requiring that no two distinct atoms of _S_ may have equal _a_ fields. Either of these solutions is easily imposed in our notation.\r\rOur treatment of scalars and sets uniformly as relations has raised the concern that the resulting succinctness comes with a loss of clarity and redundancy. Extensive use of the previous version of our language, mostly by inexperienced specifiers, suggests that this is not a problem. The loss of some static checking is more than compensated by the semantic analysis that our tool performs.\r\r\section Conclusion\r\rTwo simple ideas form the basis of our modularity mechanism: (1) that a structure is just a set of atoms, and its fields are global relations that map those atoms to structure components; and (2) that extensions of a structure are just subsets. Our relational semantics, in which all variables and fields are represented as relations, makes the use of structures simple and succinct, and it ensures that the language as a whole remains first order. For a variety of modelling tasks, we believe that our approach provides a useful balance of expressiveness and tractability.\r\r\section* Acknowledgments\r\rThe language described here was refined by experience writing specifications, long before an analyzer existed, and by the development of the analyzer tool itself. Mandana Vaziri and Sarfraz Khurshid were our early adopters, and Brian Lin and Joe Cohen helped implement the tool. The paper itself was improved greatly by comments from Mandana and Sarfraz, from Michael Jackson, from Tomi Mannisto, and especially from Pamela Zave, whose suggestions prompted a major rewrite. Jim Woodcock helped us understand Z, and the clarity and simplicity of his own work has been a source of inspiration to us. Our ideas have also been improved by the comments of the members of IFIP working groups 2.3 and 2.9, especially Tony Hoare, Greg Nelson and Rustan Leino. This work was funded in part by ITR grant #0086154 from the National Science Foundation, by a grant from NASA, and by an endowment from Doug and Pat Ross.\r\r\section* References\r\r#\ref [CD94] Steve Cook and John Daniels. Designing Object Systems: Object-Oriented Modelling with Syntropy. Prentice Hall, 1994.\r#\r\ref [1] R. Duke, G. Rose and G. Smith. Object-Z: A Specification Language Advocated for the Description of Standards. SVRC Technical Report 94-45. The Software Verification Research Centre, University of Queensland, Australia.\r\r\ref [2] John V. Guttag, James J. Horning, and Andres Modet. Report on the Larch Shared Language: Version 2.3. Technical Report 58, Compaq Systems Research Center, Palo Alto, CA, 1990.\r\r#\ref [Hal90] Anthony Hall. Using Z as a Specification Calculus for Object-Oriented Systems. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, eds., VDM and Z: Formal Methods in Software Development, Lecture Notes in Computer Science, Volume 428, pp. 290\96381, Springer-Verlag, New York, 1990.\r#\r\ref [3] Daniel Jackson. Automating first-order relational logic. Proc. ACM SIGSOFT Conf. Foundations of Software Engineering. San Diego, November 2000.\r\r\ref [4] Daniel Jackson. Alloy: A Lightweight Object Modelling Notation. To appear, ACM Transactions on Software Engineering and Methodology, October 2001.\r\r\ref [5] Daniel Jackson, Ian Schechter and Ilya Shlyakhter. Alcoa: the Alloy Constraint Analyzer. Proc. International Conference on Software Engineering, Limerick, Ireland, June 2000.\r\r\ref [6] Daniel Jackson and Jeannette Wing. Lightweight Formal Methods. In: H. Saiedian (ed.), An Invitation to Formal Methods. IEEE Computer, 29(4):16-30, April 1996. \r\r\ref [7] Michael Jackson. Software Requirements and Specifications: A Lexicon of Practice, Principles and Prejudices. Addison-Wesley, 1995.\r\r\ref [8] Cliff Jones. Systematic Software Development Using VDM. Second edition, Prentice Hall, 1990.\r\r\ref [9] Kathleen Jensen and Nicklaus Wirth. Pascal: User Manual and Report. Springer-# Verlag, 1974.\r\r\ref [10] K. Rustan M. Leino and Greg Nelson. Data abstraction and information hiding . Research Report 160, Compaq Systems Research Center, November 2000.\r\r\ref [11] Hector Levesque, Fiora Pirri, and Ray Reiter. Foundations for the Situation Calculus. Linköping Electronic Articles in Computer and Information Science, ISSN 1401-9841, Vol. 3(1998), Nr. 018.\r\r\ref [12] Robin Milner, Mads Tofte and Robert Harper. The Definition of Standard ML. MIT Press, 1990.\r\r\ref [13] S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS Language Reference. Computer Science Laboratory, SRI International, Menlo Park, CA, September 1999.\r\r\ref [14] J. Michael Spivey. The Z Notation: A Reference Manual. Second edition, Prentice Hall, 1992.\r\r\ref [15] Ian Toyn et al. Formal Specification---Z Notation---Syntax, Type and Semantics. Consensus Working Draft 2.6 of the Z Standards Panel BSI Panel IST/5/-/19/2 (Z Notation). August 24, 2000.\r\r\ref [16] Jim Woodcock and Jim Davies. Using Z: Specification, Refinement and Proof. Prentice Hall, 1996.\r\r\ref [17] Jos Warmer and Anneke Kleppe. The Object Constraint Language: Precise Modeling with UML. Addison Wesley, 1999.\r\r\ref [18] Pamela Zave and Michael Jackson. Conjunction as Composition. ACM Transactions on Software Engineering and Methodology II(4): 379--411, October 1993.\r
\ No newline at end of file
}
}
- public add( Action a, int list, Action c ) {
+ public add( Action a, int list ) {
actions[list].addFirst( a );
}
}
public StandardEngine( Gen gen ) {
Engine();
- Action c = new Action( gen );
-
Action a = new AntherAction( gen );
- add( a, 0, c );
- //add( a, 1, c );
-
-
+ add( a, 0 );
+ //add( a, 1 );
+
Action b = new AntherAction( gen );
- add( b, 0, c );
-
+ add( b, 0 );
}
}
projects / IRC.git / commitdiff