BSD 4_3 development
authorCSRG <csrg@ucbvax.Berkeley.EDU>
Sun, 10 Mar 1985 22:21:47 +0000 (14:21 -0800)
committerCSRG <csrg@ucbvax.Berkeley.EDU>
Sun, 10 Mar 1985 22:21:47 +0000 (14:21 -0800)
Work on file usr/contrib/B/doc/Description1

Synthesized-from: CSRG/cd1/4.3

usr/contrib/B/doc/Description1 [new file with mode: 0644]

diff --git a/usr/contrib/B/doc/Description1 b/usr/contrib/B/doc/Description1
new file mode 100644 (file)
index 0000000..fc1d2b0
--- /dev/null
@@ -0,0 +1,1351 @@
+.\" Copyright (c) Stichting Mathematisch Centrum, Amsterdam, 1984.
+.Du START
+.sp 1
+.in 0
+.ce 99
+DESCRIPTION OF B
+
+Lambert Meertens
+Steven Pemberton
+
+CWI
+Amsterdam
+
+April 1984
+.ce 0
+.Co
+.ds Sn Contents
+.bp
+.in 15
+.nf
+.ps 8
+.vs 10
+CONTENTS
+
+0.\0INTRODUCTION
+1.\0VALUES IN B
+2.\0SYNTAX DESCRIPTION METHOD
+3.\0REPRESENTATIONS
+4.\0UNITS
+        4.1.\0HOW-TO-UNITS
+        4.2.\0YIELD-UNITS
+        4.3.\0TEST-UNITS
+        4.4.\0REFINEMENTS
+        4.5.\0COMMAND-SUITES
+5.\0COMMANDS
+        5.1.\0\0SIMPLE-COMMANDS
+                5.1.1.\0\0CHECK-COMMANDS
+                5.1.2.\0\0WRITE-COMMANDS
+                5.1.3.\0\0READ-COMMANDS
+                5.1.4.\0\0PUT-COMMANDS
+                5.1.5.\0\0DRAW-COMMANDS
+                5.1.6.\0\0CHOOSE-COMMANDS
+                5.1.7.\0\0SET-RANDOM-COMMANDS
+                5.1.8.\0\0REMOVE-COMMANDS
+                5.1.9.\0\0INSERT-COMMANDS
+                5.1.10.\0DELETE-COMMANDS
+                5.1.11.\0QUIT-COMMAND
+                5.1.12.\0RETURN-COMMANDS
+                5.1.13.\0SUCCEED-COMMAND
+                5.1.14.\0FAIL-COMMAND
+                5.1.15.\0USER-DEFINED-COMMANDS
+                5.1.16.\0REFINED-COMMANDS
+        5.2.\0CONTROL-COMMANDS
+                5.2.1.\0IF-COMMANDS
+                5.2.2.\0SELECT-COMMANDS
+                5.2.3.\0WHILE-COMMANDS
+                5.2.4.\0FOR-COMMANDS
+6.\0EXPRESSIONS, TARGETS AND TESTS
+        6.1.\0EXPRESSIONS
+                6.1.1.\0NUMERIC-CONSTANTS
+                6.1.2.\0TARGET-CONTENTS
+                6.1.3.\0TRIMMED-TEXTS
+                6.1.4.\0TABLE-SELECTIONS
+                6.1.5.\0DISPLAYS
+                6.1.6.\0FORMULAS
+                        Formulas with user-defined functions
+                        Formulas with predefined functions
+                6.1.7.\0REFINED-EXPRESSIONS
+        6.2.\0TARGETS
+                6.2.1.\0IDENTIFIERS
+                6.2.2.\0TRIMMED-TEXT-TARGETS
+                6.2.3.\0TABLE-SELECTION-TARGETS
+        6.3.\0TESTS
+                6.3.1.\0ORDER-TESTS
+                6.3.2.\0PROPOSITIONS
+                        Propositions with user-defined predicates
+                        Propositions with predefined predicates
+                6.3.3.\0REFINED-TESTS
+                6.3.4.\0CONJUNCTIONS
+                6.3.5.\0DISJUNCTIONS
+                6.3.6.\0NEGATIONS
+                6.3.7.\0QUANTIFICATIONS
+INDEX
+.ps 10
+.vs 12
+.in 0
+.ds Sn Introduction
+.bp
+.St 0 INTRODUCTION
+.fi
+.Tx
+\*B is a simple but powerful new programming language, designed for use in
+personal computing.
+(Note: the name ``\*B'' is only a temporary working title,
+and the new language bears no relation to the predecessor of
+C.)\ 
+The foremost aim in the design of \*B has been the ease of use for
+programmers who want to produce working programs without having
+to master a complex tool.
+An implementation of \*B is available from the \*B group at
+the CWI, currently only under UNIX* or its look-alikes, but soon
+(scheduled early 1985) also for the IBM-PC under MS-DOS.
+Remarks concerning the implementation appear in this description
+between double braces {{ and }}.
+.sp 0.6v
+This description of \*B originated from a text, prepared by
+the first author, for use in teaching \*B during the Fall
+term of 1982 at New York University.
+The aim is to provide a reference book for the users of \*B that is more
+accessible than the somewhat formal ``Draft Proposal'' [2].
+While it is not a text book, it should also be useful
+to people who already have ample programming
+experience and want to learn \*B.
+A text book for beginners is also available from the CWI [1].
+.sp 0.6v
+In this description we have tried to remain close to the Draft Proposal
+in order to facilitate cross-referencing. To this end, all section numbers
+from section 4 onwards are the same as in the Draft Proposal.
+However there are some changes in terminology.
+Some minor differences are
+.sp 0.6v
+.ta 2m \w'mmTYPE-TYPES-expressionmm'u \w'mmTYPE-TYPES-expressionmm'u+\w'multiple-expressionmm'u
+.nf
+\&     Draft Proposal: This description:
+.sp 0.4v
+\&     textual-display text-display
+\&     textual-body    text-body
+\&     LIST-body       optional-list-body
+\&     TABLE-body      optional-table-filler-series
+.fi
+.sp 0.6v
+But the main difference is perhaps in the treatment of ``collateral'':
+.sp 0.6v
+.nf
+\&     Draft Proposal: This description:       Examples
+.sp 0.4v
+\&     collateral-expression   expression      \*(<:a   (a, b)   a, b\*(:>
+\&     TYPE-expression single-expression       \*(<:a   (a, b)\*(:>
+\&     TYPE-TYPES-expression   multiple-expression     \*(<:             a, b\*(:>
+.fi
+.sp 0.6v
+Whereas these are purely descriptional differences,
+there are also a few differences in content.
+Where the Draft Proposal has the keyword \*(<:ALLOW\*(:>,
+\*B now has the keyword \*(<:SHARE\*(:>;
+a command \*(<:READ\*(:>\ ...\ \*(<:RAW\*(:> has been added;
+and approximate-constants may no longer consist of just an exponent-part:
+\*(<:E-1\*(:> must now be written \*(<:1E-1\*(:>.
+.sp 0.6v
+References
+.sp 0.5v
+.in +\w'[1]\ 'u
+.ti 0
+[1]\ \fIComputer Programming for Beginners, Introducing the B Language,
+Part 1\fP,
+.br
+Leo Geurts, CWI, Amsterdam, 1984
+.sp 0.5v
+.ti 0
+[2]\ \fIDraft Proposal for the B Programming Language\fP,
+.br
+Lambert Meertens, CWI, Amsterdam, 1981
+.sp 0.6v
+.in 0
+*\ \s-2Unix is a trademark of Bell Laboratories.\s0
+.fi
+.SN 1
+.bp
+.St 1 "VALUES IN \*B"
+.de tY
+.sp 1
+.ne 5
+.in \w'Compounds\0\0'u
+.ta \w'Compounds\0\0'u
+.ti 0
+\\$1\t\c
+..
+.Xx number
+.Xx exact number
+.Xx approximate number
+.Xx text
+.Xx character
+.Xx order
+.Xx compound
+.Xx field
+.Xx list
+.Xx entry
+.Xx list entry
+.Xx table
+.Xx table entry
+.Xx key
+.Xx associate
+.Tx
+\*B has two basic types of values: numbers and texts, and three ways of making
+new types of values from existing ones: compounds, lists and tables.
+The built-in functions for operating on these values are described
+in section 6.1.6 entitled ``Formulas with predefined functions''.
+.tY Numbers
+Numbers come in two kinds: exact and approximate.
+Exact numbers are rational numbers.
+For example, \*(<:1.25\*(:> = \*(<:5/4\*(:>, and \*(<:(1/3)*3\*(:> = \*(<:1\*(:>.
+There is no restriction on the size of numerator and denominator.
+Approximate numbers are implemented by whatever the hardware has to offer
+for fast but approximate arithmetic (floating point).
+.br
+The arithmetic operations and many other functions give an exact result
+when their operands are exact,
+and an approximate result otherwise,
+but the function \*(<:sin\*(:>, for example, always returns an approximate number.
+.br
+An exact number can be made approximate with the \*(<:~\*(:> function
+(e.g. \*(<:~1.25\*(:>);
+the functions \*(<:round\*(:>, \*(<:floor\*(:> and \*(<:ceiling\*(:> can be used to convert
+an approximate number to an exact one.
+.br
+Exact and approximate numbers may be mixed in arithmetic, as in \*(<:4 * atan 1\*(:>.
+.tY Texts
+Texts (strings) are composed of printable ASCII characters.
+They are variable length, and are ordered in the usual lexicographic way:
+\&\*(<:'a' < 'aa' < 'b'\*(:>.
+There is no type ``character'': a text of length one will do.
+.br
+The printable characters
+are the 95 characters represented on the lines below,
+where the blank space preceding `\*(<:!\*(:>' stands for the
+(otherwise invisible) space character:
+.Di 5
+\*(<: !"#$%&'()*+,-./0123456789:;<=>?
+@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\\]^_
+`abcdefghijklmnopqrstuvwxyz{|}~\*(:>
+.br
+.Ed
+The ordering
+on the characters is the ASCII collating order, which is the order
+in which the characters are displayed above.
+.tY Compounds
+A compound consists of a sequence of other values, its ``fields''.
+For example,
+the number \*(<:3\*(:> and the text \*(<:'xyz'\*(:> may be combined to give the
+compound \*(<:3, 'xyz'\*(:>.
+Compounds are also ordered lexicographically.
+.br
+For example, \*(<:(3, 'xyz') < (3, 'yz') < (pi, 'aaa')\*(:>.
+For this to be meaningful, the compounds that are compared must
+be of the same type.
+This means that they have the
+same number of fields, and that corresponding fields are of the same type.
+.br
+The only way to obtain the individual fields of a compound is to put it
+in a multiple-target with the right number of components, as in
+.Di 1
+\*(<:PUT name IN last'name, first'name, middle'name\*(:>.
+.Ed
+.tY Lists
+A list is a \fIsorted\fP sequence of values, its ``entries''.
+All entries of a list must be of the same type, and this determines
+the type of the list.
+The length of a list may vary without influencing its type.
+When an entry is inserted in a list (with an \*(<:INSERT\*(:> command), it is automatically
+inserted in the list in the proper position in the sorting order.
+A list may contain duplicates of the same entry.
+Entries may be removed with the \*(<:REMOVE\*(:> command.
+Again, lists themselves are ordered lexicographically.
+.tY Tables
+A table consists of a (sorted) sequence of ``table entries''.
+Each table entry is a pair of two values: a \fIkey\fP and an \fIassociate\fP.
+All keys of a table must be of the same type; similarly, all associates must
+also be of the same type (but that type may be different to
+that of the keys).
+A table may not contain duplicate keys.
+If \*(<:k\*(:> is a key of the table \*(<:t\*(:>, then \*(<:t[k]\*(:>
+gives the associate corresponding to \*(<:k\*(:>.
+New entries can be made, or existing entries modified, by putting the
+associate value in the table after selecting with the key value, as
+in \*(<:PUT a IN t[k]\*(:>.
+Entries can be deleted with the \*(<:DELETE\*(:> command, as in \*(<:DELETE t[k]\*(:>.
+The ordering is again lexicographic.
+.St 2 "SYNTAX DESCRIPTION METHOD"
+.Tx
+The syntax of \*B is given in the following form:
+each rule starts with the name of the thing being defined followed by a colon;
+following this are one or more alternatives,
+each marked with a \(bu in front.
+Each alternative is composed of symbols that stand for
+themselves, or the names of other rules.
+These other rules are then defined elsewhere in the grammar,
+or possibly in the same rule.
+As an example, here is a simple grammar for a small part of English:
+.Sy  4
+.Pn  sentence 3
+.Al
+declarative
+.Al
+declarative \*(<:,\*(:> connective\0sentence
+.Pn  declarative 3
+.Al
+collective-noun\0verb\0collective-noun
+.Al
+collective-noun \*(<:do not\*(:> verb\0collective-noun
+.Pn collective-noun 2
+.Al
+\*(<:cats\*(:>
+.Al
+\*(<:dogs\*(:>
+.Al
+\*(<:people\*(:>
+.Al
+\*(<:the police\*(:>
+.Pn verb 2
+.Al
+\*(<:love\*(:>
+.Al
+\*(<:hate\*(:>
+.Al
+\*(<:eat\*(:>
+.Al
+\*(<:hassle\*(:>
+.Pn connective 2
+.Al
+\*(<:and\*(:>
+.Al
+\*(<:but\*(:>
+.Al
+\*(<:although\*(:>
+.Al
+\*(<:because\*(:>
+.Al
+\*(<:yet\*(:>
+.Tx
+This produces sentences like:
+.Di 4
+.in -6
+\*(<:dogs do not love the police\*(:>
+\*(<:the police hassle dogs\*(:>
+\*(<:cats do not hate cats , but cats hate dogs , because dogs hate cats\*(:>
+\*(<:people eat dogs , yet dogs love people\*(:>
+.in +6
+.Ed
+.in 0
+You will notice that the names of rules are in a different
+typeface to words that stand for themselves.
+In the grammar of \*B that follows, furthermore, rule names
+are all in lower-case letters, while words that stand for themselves are all
+in upper-case letters, so they are easily distinguished.
+.sp
+It often happens that a part of an alternative is optional.
+There is a special rule for this:
+.Sy  4
+.Pr empty 2
+.Al
+.br
+.Pr optional-ANYTHING 3
+.Al
+empty
+.Al
+ANYTHING
+.Tx
+The ``optional'' rule is included to save many rules in the definition.
+For example, it stands for a rule
+.Pn  optional-comment 3
+.Al
+empty
+.Al
+comment
+.Tx
+and similar rules.
+(Empty produces an empty result.)
+.St 3 REPRESENTATIONS
+.Xx indentation
+.Xx increase-indentation
+.Xx decrease-indentation
+.Xx new-line-proper
+.Xx keyword
+.Xx tag
+.Pr new-line 2
+.Sl
+optional-comment\0new-line-proper\0indent
+.Ps
+A \*B program consists of indented lines.
+A new-line-proper marks a transition to a new line.
+An indent stands for the left margin blank offset.
+Initially, the left margin has zero width.
+The indentation is increased by an increase-indentation
+and decreased again by a decrease-indentation.
+These always come in pairs and serve for grouping, just as BEGIN-END pairs
+do in other programming languages.
+An increase-indentation is always preceded by a line ending with a colon
+(possibly followed by comment).
+.Pr comment 3
+.Al
+optional-new-line-proper\0optional-spaces
+\*(<:\\\*(:> comment-body\0optional-further-comment
+.Pr further-comment 3
+.Al
+new-line-proper\0optional-spaces
+\*(<:\\\*(:> comment-body\0optional-further-comment
+.Pr spaces 2
+.Sl
+space\0optional-spaces
+.Ps
+Comments may be placed at the end of a line or may stand alone
+on a line.
+No comment may precede the first line of a unit (see section 4).
+.br
+A comment-body may be any sequence of printable characters.
+.Sx 2 comment:
+\*(<:\\modified 6/4/84 to reject passwords of length < 6\*(:>
+.Tx
+Keywords are composed of CAPITAL letters (\*(<:A\*(:> to \*(<:Z\*(:>), digits,
+and quotes (\*(<:'\*(:> and \*(<:"\*(:>).
+A keyword must start with a letter.
+For example, \*(<:A3'B"\*(:> is a keyword.
+.Tx
+Tags are composed of lower-case letters (\*(<:a\*(:> to \*(<:z\*(:>), digits, 
+and quotes (\*(<:'\*(:> and \*(<:"\*(:>).
+A tag must start with a letter.
+For example, \*(<:a3'b"\*(:> is a tag.
+.Tx
+Some other signs are composite: \*(<:..\*(:>, \*(<:**\*(:>, \*(<:*/\*(:>, \*(<:/*\*(:>, \*(<:^^\*(:>,
+\*(<:<<\*(:>, \*(<:><\*(:>, \*(<:>>\*(:>, \*(<:<=\*(:>, \*(<:<>\*(:> and \*(<:>=\*(:>.
+Spaces are freely allowed between symbols, but not
+within keywords, tags,  numeric-constants and composite signs.
+Sometimes spaces are required to separate keywords and tags from following
+symbols.
+For example, \*(<:cos y\*(:> is not the same as \*(<:cosy\*(:>: the latter is
+taken to be one tag.
+.St 4 UNITS 
+.Xx work-space
+.Sy  4
+.Pr unit 4
+.Al
+how-to-unit
+.Al
+yield-unit
+.Al
+test-unit
+.Ps
+Units are the building blocks of a \*B ``program''.
+Users can define new commands, functions and predicates by writing a unit.
+These units reside in a work-space.
+.Pr refinement-suite 2
+.Al
+new-line\0refinement\0optional-refinement-suite
+.Ps
+When writing a unit, the specification of some parts
+(commands, expressions and tests) may be deferred by
+using a ``refinement''.
+These refinements are then specified at the end of the unit.
+.Se 3  4.1 HOW-TO-UNITS
+.Xx keyword
+.Xx user-defined-command
+.Sy  3
+.Pr how-to-unit 3
+.Al
+\*(<:HOW'TO\*(:> formal-user-defined-command\*(<::\*(:>
+.br
+command-suite
+.br
+optional-refinement-suite
+.Pr formal-user-defined-command 2
+.Sl
+keyword\0optional-formal-tail
+.Ps 
+The first keyword of a formal-user-defined-command must be unique, i.e.,
+different from the first keywords of all predefined and other
+user-defined commands.
+So it is impossible to redefine the built-in commands of \*B.
+It may also not be \*(<:HOW'TO\*(:>, \*(<:YIELD\*(:>, \*(<:TEST\*(:>, \*(<:SHARE\*(:> or \*(<:ELSE\*(:>.
+Otherwise, it may be chosen freely.
+There are no restrictions on the second and further keywords.
+.Pr formal-tail 3
+.Al
+formal-parameter\0optional-formal-trailer
+.Al
+formal-trailer
+.Pr formal-trailer 2
+.Sl
+keyword\0optional-formal-tail
+.Pr formal-parameter 1
+.Sl
+tag
+.Ps
+Note that, although actual-parameters (section 5.1.16)
+and formal-operands (section 4.2) may be composite,
+formal-parameters must be simple tags.
+.Sx 5 \k1how-to-unit:
+\*(<:HOW'TO PUSH value ON stack:
+    PUT value IN stack[#stack+1]\*(:>
+.Tx
+A how-to-unit defines the meaning of a new command
+(see ``user-defined-commands'', section 5.1.16).
+The above unit defines a \*(<:PUSH\*(:>\ ...\ \*(<:ON\*(:>\ ... command.
+Once the command has been defined, it may be used in the
+same way as the built-in commands.
+Other user-defined commands may be used in the body of a unit
+even if they have not yet been defined,
+though they must be defined by the time the unit is invoked.
+.Xe
+.Sa
+quit-command (5.1.11),
+share-heading (4.5),
+user-defined-commands (5.1.16).
+.Se 3  4.2 YIELD-UNITS
+.Xx "overloading of functions and predicates"
+.Xx user-defined functions
+.Xx formula
+.Xx function
+.Xx predicate
+.Xx zeroadic
+.Xx monadic
+.Xx dyadic
+.Sy  3
+.Pr yield-unit 3
+.Al
+\*(<:YIELD\*(:> formal-formula\*(<::\*(:>
+.br
+command-suite
+.br
+optional-refinement-suite
+.Pr formal-formula 4
+.Al
+formal-zeroadic-formula
+.Al
+formal-monadic-formula
+.Al
+formal-dyadic-formula
+.Pr formal-zeroadic-formula 2
+.Sl
+zeroadic-function
+.Pr formal-monadic-formula 2
+.Sl
+monadic-function\0formal-operand
+.Pr formal-dyadic-formula 2
+.Al
+formal-operand\0dyadic-function\0formal-operand
+.Ps 
+Functions must not be ``overloaded'' (multiply defined),
+and a user-defined function must be represented by a tag.
+However, a given tag may be used, at the same time, for
+a dyadic-function and either a zeroadic- or a monadic-function or -predicate.
+(In other words, you may not have a function that is both monadic
+and zeroadic, for otherwise it would be impossible to decide what was meant
+in cases such as \*(<:f + 1\*(:>,
+where \*(<:f\*(:> could be either zeroadic or monadic, and the restrictions
+also apply to combinations of functions and predicates.)
+.Pr formal-operand 2
+.Sl
+single-identifier
+.Sx 5 \k1yield-unit:
+\*(<:YIELD (a, b) over (c, d):
+    PUT c*c+d*d IN rr
+    RETURN (a*c+b*d)/rr, (-a*d+b*c)/rr\*(:>
+.Xe
+.Tx
+A yield-unit defines the meaning of a new function
+(see ``Formulas with user-defined functions'', section 6.1.6).
+The example given above defines complex division.
+(Complex numbers are not a built-in type of \*B.)
+.br
+Functions may be zeroadic (no operands), monadic (one trailing operand)
+or dyadic (two operands, one at the left and one at the right).
+.Sa
+return-commands (5.1.12),
+share-headings (4.5),
+formulas with user-defined functions (6.1.6).
+.Se 3  4.3 TEST-UNITS
+.Xx "overloading of functions and predicates"
+.Xx user-defined-predicates
+.Xx test
+.Xx formula
+.Xx function
+.Xx predicate
+.Xx proposition
+.Xx zeroadic
+.Xx monadic
+.Xx dyadic
+.Sy  3
+.Pr test-unit 3
+.Al
+\*(<:TEST\*(:> formal-proposition\*(<::\*(:>
+.br
+command-suite
+.br
+optional-refinement-suite
+.Pr formal-proposition 4
+.Al
+formal-zeroadic-proposition
+.Al
+formal-monadic-proposition
+.Al
+formal-dyadic-proposition
+.Pr formal-zeroadic-proposition 2
+.Sl
+zeroadic-predicate
+.Pr formal-monadic-proposition 2
+.Al
+monadic-predicate\0formal-operand
+.Pr formal-dyadic-proposition 2
+.Al
+formal-operand\0dyadic-predicate\0formal-operand
+.Ps 
+Like functions, predicates must not be ``overloaded'',
+though a given tag may be used, at the same time, for
+a dyadic-predicate and either a zeroadic- or a monadic-function or -predicate.
+.Sx 5 \k1test-unit:
+\*(<:TEST a subset b:
+    REPORT EACH x IN a HAS x in b\*(:>
+.Xe
+.Tx
+A test-unit defines the meaning of a new predicate
+(see ``Propositions with user-defined predicates'', section 6.3.2).
+Like functions, predicates may be zeroadic, monadic or dyadic.
+.br
+Tests do not return a value, but succeed or fail via the \*(<:REPORT\*(:>,
+\*(<:SUCCEED\*(:> and \*(<:FAIL\*(:> commands.
+.Sa
+report-commands (5.1.13),
+succeed-command (5.1.14),
+fail-command (5.1.15),
+share-headings (4.5),
+propositions with user-defined predicates (6.3.2).
+.Se 4  4.4 REFINEMENTS
+.Xx keyword
+.Sy  4
+.Pr refinement 4
+.Al
+command-refinement
+.Al
+expression-refinement
+.Al
+test-refinement
+.Pr command-refinement 2
+.Sl
+keyword\*(<::\*(:> command-suite
+.Ps
+The keyword of a command-refinement must be different from the first keywords
+of all predefined commands,
+and it may also not be \*(<:HOW'TO\*(:>, \*(<:YIELD\*(:>, \*(<:TEST\*(:>, \*(<:SHARE\*(:> or \*(<:ELSE\*(:>.
+It may, however, be the same as the first keyword of a user-defined-command.
+.Sx 4 \k1command-refinement:
+\*(<:SELECT'TASK:
+    PUT min tasks IN task
+    REMOVE task FROM tasks\*(:>
+.Pr expression-refinement 2
+.Sl
+tag\*(<::\*(:> command-suite
+.Sx 4 expression-refinement:
+\*(<:stack'pointer:
+    IF stack = {}: RETURN 0
+    RETURN max keys stack\*(:>
+.Pr test-refinement 2
+.Sl
+tag\*(<::\*(:> command-suite
+.Sx 4 test-refinement:
+\*(<:special'case:
+    REPORT position+d = line'length\*(:>
+.Xe
+.Tx
+Refinements support the method of ``top-down'' programming, also
+known as programming by ``stepwise refinement''.
+The body of a unit may be written using refined-commands, -expressions
+and -tests that reflect the appropriate, coarse-grained, level of
+abstraction for expressing the algorithmic intention.
+In subsequent refinements, these may be refined to
+the necessary detail, possibly in several steps.
+As with units, there are three kinds of refinements.
+The differences with units are:
+.in (\w'\(em\ 'u+3m)u
+.ti 3m
+\(em\ refinements are bound to a unit and may not be invoked
+from other units;
+.ti 3m
+\(em\ all tags known inside the unit are also known inside the
+refinement;
+.ti 3m
+\(em\ no parameters or operands can be passed when the
+refinement is invoked.
+.in 0
+{{Currently, refinements may only occur within unit bodies, and not
+in ``immediate commands''.}}
+.Sa
+refined-commands (5.1.17),
+refined-expressions (6.1.7),
+refined-tests (6.3.3).
+.Se 4  4.5 COMMAND-SUITES
+.Xx target
+.Xx local
+.Xx global
+.Xx work-space
+.Xx permanent environment
+.Xx yield-unit
+.Xx expression-refinement
+.Xx return-command
+.Xx test-unit
+.Xx test-refinement
+.Xx report-command
+.Xx succeed-command
+.Xx fail-command
+.Sy  4
+.Pr command-suite 4
+.Al
+simple-command
+.Al
+increase-indentation\0optional-share-heading
+optional-command-sequence\0decrease-indentation
+.Ps
+A command-suite may only follow the preceding colon on the same line
+if it is a simple-command.
+Otherwise, it starts on a new line, with
+all lines of the command-suite indented.
+.Sx 4 command-suite
+\*(<:SHARE name'list, abbreviation'table
+IF name in keys abbreviation'table:
+    PUT abbreviation'table[name] IN name
+IF name not'in name'list:
+    INSERT name IN name'list\*(:>
+.Xe
+.Pr share-heading 3
+.Al
+new-line \*(<:SHARE\*(:> identifier\0optional-share-heading
+.Ps 
+Tags used as targets (variables) in a unit
+(except those that are formal-parameters)
+are by default local to the unit.
+If a target should be shared between several units,
+this can be indicated by listing the tag
+in a share-heading at the start of the unit body.
+It stands then for a global target of the work-space.
+The global targets together with their contents are also called the ``permanent
+environment'', because they survive on logging out.
+.br
+A share-heading may only occur in the command-suite of a unit (and not
+of a refinement or compound-command).
+.Sx 2 share-heading
+\*(<:SHARE name'list, abbreviation'table\*(:>
+.Xe
+.Pr command-sequence 2
+.Al
+new-line\0command\0optional-command-sequence
+.Ps 
+The execution of the command-suite of a yield-unit or
+expression-refinement must end in a return-command, and return-commands
+may only occur within such command-suites.
+.Ps 
+The execution of the command-suite of a test-unit or
+test-refinement must end in a report-, succeed- or fail-command, and these
+may only occur within such command-suites.
+.Sx 3 command-sequence
+\*(<:IF name in keys abbreviation'table:
+    PUT abbreviation'table[name] IN name
+IF name not'in name'list:
+    INSERT name IN name'list\*(:>
+.Xe
+.St 5 COMMANDS
+.Xx immediate command
+.Xx global
+.Xx interrupt key
+.Tx
+Commands may be given as ``immediate commands'', directly from
+the terminal, or may be part of a unit.
+If commands are given as immediate commands, they are obeyed
+directly.
+Any targets in the command are then interpreted as global targets
+from the permanent environment.
+Within a unit, targets are local, unless they have been listed
+in a share-heading (see above).
+.br
+If the user presses the interrupt key while a command is executing,
+execution is aborted, and the user is prompted for another immediate command.
+.Sy  3
+.Pr command 3
+.Al
+simple-command
+.Al
+control-command
+.Se 3  5.1 SIMPLE-COMMANDS
+.Sy  3
+.Pr simple-command 3
+.Al
+check-command
+.Al
+write-command
+.Al
+read-command
+.Al
+put-command
+.Al
+draw-command
+.Al
+choose-command
+.Al
+set-random-command
+.Al
+remove-command
+.Al
+insert-command
+.Al
+delete-command
+.Al
+terminating-command
+.Al
+user-defined-command
+.Al
+refined-command
+.Pr terminating-command 3
+.Al
+quit-command
+.Al
+return-command
+.Al
+report-command
+.Al
+succeed-command
+.Al
+fail-command
+.Se 2  5.1.1 CHECK-COMMANDS
+.Sy  2
+.Pr check-command 2
+.Sl
+\*(<:CHECK\*(:> test
+.Sx 3 \k1check-command:
+\*(<:CHECK i >= 0 AND j >= 0 AND i+j <= n\*(:>
+.Xe
+.Tx
+When a check-command is executed, its test is tested.
+If the test fails, an error is reported and execution halts.
+Otherwise, no message is given and execution continues.
+Check-commands may be used, for example, to check the requirements of
+parameters or operands on entry to a unit.
+The liberal use of check-commands helps to get programs correct quickly.
+.Se 3  5.1.2 WRITE-COMMANDS
+.Xx convert to a text
+.Xx permanent environment
+.Xx interrupt key
+.Sy  3
+.Pr write-command 3
+.Al
+\*(<:WRITE\*(:> new-liners
+.Al
+\*(<:WRITE\*(:> optional-new-liners\0expression\0optional-new-liners
+.Pr new-liners 2
+.Sl
+\*(<:/\*(:> optional-new-liners
+.Ex 3
+\k1write-commands:
+\h'|\n1u'\*(<:WRITE //\*(:>
+\h'|\n1u'\*(<:WRITE // 'Give a value in the range 1 through `n`: '\*(:>
+.Tx
+The expression is converted to a text and written to the screen.
+Each \*(<:/\*(:> gives a transition to a new line.
+Note that you write no comma before or after the \*(<:/\*(:>s.
+.br
+With the exception of adjacent texts,
+values that are adjacent are written separated by a space.
+Compounds within other values (within lists, tables or other compounds)
+are written with commas between their fields,
+and where necessary, the whole surrounded by brackets.
+Similarly, inner texts are written enclosed by quotes.
+Compounds and texts not within other values are output without commas,
+brackets and quotes.
+Thus,
+.Di 2
+\*(<:WRITE 0, 1, ',', 2, '!', '!', 3
+WRITE {1; 2}, {['a','b']:('b','a'); ['b','a']:('a','b')} /\*(:>
+.Ed
+gives
+.Di 1
+\*(<:0 1 , 2 !! 3 {1; 2} {['a', 'b']: ('b', 'a'); ['b', 'a']: ('a', 'b')}\*(:>
+.Ed
+For formatting purposes, see the operators \*(<:>>\*(:>, \*(<:<<\*(:>, and \*(<:><\*(:>
+in section 6.1.6, ``Functions on Texts'',
+and the conversions in text-displays in section 6.1.5, ``Displays''.
+.Se 3  5.1.3 READ-COMMANDS
+.Sy  3
+.Pr read-command 4
+.Al
+\*(<:READ\*(:> target \*(<:EG\*(:> expression
+.Al
+\*(<:READ\*(:> target \*(<:RAW\*(:>
+.Ex 3
+read-commands:
+\*(<:READ n, s EG 0, ''
+READ line RAW\*(:>
+.Xe
+.Tx
+The execution of a read-command prompts the user
+to supply one input line.
+.br
+If an \*(<:EG\*(:> part is present, the input is interpreted as an
+\fIexpression\fP of the same type as the expression following \*(<:EG\*(:>.
+(Usually, the example expression will consist of constants,
+but other expressions are also allowed.)
+The input expression is evaluated in the permanent environment
+(so local tags of units cannot be used) and put in the target.
+To input a text-display (literal), text quotes are required.
+.br
+If \*(<:RAW\*(:> is specified, the target must be a text target.
+The input line is put in the target literally.
+No text quotes are needed.
+.br
+If the user presses the interrupt key instead of supplying a value,
+the read-command, and in fact the whole program, is aborted.
+This is useful for entering a sequence of data of unspecified length.
+.Se 3  5.1.4 PUT-COMMANDS
+.Xx target
+.Xx location
+.Xx type
+.Sy  3
+.Pr put-command 3
+.Sl
+\*(<:PUT\*(:> expression \*(<:IN\*(:> target
+.Sx 3 \k1put-command:
+\*(<:PUT a+1, ({}, {1..a}) IN a, b\*(:>
+.Xe
+.Tx
+The value of the expression is put in the target.
+This means that the value will be held in a location
+for the target, until a different value is put in the target,
+or the target is deleted.
+If no such location exists already, it is created on
+the spot.
+Here, as in other cases, the types must agree.
+{{This is currently not checked in general.}}
+See also the sections on various kinds of targets below (section 6.2).
+.Se 2  5.1.5 DRAW-COMMANDS
+.Xx random
+.Xx number
+.Sy  2
+.Pr draw-command 2
+.Sl
+\*(<:DRAW\*(:> target
+.Sx 3 \k1draw-command:
+\*(<:DRAW r\*(:>
+.Xe
+.Tx
+A random approximate number
+(from \*(<:~0\*(:> up to, but not including, \*(<:~1\*(:>)
+is drawn and put in the target.
+.Se 4  5.1.6 CHOOSE-COMMANDS
+.Xx text, list or table
+.Xx random
+.Xx character
+.Xx list entry
+.Xx associate
+.Sy  4
+.Pr choose-command 4
+.Sl
+\*(<:CHOOSE\*(:> target \*(<:FROM\*(:> expression
+.Sx 3 \k1choose-command:
+\*(<:CHOOSE exit FROM exits[current'room]\*(:>
+.Xe
+.Tx
+The expression must have a text, list or table as value.
+This value must not be empty.
+An item is drawn at random from the value
+(characters from a text, entries from a list and associates
+from a table)
+and put in the target.
+The item is not removed from the value.
+.Se 2  5.1.7 SET-RANDOM-COMMANDS
+.Xx random
+.Sy  2
+.Pr set-random-command 2
+.Sl
+\*(<:SET'RANDOM\*(:> expression
+.Sx 3 \k1set-random-command:
+\*(<:SET'RANDOM 'Monte Carlo', run\*(:>
+.Xe
+.Tx
+The (pseudo-)random sequence
+used for draw- and choose-commands
+is reset to a point, depending on the
+value of the expression.
+.Se 3  5.1.8 REMOVE-COMMANDS
+.Xx list entry
+.Sy  3
+.Pr remove-command 3
+.Sl
+\*(<:REMOVE\*(:> expression \*(<:FROM\*(:> target
+.Sx 3 \k1remove-command:
+\*(<:REMOVE task FROM tasks\*(:>
+.Xe
+.Tx
+The target must hold a list, and the value of the expression must be
+an entry of that list.
+The entry is removed.
+If it was present more than once, only one instance is removed.
+.Se 3  5.1.9 INSERT-COMMANDS
+.Xx list entry
+.Sy  3
+.Pr insert-command 3
+.Sl
+\*(<:INSERT\*(:> expression \*(<:IN\*(:> target
+.Sx 3 \k1insert-command:
+\*(<:INSERT new'task IN tasks\*(:>
+.Xe
+.Tx
+The target must hold a list.
+The value of the expression is inserted as a list entry.
+If that entry was already present, one more instance will be present.
+.Se 2  5.1.10 DELETE-COMMANDS
+.Xx location
+.Xx table entry
+.Xx table-selection-target
+.Sy  2
+.Pr delete-command 2
+.Sl
+\*(<:DELETE\*(:> target
+.Sx 3 \k1delete-command:
+\*(<:DELETE t[i], u[i, j]\*(:>
+.Xe
+.Tx
+The location for the target ceases to exist.
+If a multiple-target is given, all its single-targets are deleted.
+If a table-selection-target is given, the table must contain the key
+that is used as selector.
+The table entry with that key is then deleted from the table.
+It is an error to delete a trimmed-text-target (e.g., \*(<:t@2\*(:>).
+.Se 2  5.1.11 QUIT-COMMAND
+.Xx how-to-unit
+.Xx command-refinement
+.Xx immediate-command
+.Xx permanent environment
+.Sy  2
+.Pr quit-command 2
+.Sl
+\*(<:QUIT\*(:>
+.Ps 
+A quit-command may only occur in the command-suite of a
+how-to-unit or command-refinement, or as an immediate command.
+.Sx 3 \k1quit-command:
+\*(<:QUIT\*(:>
+.Xe
+.Tx
+The execution of a quit-command causes the termination of the execution
+of the how-to-unit or command-refinement in whose command-suite
+it occurs.
+If it occurs in a command-refinement, the execution of
+the invoking refined-command is thereby terminated and the further
+execution continues as if the refined-command had terminated normally.
+Otherwise, the execution of
+the invoking user-defined-command is terminated and the further
+execution continues similarly.
+.br
+Given as an immediate command, \*(<:QUIT\*(:> terminates the current
+session.
+All units and targets in the permanent environment
+survive and can be used again at the next session.
+.Se 2  5.1.12 RETURN-COMMANDS
+.Xx expression-refinement
+.Xx user-defined-function
+.Xx refined-expression
+.Xx yield-unit
+.Sy  2
+.Pr return-command 2
+.Sl
+\*(<:RETURN\*(:> expression
+.Sx 3 \k1return-command:
+\*(<:RETURN (a*c+b*d)/rr, (-a*d+b*c)/rr\*(:>
+.Xe
+.Tx
+The execution of a return-command causes the termination of the execution
+of the yield-unit or expression-refinement in whose command-suite
+it occurs.
+The value of the expression is returned as the value of the invoking
+user-defined function or refined-expression.
+Return-commands may only occur within the command-suite of a
+yield-unit or expression-refinement.
+.Se 2  5.1.13 REPORT-COMMANDS
+.Xx test-unit
+.Xx test-refinement
+.Xx user-defined-predicate
+.Xx refined-test
+.Xx bound tags
+.Pr report-command 2
+.Sl
+\*(<:REPORT\*(:> test
+.Sx 3 \k1report-command:
+\*(<:REPORT i in keys t\*(:>
+.Xe
+.Tx
+The execution of a report-command causes the termination of the execution
+of the test-unit or test-refinement in whose command-suite
+it occurs.
+The invoking user-defined predicate or refined-test
+succeeds/fails if the test of the report-command succeeds/fails.
+If the invoker is a test-refinement,
+any bound tags set by a for-command (see section 5.2.4) or
+a quantification (section 6.3.7) will temporarily survive,
+as described under REFINED-TESTS (section 6.3.3).
+.br
+Report-commands may only occur within the command-suite of a
+test-unit or test-refinement.
+.br
+The command ``\*(<:REPORT\*(:> test'' is equivalent to
+.Di 3
+\*(<:SELECT:
+    \*(:>test\*(<:: SUCCEED
+    ELSE: FAIL\*(:>
+.Ed
+.Se 2  5.1.14 SUCCEED-COMMAND
+.Xx test-unit
+.Xx test-refinement
+.Xx user-defined-predicate
+.Xx refined-test
+.Xx bound tags
+.Sy  2
+.Pr succeed-command 2
+.Sl
+\*(<:SUCCEED\*(:>
+.Sx 3 \k1succeed-command:
+\*(<:SUCCEED\*(:>
+.Xe
+.Tx
+The execution of a succeed-command causes the termination of the execution
+of the test-unit or test-refinement in whose command-suite
+it occurs.
+The invoking user-defined predicate or refined-test succeeds.
+As with report-commands, bound tags temporarily survive.
+.br
+Succeed-commands may only occur within the command-suite of a
+test-unit or test-refinement.
+.br
+The command \*(<:SUCCEED\*(:> is equivalent to \*(<:REPORT 0 = 0\*(:>.
+.Se 2  5.1.15 FAIL-COMMAND
+.Xx test-unit
+.Xx test-refinement
+.Xx user-defined-predicate
+.Xx refined-test
+.Xx bound tags
+.Sy  2
+.Pr fail-command 2
+.Sl
+\*(<:FAIL\*(:>
+.Sx 3 \k1fail-command:
+\*(<:FAIL\*(:>
+.Xe
+.Tx
+The execution of a fail-command causes the termination of the execution
+of the test-unit or test-refinement in whose command-suite
+it occurs.
+The invoking user-defined predicate or refined-test fails.
+As with report-commands, bound tags temporarily survive.
+.br
+Fail-commands may only occur within the command-suite of a
+test-unit or test-refinement.
+.br
+The command \*(<:FAIL\*(:> is equivalent to \*(<:REPORT 0 = 1\*(:>.
+.Se 2  5.1.16 USER-DEFINED-COMMANDS
+.Xx keyword
+.Xx how-to-unit
+.Xx quit-command
+.Sy  2
+.Pr user-defined-command 2
+.Sl
+keyword\0optional-actual-parameter\0optional-trailer
+.Pr trailer 2
+.Sl
+keyword\0optional-actual-parameter\0optional-trailer
+.Pr actual-parameter 2
+.Al
+identifier
+.Al
+target
+.Al
+expression
+.Ps 
+The keywords and actual-parameters must correspond one to one to those
+of the formal-user-defined-command of one unique how-to-unit.
+.Ex 6
+\k1user-defined-commands:
+\h'|\n1u'\*(<:CLEAN'UP\*(:>
+\h'|\n1u'\*(<:DRINK me\*(:>
+\h'|\n1u'\*(<:TURN a UPSIDE DOWN\*(:>
+\h'|\n1u'\*(<:PUSH v ON operand'stack\*(:>
+.Xe
+.Tx
+A user-defined-command is executed in the following steps:
+.in \w'2.\ 'u
+.ti 0
+1.\ Any local tags in the how-to-unit that might clash with tags currently
+in use are systematically replaced by other tags that do not cause conflict.
+.ti 0
+2.\ Each actual-parameter is placed between parentheses \*(<:(\*(:> and \*(<:)\*(:>
+and then
+substituted throughout the unit for the corresponding formal-parameter.
+.ti 0
+3.\ The command-suite of the unit, thus modified, is executed.
+.in 0
+The execution of the user-defined-command is complete when the execution
+of this command-suite terminates (normally, or because of the execution
+of a quit-command).
+After the execution is complete,
+the local tags of the unit are no longer accessible.
+.Se 2  5.1.17 REFINED-COMMANDS
+.Xx keyword
+.Xx command-refinement
+.Xx quit-command
+.Sy  2
+.Pr refined-command 2
+.Sl
+keyword
+.Ps 
+The keyword of a refined-command must occur as the keyword of one
+command-refinement in the unit
+in which it occurs.
+That command-refinement specifies the meaning of the refined-command.
+.Sx 3 \k1refined-command:
+\*(<:REMOVE'MULTIPLES\*(:>
+.Xe
+.Tx
+A refined-command is executed by executing
+the command-suite of the corresponding command-refinement.
+The execution of the refined-command is complete when the execution
+of this command-suite terminates
+(normally, or because of the execution of a quit-command).
+.Se 5  5.2 CONTROL-COMMANDS
+.Sy  5
+.Pr control-command 5
+.Al
+if-command
+.Al
+select-command
+.Al
+while-command
+.Al
+for-command
+.Se 2  5.2.1 IF-COMMANDS
+.Sy  2
+.Pr if-command 2
+.Sl
+\*(<:IF\*(:> test\*(<::\*(:> command-suite
+.Sx 3 \k1if-command:
+\*(<:IF i < 0: PUT -i, -j IN i, j\*(:>
+.Xe
+.Tx
+The test is tested.
+If it succeeds, the command-suite is executed;
+if it fails, the command-suite is not executed.
+.br
+(If something should be executed on failure too, or there are
+more alternatives, you should use a select-command instead.)
+.br
+The command
+``\*(<:IF\*(:> test\*(<::\*(:> command-suite''
+is equivalent to:
+.Di 3
+\*(<:SELECT:
+    \*(:>test\*(<:: \*(:>command-suite\*(<:
+    ELSE: \\do nothing.\*(:>
+.Ed
+.Se 2  5.2.2 SELECT-COMMANDS
+.Sy  2
+.Pr select-command 2
+.Sl
+\*(<:SELECT:\*(:> alternative-suite
+.Pr alternative-suite 3
+.Al
+increase-indentation\0new-line\0alternative-sequence\0decrease-indentation
+.Pr alternative-sequence 4
+.Al
+single-alternative
+.Al
+else-alternative
+.Al
+single-alternative\0new-line\0alternative-sequence
+.Pr single-alternative 2
+.Sl
+test\*(<::\*(:> command-suite
+.Pr else-alternative 2
+.Sl
+\*(<:ELSE:\*(:> command-suite
+.Eo 5 select-commands:\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\k2\":
+\h'|\n1u'\*(<:SELECT:\*(:> \h'|\n2u'\*(<:SELECT:\*(:>
+\h'|\n1u'\*(<:    a < 0: RETURN -a\*(:> \h'|\n2u'\*(<:    a < 0: RETURN -a\*(:>
+\h'|\n1u'\*(<:    a >= 0: RETURN a\*(:> \h'|\n2u'\*(<:    ELSE: RETURN a\*(:>
+.Xe
+.Tx
+The tests of the alternatives are tested one by one,
+starting with the first and proceeding downwards, until one
+is found that succeeds.
+The corresponding command-suite is then executed.
+\*(<:ELSE\*(:> may be used in the final alternative as a test that always succeeds.
+If all the tests fail, an error is reported.
+.Se 2  5.2.3 WHILE-COMMANDS
+.Xx terminating command
+.Sy  2
+.Pr while-command 2
+.Sl
+\*(<:WHILE\*(:> test\*(<::\*(:> command-suite
+.Sx 3 \k1while-command:
+\*(<:WHILE x > 1: PUT x/10, c+1 IN x, c\*(:>
+.Xe
+.Tx
+If the test succeeds, the command-suite is executed, and the
+while-command is repeated, and so on, until the test fails,
+or until an escape is forced by a terminating command.
+If the test fails the very first time, the command-suite is
+not executed at all.
+.Se 3  5.2.4 FOR-COMMANDS
+.Xx text, list or table
+.Xx character
+.Xx list entry
+.Xx associate
+.Xx target
+.Xx bound tags
+.Sy  3
+.Pr for-command 3
+.Sl
+\*(<:FOR\*(:> in-ranger\*(<::\*(:> command-suite
+.Pr in-ranger 2
+.Sl
+identifier \*(<:IN\*(:> expression
+.Sx 3 \k1for-command:
+\*(<:FOR i, j IN keys t: PUT t[i, j] IN t'[j, i]\*(:>
+.Xe
+.Tx
+The value of the expression must be a text, list or table.
+One by one, each item of that value
+(characters for a text, list entries for a list and associates for a table)
+is put in the identifier, and the command-suite executed.
+For example,
+.Di 1
+\*(<:FOR c IN 'ABC': WRITE 'letter is', c /\*(:>
+.Ed
+is equivalent to
+.Di 3
+\*(<:WRITE 'letter is', 'A' /
+WRITE 'letter is', 'B' /
+WRITE 'letter is', 'C' /\*(:>
+.Ed
+If \*(<:t\*(:> is a table, then
+``\*(<:FOR a IN t: TREAT a\*(:>''
+treats the associates of \*(<:t\*(:> in the same way as
+.Di 3
+\*(<:FOR k IN keys t:
+    PUT t[k] IN a
+    TREAT a\*(:>
+.Ed
+The tags of the identifier of a for-command may not be used as targets
+or target-contents
+outside such a for-command.
+They are ``bound tags'', and lose their meaning outside the
+for-command.
+There is one exception to this rule:
+if a for-command is used in a test-refinement, and within
+the for-command a report-, succeed- or fail-command is
+executed, the currently bound tags will temporarily survive
+as described under REFINED-TESTS (section 6.3.3).
+.Sa
+quantifications (6.3.7).