'module' Keyword.Namespace ' ' Text 'examples' Name '/' Operator 'systems' Name '/' Operator 'views' Name '\n' Text '\n' Text "/*\n * Model of views in object-oriented programming.\n *\n * Two object references, called the view and the backing,\n * are related by a view mechanism when changes to the\n * backing are automatically propagated to the view. Note\n * that the state of a view need not be a projection of the\n * state of the backing; the keySet method of Map, for\n * example, produces two view relationships, and for the\n * one in which the map is modified by changes to the key\n * set, the value of the new map cannot be determined from\n * the key set. Note that in the iterator view mechanism,\n * the iterator is by this definition the backing object,\n * since changes are propagated from iterator to collection\n * and not vice versa. Oddly, a reference may be a view of\n * more than one backing: there can be two iterators on the\n * same collection, eg. A reference cannot be a view under\n * more than one view type.\n *\n * A reference is made dirty when it is a backing for a view\n * with which it is no longer related by the view invariant.\n * This usually happens when a view is modified, either\n * directly or via another backing. For example, changing a\n * collection directly when it has an iterator invalidates\n * it, as does changing the collection through one iterator\n * when there are others.\n *\n * More work is needed if we want to model more closely the\n * failure of an iterator when its collection is invalidated.\n *\n * As a terminological convention, when there are two\n * complementary view relationships, we will give them types\n * t and t'. For example, KeySetView propagates from map to\n * set, and KeySetView' propagates from set to map.\n *\n * author: Daniel Jackson\n */" Comment.Multiline '\n' Text '\n' Text 'open' Keyword.Namespace ' ' Text 'util' Name '/' Operator 'ordering' Name '[' Operator 'State' Name ']' Operator ' ' Text 'as' Keyword ' ' Text 'so' Name '\n' Text 'open' Keyword.Namespace ' ' Text 'util' Name '/' Operator 'relation' Name ' ' Text 'as' Keyword ' ' Text 'rel' Name '\n' Text '\n' Text 'sig' Keyword.Declaration ' ' Text 'Ref' Name ' ' Text '{' Operator '}' Operator '\n' Text 'sig' Keyword.Declaration ' ' Text 'Object' Name ' ' Text '{' Operator '}' Operator '\n' Text '\n' Text '-- t->b->v in views when v is view of type t of backing b' Comment.Single '\n' Text '-- dirty contains refs that have been invalidated' Comment.Single '\n' Text 'sig' Keyword.Declaration ' ' Text 'State' Name ' ' Text '{' Operator '\n' Text ' ' Text 'refs' Name ':' Punctuation ' ' Text 'set' Keyword ' ' Text 'Ref' Name ',' Punctuation '\n' Text ' ' Text 'obj' Name ':' Punctuation ' ' Text 'refs' Name ' ' Text '->' Operator ' ' Text 'one' Keyword ' ' Text 'Object' Name ',' Punctuation '\n' Text ' ' Text 'views' Name ':' Punctuation ' ' Text 'ViewType' Name ' ' Text '->' Operator ' ' Text 'refs' Name ' ' Text '->' Operator ' ' Text 'refs' Name ',' Punctuation '\n' Text ' ' Text 'dirty' Name ':' Punctuation ' ' Text 'set' Keyword ' ' Text 'refs' Name '\n' Text '-- , anyviews: Ref -> Ref -- for visualization' Comment.Single '\n' Text ' ' Text '}' Operator '\n' Text '-- {anyviews = ViewType.views}' Comment.Single '\n' Text '\n' Text 'sig' Keyword.Declaration ' ' Text 'Map' Name ' ' Text 'extends' Keyword ' ' Text 'Object' Name ' ' Text '{' Operator '\n' Text ' ' Text 'keys' Name ':' Punctuation ' ' Text 'set' Keyword ' ' Text 'Ref' Name ',' Punctuation '\n' Text ' ' Text 'map' Name ':' Punctuation ' ' Text 'keys' Name ' ' Text '->' Operator ' ' Text 'one' Keyword ' ' Text 'Ref' Name '\n' Text ' ' Text '}' Operator '{' Operator 'all' Keyword ' ' Text 's' Name ':' Punctuation ' ' Text 'State' Name ' ' Text '|' Operator ' ' Text 'keys' Name ' ' Text '+' Operator ' ' Text 'Ref' Name '.' Operator 'map' Name ' ' Text 'in' Operator.Word ' ' Text 's' Name '.' Operator 'refs' Name '}' Operator '\n' Text 'sig' Keyword.Declaration ' ' Text 'MapRef' Name ' ' Text 'extends' Keyword ' ' Text 'Ref' Name ' ' Text '{' Operator '}' Operator '\n' Text 'fact' Keyword ' ' Text '{' Operator 'State' Name '.' Operator 'obj' Name '[' Operator 'MapRef' Name ']' Operator ' ' Text 'in' Operator.Word ' ' Text 'Map' Name '}' Operator '\n' Text '\n' Text 'sig' Keyword.Declaration ' ' Text 'Iterator' Name ' ' Text 'extends' Keyword ' ' Text 'Object' Name ' ' Text '{' Operator '\n' Text ' ' Text 'left' Name ',' Punctuation ' ' Text 'done' Name ':' Punctuation ' ' Text 'set' Keyword ' ' Text 'Ref' Name ',' Punctuation '\n' Text ' ' Text 'lastRef' Name ':' Punctuation ' ' Text 'lone' Keyword ' ' Text 'done' Name '\n' Text ' ' Text '}' Operator '{' Operator 'all' Keyword ' ' Text 's' Name ':' Punctuation ' ' Text 'State' Name ' ' Text '|' Operator ' ' Text 'done' Name ' ' Text '+' Operator ' ' Text 'left' Name ' ' Text '+' Operator ' ' Text 'lastRef' Name ' ' Text 'in' Operator.Word ' ' Text 's' Name '.' Operator 'refs' Name '}' Operator '\n' Text 'sig' Keyword.Declaration ' ' Text 'IteratorRef' Name ' ' Text 'extends' Keyword ' ' Text 'Ref' Name ' ' Text '{' Operator '}' Operator '\n' Text 'fact' Keyword ' ' Text '{' Operator 'State' Name '.' Operator 'obj' Name '[' Operator 'IteratorRef' Name ']' Operator ' ' Text 'in' Operator.Word ' ' Text 'Iterator' Name '}' Operator '\n' Text '\n' Text 'sig' Keyword.Declaration ' ' Text 'Set' Name ' ' Text 'extends' Keyword ' ' Text 'Object' Name ' ' Text '{' Operator '\n' Text ' ' Text 'elts' Name ':' Punctuation ' ' Text 'set' Keyword ' ' Text 'Ref' Name '\n' Text ' ' Text '}' Operator '{' Operator 'all' Keyword ' ' Text 's' Name ':' Punctuation ' ' Text 'State' Name ' ' Text '|' Operator ' ' Text 'elts' Name ' ' Text 'in' Operator.Word ' ' Text 's' Name '.' Operator 'refs' Name '}' Operator '\n' Text 'sig' Keyword.Declaration ' ' Text 'SetRef' Name ' ' Text 'extends' Keyword ' ' Text 'Ref' Name ' ' Text '{' Operator '}' Operator '\n' Text 'fact' Keyword ' ' Text '{' Operator 'State' Name '.' Operator 'obj' Name '[' Operator 'SetRef' Name ']' Operator ' ' Text 'in' Operator.Word ' ' Text 'Set' Name '}' Operator '\n' Text '\n' Text 'abstract' Keyword ' ' Text 'sig' Keyword.Declaration ' ' Text 'ViewType' Name ' ' Text '{' Operator '}' Operator '\n' Text 'one' Keyword ' ' Text 'sig' Keyword.Declaration ' ' Text 'KeySetView' Name ',' Punctuation ' ' Text "KeySetView'" Name ',' Punctuation ' ' Text 'IteratorView' Name ' ' Text 'extends' Keyword ' ' Text 'ViewType' Name ' ' Text '{' Operator '}' Operator '\n' Text 'fact' Keyword ' ' Text 'ViewTypes' Name ' ' Text '{' Operator '\n' Text ' ' Text 'State' Name '.' Operator 'views' Name '[' Operator 'KeySetView' Name ']' Operator ' ' Text 'in' Operator.Word ' ' Text 'MapRef' Name ' ' Text '->' Operator ' ' Text 'SetRef' Name '\n' Text ' ' Text 'State' Name '.' Operator 'views' Name '[' Operator "KeySetView'" Name ']' Operator ' ' Text 'in' Operator.Word ' ' Text 'SetRef' Name ' ' Text '->' Operator ' ' Text 'MapRef' Name '\n' Text ' ' Text 'State' Name '.' Operator 'views' Name '[' Operator 'IteratorView' Name ']' Operator ' ' Text 'in' Operator.Word ' ' Text 'IteratorRef' Name ' ' Text '->' Operator ' ' Text 'SetRef' Name '\n' Text ' ' Text 'all' Keyword ' ' Text 's' Name ':' Punctuation ' ' Text 'State' Name ' ' Text '|' Operator ' ' Text 's' Name '.' Operator 'views' Name '[' Operator 'KeySetView' Name ']' Operator ' ' Text '=' Operator ' ' Text '~' Operator '(' Operator 's' Name '.' Operator 'views' Name '[' Operator "KeySetView'" Name ']' Operator ')' Operator '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text "/**\n * mods is refs modified directly or by view mechanism\n * doesn't handle possibility of modifying an object and its view at once?\n * should we limit frame conds to non-dirty refs?\n */" Comment.Multiline '\n' Text 'pred' Keyword ' ' Text 'modifies' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ':' Punctuation ' ' Text 'State' Name ',' Punctuation ' ' Text 'rs' Name ':' Punctuation ' ' Text 'set' Keyword ' ' Text 'Ref' Name ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text 'let' Keyword ' ' Text 'vr' Name ' ' Text '=' Operator ' ' Text 'pre' Name '.' Operator 'views' Name '[' Operator 'ViewType' Name ']' Operator ',' Punctuation ' ' Text 'mods' Name ' ' Text '=' Operator ' ' Text 'rs' Name '.' Operator '*' Operator 'vr' Name ' ' Text '{' Operator '\n' Text ' ' Text 'all' Keyword ' ' Text 'r' Name ':' Punctuation ' ' Text 'pre' Name '.' Operator 'refs' Name ' ' Text '-' Operator ' ' Text 'mods' Name ' ' Text '|' Operator ' ' Text 'pre' Name '.' Operator 'obj' Name '[' Operator 'r' Name ']' Operator ' ' Text '=' Operator ' ' Text 'post' Name '.' Operator 'obj' Name '[' Operator 'r' Name ']' Operator '\n' Text ' ' Text 'all' Keyword ' ' Text 'b' Name ':' Punctuation ' ' Text 'mods' Name ',' Punctuation ' ' Text 'v' Name ':' Punctuation ' ' Text 'pre' Name '.' Operator 'refs' Name ',' Punctuation ' ' Text 't' Name ':' Punctuation ' ' Text 'ViewType' Name ' ' Text '|' Operator '\n' Text ' ' Text 'b' Name '->' Operator 'v' Name ' ' Text 'in' Operator.Word ' ' Text 'pre' Name '.' Operator 'views' Name '[' Operator 't' Name ']' Operator ' ' Text '=' Operator '>' Operator ' ' Text 'viewFrame' Name ' ' Text '[' Operator 't' Name ',' Punctuation ' ' Text 'pre' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text 'post' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text 'post' Name '.' Operator 'obj' Name '[' Operator 'b' Name ']' Operator ']' Operator '\n' Text ' ' Text 'post' Name '.' Operator 'dirty' Name ' ' Text '=' Operator ' ' Text 'pre' Name '.' Operator 'dirty' Name ' ' Text '+' Operator '\n' Text ' ' Text '{' Operator 'b' Name ':' Punctuation ' ' Text 'pre' Name '.' Operator 'refs' Name ' ' Text '|' Operator ' ' Text 'some' Keyword ' ' Text 'v' Name ':' Punctuation ' ' Text 'Ref' Name ',' Punctuation ' ' Text 't' Name ':' Punctuation ' ' Text 'ViewType' Name ' ' Text '|' Operator '\n' Text ' ' Text 'b' Name '->' Operator 'v' Name ' ' Text 'in' Operator.Word ' ' Text 'pre' Name '.' Operator 'views' Name '[' Operator 't' Name ']' Operator ' ' Text '&&' Operator ' ' Text '!' Operator 'viewFrame' Name ' ' Text '[' Operator 't' Name ',' Punctuation ' ' Text 'pre' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text 'post' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text 'post' Name '.' Operator 'obj' Name '[' Operator 'b' Name ']' Operator ']' Operator '\n' Text ' ' Text '}' Operator '\n' Text ' ' Text '}' Operator '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text 'pred' Keyword ' ' Text 'allocates' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ':' Punctuation ' ' Text 'State' Name ',' Punctuation ' ' Text 'rs' Name ':' Punctuation ' ' Text 'set' Keyword ' ' Text 'Ref' Name ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text 'no' Keyword ' ' Text 'rs' Name ' ' Text '&' Operator ' ' Text 'pre' Name '.' Operator 'refs' Name '\n' Text ' ' Text 'post' Name '.' Operator 'refs' Name ' ' Text '=' Operator ' ' Text 'pre' Name '.' Operator 'refs' Name ' ' Text '+' Operator ' ' Text 'rs' Name '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text "/** \n * models frame condition that limits change to view object from v to v' when backing object changes to b'\n */" Comment.Multiline '\n' Text 'pred' Keyword ' ' Text 'viewFrame' Name ' ' Text '[' Operator 't' Name ':' Punctuation ' ' Text 'ViewType' Name ',' Punctuation ' ' Text 'v' Name ',' Punctuation ' ' Text "v'" Name ',' Punctuation ' ' Text "b'" Name ':' Punctuation ' ' Text 'Object' Name ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text 't' Name ' ' Text 'in' Operator.Word ' ' Text 'KeySetView' Name ' ' Text '=' Operator '>' Operator ' ' Text "v'" Name '.' Operator 'elts' Name ' ' Text '=' Operator ' ' Text 'dom' Name ' ' Text '[' Operator "b'" Name '.' Operator 'map' Name ']' Operator '\n' Text ' ' Text 't' Name ' ' Text 'in' Operator.Word ' ' Text "KeySetView'" Name ' ' Text '=' Operator '>' Operator ' ' Text "b'" Name '.' Operator 'elts' Name ' ' Text '=' Operator ' ' Text 'dom' Name ' ' Text '[' Operator "v'" Name '.' Operator 'map' Name ']' Operator '\n' Text ' ' Text 't' Name ' ' Text 'in' Operator.Word ' ' Text "KeySetView'" Name ' ' Text '=' Operator '>' Operator ' ' Text '(' Operator "b'" Name '.' Operator 'elts' Name ')' Operator ' ' Text '<' Operator ':' Punctuation ' ' Text '(' Operator 'v' Name '.' Operator 'map' Name ')' Operator ' ' Text '=' Operator ' ' Text '(' Operator "b'" Name '.' Operator 'elts' Name ')' Operator ' ' Text '<' Operator ':' Punctuation ' ' Text '(' Operator "v'" Name '.' Operator 'map' Name ')' Operator '\n' Text ' ' Text 't' Name ' ' Text 'in' Operator.Word ' ' Text 'IteratorView' Name ' ' Text '=' Operator '>' Operator ' ' Text "v'" Name '.' Operator 'elts' Name ' ' Text '=' Operator ' ' Text "b'" Name '.' Operator 'left' Name ' ' Text '+' Operator ' ' Text "b'" Name '.' Operator 'done' Name '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text 'pred' Keyword ' ' Text 'MapRef' Name '.' Operator 'keySet' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ':' Punctuation ' ' Text 'State' Name ',' Punctuation ' ' Text 'setRefs' Name ':' Punctuation ' ' Text 'SetRef' Name ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text 'post' Name '.' Operator 'obj' Name '[' Operator 'setRefs' Name ']' Operator '.' Operator 'elts' Name ' ' Text '=' Operator ' ' Text 'dom' Name ' ' Text '[' Operator 'pre' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator '.' Operator 'map' Name ']' Operator '\n' Text ' ' Text 'modifies' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ',' Punctuation ' ' Text 'none' Keyword.Constant ']' Operator '\n' Text ' ' Text 'allocates' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ',' Punctuation ' ' Text 'setRefs' Name ']' Operator '\n' Text ' ' Text 'post' Name '.' Operator 'views' Name ' ' Text '=' Operator ' ' Text 'pre' Name '.' Operator 'views' Name ' ' Text '+' Operator ' ' Text 'KeySetView' Name '->' Operator 'this' Keyword '->' Operator 'setRefs' Name ' ' Text '+' Operator ' ' Text "KeySetView'" Name '->' Operator 'setRefs' Name '->' Operator 'this' Keyword '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text 'pred' Keyword ' ' Text 'MapRef' Name '.' Operator 'put' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ':' Punctuation ' ' Text 'State' Name ',' Punctuation ' ' Text 'k' Name ',' Punctuation ' ' Text 'v' Name ':' Punctuation ' ' Text 'Ref' Name ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text 'post' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator '.' Operator 'map' Name ' ' Text '=' Operator ' ' Text 'pre' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator '.' Operator 'map' Name ' ' Text '++' Operator ' ' Text 'k' Name '->' Operator 'v' Name '\n' Text ' ' Text 'modifies' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ',' Punctuation ' ' Text 'this' Keyword ']' Operator '\n' Text ' ' Text 'allocates' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ',' Punctuation ' ' Text 'none' Keyword.Constant ']' Operator '\n' Text ' ' Text 'post' Name '.' Operator 'views' Name ' ' Text '=' Operator ' ' Text 'pre' Name '.' Operator 'views' Name '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text 'pred' Keyword ' ' Text 'SetRef' Name '.' Operator 'iterator' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ':' Punctuation ' ' Text 'State' Name ',' Punctuation ' ' Text 'iterRef' Name ':' Punctuation ' ' Text 'IteratorRef' Name ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text 'let' Keyword ' ' Text 'i' Name ' ' Text '=' Operator ' ' Text 'post' Name '.' Operator 'obj' Name '[' Operator 'iterRef' Name ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text 'i' Name '.' Operator 'left' Name ' ' Text '=' Operator ' ' Text 'pre' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator '.' Operator 'elts' Name '\n' Text ' ' Text 'no' Keyword ' ' Text 'i' Name '.' Operator 'done' Name ' ' Text '+' Operator ' ' Text 'i' Name '.' Operator 'lastRef' Name '\n' Text ' ' Text '}' Operator '\n' Text ' ' Text 'modifies' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation 'post' Name ',' Punctuation 'none' Keyword.Constant ']' Operator '\n' Text ' ' Text 'allocates' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ',' Punctuation ' ' Text 'iterRef' Name ']' Operator '\n' Text ' ' Text 'post' Name '.' Operator 'views' Name ' ' Text '=' Operator ' ' Text 'pre' Name '.' Operator 'views' Name ' ' Text '+' Operator ' ' Text 'IteratorView' Name '->' Operator 'iterRef' Name '->' Operator 'this' Keyword '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text 'pred' Keyword ' ' Text 'IteratorRef' Name '.' Operator 'remove' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ':' Punctuation ' ' Text 'State' Name ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text 'let' Keyword ' ' Text 'i' Name ' ' Text '=' Operator ' ' Text 'pre' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator ',' Punctuation ' ' Text "i'" Name ' ' Text '=' Operator ' ' Text 'post' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text "i'" Name '.' Operator 'left' Name ' ' Text '=' Operator ' ' Text 'i' Name '.' Operator 'left' Name '\n' Text ' ' Text "i'" Name '.' Operator 'done' Name ' ' Text '=' Operator ' ' Text 'i' Name '.' Operator 'done' Name ' ' Text '-' Operator ' ' Text 'i' Name '.' Operator 'lastRef' Name '\n' Text ' ' Text 'no' Keyword ' ' Text "i'" Name '.' Operator 'lastRef' Name '\n' Text ' ' Text '}' Operator '\n' Text ' ' Text 'modifies' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation 'post' Name ',' Punctuation 'this' Keyword ']' Operator '\n' Text ' ' Text 'allocates' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ',' Punctuation ' ' Text 'none' Keyword.Constant ']' Operator '\n' Text ' ' Text 'pre' Name '.' Operator 'views' Name ' ' Text '=' Operator ' ' Text 'post' Name '.' Operator 'views' Name '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text 'pred' Keyword ' ' Text 'IteratorRef' Name '.' Operator 'next' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ':' Punctuation ' ' Text 'State' Name ',' Punctuation ' ' Text 'ref' Name ':' Punctuation ' ' Text 'Ref' Name ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text 'let' Keyword ' ' Text 'i' Name ' ' Text '=' Operator ' ' Text 'pre' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator ',' Punctuation ' ' Text "i'" Name ' ' Text '=' Operator ' ' Text 'post' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text 'ref' Name ' ' Text 'in' Operator.Word ' ' Text 'i' Name '.' Operator 'left' Name '\n' Text ' ' Text "i'" Name '.' Operator 'left' Name ' ' Text '=' Operator ' ' Text 'i' Name '.' Operator 'left' Name ' ' Text '-' Operator ' ' Text 'ref' Name '\n' Text ' ' Text "i'" Name '.' Operator 'done' Name ' ' Text '=' Operator ' ' Text 'i' Name '.' Operator 'done' Name ' ' Text '+' Operator ' ' Text 'ref' Name '\n' Text ' ' Text "i'" Name '.' Operator 'lastRef' Name ' ' Text '=' Operator ' ' Text 'ref' Name '\n' Text ' ' Text '}' Operator '\n' Text ' ' Text 'modifies' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ',' Punctuation ' ' Text 'this' Keyword ']' Operator '\n' Text ' ' Text 'allocates' Name ' ' Text '[' Operator 'pre' Name ',' Punctuation ' ' Text 'post' Name ',' Punctuation ' ' Text 'none' Keyword.Constant ']' Operator '\n' Text ' ' Text 'pre' Name '.' Operator 'views' Name ' ' Text '=' Operator ' ' Text 'post' Name '.' Operator 'views' Name '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text 'pred' Keyword ' ' Text 'IteratorRef' Name '.' Operator 'hasNext' Name ' ' Text '[' Operator 's' Name ':' Punctuation ' ' Text 'State' Name ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text 'some' Keyword ' ' Text 's' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator '.' Operator 'left' Name '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text 'assert' Keyword ' ' Text 'zippishOK' Name ' ' Text '{' Operator '\n' Text ' ' Text 'all' Keyword '\n' Text ' ' Text 'ks' Name ',' Punctuation ' ' Text 'vs' Name ':' Punctuation ' ' Text 'SetRef' Name ',' Punctuation '\n' Text ' ' Text 'm' Name ':' Punctuation ' ' Text 'MapRef' Name ',' Punctuation '\n' Text ' ' Text 'ki' Name ',' Punctuation ' ' Text 'vi' Name ':' Punctuation ' ' Text 'IteratorRef' Name ',' Punctuation '\n' Text ' ' Text 'k' Name ',' Punctuation ' ' Text 'v' Name ':' Punctuation ' ' Text 'Ref' Name ' ' Text '|' Operator '\n' Text ' ' Text 'let' Keyword ' ' Text 's0' Name '=' Operator 'so' Name '/' Operator 'first' Name ',' Punctuation '\n' Text ' ' Text 's1' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's0' Name ']' Operator ',' Punctuation '\n' Text ' ' Text 's2' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's1' Name ']' Operator ',' Punctuation '\n' Text ' ' Text 's3' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's2' Name ']' Operator ',' Punctuation '\n' Text ' ' Text 's4' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's3' Name ']' Operator ',' Punctuation '\n' Text ' ' Text 's5' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's4' Name ']' Operator ',' Punctuation '\n' Text ' ' Text 's6' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's5' Name ']' Operator ',' Punctuation '\n' Text ' ' Text 's7' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's6' Name ']' Operator ' ' Text '|' Operator '\n' Text ' ' Text '(' Operator '{' Operator '\n' Text ' ' Text 'precondition' Name ' ' Text '[' Operator 's0' Name ',' Punctuation ' ' Text 'ks' Name ',' Punctuation ' ' Text 'vs' Name ',' Punctuation ' ' Text 'm' Name ']' Operator '\n' Text ' ' Text 'no' Keyword ' ' Text 's0' Name '.' Operator 'dirty' Name '\n' Text ' ' Text 'ks' Name '.' Operator 'iterator' Name ' ' Text '[' Operator 's0' Name ',' Punctuation ' ' Text 's1' Name ',' Punctuation ' ' Text 'ki' Name ']' Operator '\n' Text ' ' Text 'vs' Name '.' Operator 'iterator' Name ' ' Text '[' Operator 's1' Name ',' Punctuation ' ' Text 's2' Name ',' Punctuation ' ' Text 'vi' Name ']' Operator '\n' Text ' ' Text 'ki' Name '.' Operator 'hasNext' Name ' ' Text '[' Operator 's2' Name ']' Operator '\n' Text ' ' Text 'vi' Name '.' Operator 'hasNext' Name ' ' Text '[' Operator 's2' Name ']' Operator '\n' Text ' ' Text 'ki' Name '.' Operator 'this' Keyword '/' Operator 'next' Name ' ' Text '[' Operator 's2' Name ',' Punctuation ' ' Text 's3' Name ',' Punctuation ' ' Text 'k' Name ']' Operator '\n' Text ' ' Text 'vi' Name '.' Operator 'this' Keyword '/' Operator 'next' Name ' ' Text '[' Operator 's3' Name ',' Punctuation ' ' Text 's4' Name ',' Punctuation ' ' Text 'v' Name ']' Operator '\n' Text ' ' Text 'm' Name '.' Operator 'put' Name ' ' Text '[' Operator 's4' Name ',' Punctuation ' ' Text 's5' Name ',' Punctuation ' ' Text 'k' Name ',' Punctuation ' ' Text 'v' Name ']' Operator '\n' Text ' ' Text 'ki' Name '.' Operator 'remove' Name ' ' Text '[' Operator 's5' Name ',' Punctuation ' ' Text 's6' Name ']' Operator '\n' Text ' ' Text 'vi' Name '.' Operator 'remove' Name ' ' Text '[' Operator 's6' Name ',' Punctuation ' ' Text 's7' Name ']' Operator '\n' Text ' ' Text '}' Operator ' ' Text '=' Operator '>' Operator ' ' Text 'no' Keyword ' ' Text 'State' Name '.' Operator 'dirty' Name ')' Operator '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text 'pred' Keyword ' ' Text 'precondition' Name ' ' Text '[' Operator 'pre' Name ':' Punctuation ' ' Text 'State' Name ',' Punctuation ' ' Text 'ks' Name ',' Punctuation ' ' Text 'vs' Name ',' Punctuation ' ' Text 'm' Name ':' Punctuation ' ' Text 'Ref' Name ']' Operator ' ' Text '{' Operator '\n' Text ' ' Text '// all these conditions and other errors discovered in scope of 6 but 8,3' Comment.Single '\n' Text ' ' Text '// in initial state, must have view invariants hold' Comment.Single '\n' Text ' ' Text '(' Operator 'all' Keyword ' ' Text 't' Name ':' Punctuation ' ' Text 'ViewType' Name ',' Punctuation ' ' Text 'b' Name ',' Punctuation ' ' Text 'v' Name ':' Punctuation ' ' Text 'pre' Name '.' Operator 'refs' Name ' ' Text '|' Operator '\n' Text ' ' Text 'b' Name '->' Operator 'v' Name ' ' Text 'in' Operator.Word ' ' Text 'pre' Name '.' Operator 'views' Name '[' Operator 't' Name ']' Operator ' ' Text '=' Operator '>' Operator ' ' Text 'viewFrame' Name ' ' Text '[' Operator 't' Name ',' Punctuation ' ' Text 'pre' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text 'pre' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text 'pre' Name '.' Operator 'obj' Name '[' Operator 'b' Name ']' Operator ']' Operator ')' Operator '\n' Text ' ' Text '// sets are not aliases' Comment.Single '\n' Text '-- ks != vs' Comment.Single '\n' Text ' ' Text '// sets are not views of map' Comment.Single '\n' Text '-- no (ks+vs)->m & ViewType.pre.views' Comment.Single '\n' Text ' ' Text '// no iterator currently on either set' Comment.Single '\n' Text '-- no Ref->(ks+vs) & ViewType.pre.views' Comment.Single '\n' Text ' ' Text '}' Operator '\n' Text '\n' Text 'check' Keyword ' ' Text 'zippishOK' Name ' ' Text 'for' Keyword ' ' Text '6' Literal.Number.Integer ' ' Text 'but' Keyword ' ' Text '8' Literal.Number.Integer ' ' Text 'State' Name ',' Punctuation ' ' Text '3' Literal.Number.Integer ' ' Text 'ViewType' Name ' ' Text 'expect' Keyword ' ' Text '1' Literal.Number.Integer '\n' Text '\n' Text '/** \n * experiment with controlling heap size\n */' Comment.Multiline '\n' Text 'fact' Keyword ' ' Text '{' Operator 'all' Keyword ' ' Text 's' Name ':' Punctuation ' ' Text 'State' Name ' ' Text '|' Operator ' ' Text '#' Operator 's' Name '.' Operator 'obj' Name ' ' Text '<' Operator ' ' Text '5' Literal.Number.Integer '}' Operator '\n' Text