[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] >> [papers] >> rjb99g.xbnf
[Index] [Contents] [Source] [Notation] [Copyright] [Comment] [Search ]
Thu Nov 8 14:28:24 PST 2012

This part of my site contains partly baked ideas (PBI). It has drafts for publications, essays, plus illustrations and visual aids for presentations and seminars.

Disclaimer. CSUSB and the CS Dept have no responsibility for the content of this page.

Copyright. Richard J. Botting ( Thu Nov 8 14:28:24 PST 2012 ). Permission is granted to quote and use this document as long as the source is acknowledged.


    How Far Can EBNF Stretch?


      Dr. Richard J. Botting <dick@csci.csusb.edu>


      Computer Science Dept, CSUSB (909)-880-5327 rbotting@csusb.edu


      http://cse.csusb.edu/dick/papers/rjb99g.xbnf.mth http://cse.csusb.edu/dick/papers/rjb99g.xbnf.html


      Presented May 14th 1993 [ rjb93a.xbnf.html ]

      Revised March 1995

      Revised March-April 1996 [ rjb96x.xbnf.html ]

      Revised June 1999 to include latest additions to the notations: Tables and distinguishing quotation from assertion.

      Revised November 2012 to give a better reference to Cantor's Theorem.


      Extensions to Backus Naur Form(EBNFs) have been in use for nearly 30 years. They are a form of documentation that is both mathematical and widely used. I explore the use of EBNF as a role model for how a mathematical idea (grammar theory) can be put to use. I will show that EBNF can be extended much further than its use in documenting syntax. It can be a paradigm for the formal documentation of requirements, designs, and specifications of all types of software.

      I will further show that there comes a point when BNF style definitions can cease to have meaning and lead to paradoxes.

      Body of Paper



          BNF became Extended BNF and is used in all programming language standards and manuals. It is a most successful modern formal notation. This presentation examines how EBNF can be extended to help in other parts of software engineering. I start by listing similar forms that are already in use in non-linguistic domains.

          I then define EBNF formally and then to explore the consequences of making small changes to the syntax and semantics of EBNF. This gives rise to a version called XBNF that has proved useful in teaching a programming languages course.

          We can define terms of other types: Sets, functions, relations, types, classes, ... Definitions become a way of naming that can be used in any kind of documentation.

          Finally, we can treat a piece of documentations itself as a piece of data. I will show how BNF can be used for pieces of documentation. The effect is to introduce an enhanced for inheritance into general documentation. Documentation becomes a "first class object" for its users. The theory of the resulting system seems to need recently developed theories of types, semantics, etc[Example: Leeuwen 90].

          I prove that one set of extensions leads to paradox and hence has to be forbidden.

          Relation to other work

          This is part of an experiment on inexpensive formal documentation. The working name for the language is MATHS [C Sci Seminar CSUSB 1992]. I have a graphical version called TEMPO [Faculty Research Seminar CSUSB 1992]. The goals (but not the tools or means) of this project are similar to those of the Z language and the PVS system. The goals are wider than those of languages like Larch, Anna, LOTOS, Spec, VDL, or SDL. The aim is to be a general way for software developers to use mathematical and logical notation as part of their work: analysis, design, code, EMail, jokes, etc. without having to learn ΤΕΧ.

        . . . . . . . . . ( end of section Introduction) <<Contents | End>>

        Grammars & Dictionaries


          Bugs occur when ideas are not clearly understood - so good software depends on defining terms correctly and exactly. All projects need a collection of definitions. Call a set of definitions a dictionary . A BNF grammar is such a dictionary. BNF is a syntactically sugared context free grammar. EBNF has the same expressive power as BNF, but is easier to write because it permits regular expressions on the right hand side of a definition:
          	BNF       	<number>::=<digit>|<number><digit>	[Naur et al 64]
          	EBNF     	number::= digit {digit}		[ANSI 83 ADA]
          The '{...}' indicate 'zero or more of. In EBNF a series of non_terminal are defined in terms of a regular expression that represents a set of strings (a language). However, EBNF-like dictionaries turn up in all parts of software engineering theory and practice, see Table 1 below.

          Table 1. Applications

          GrammarTokens|LexemesSyntactic unitsNaur et al 64,...Ada 93
          LexiconStringLexemsBell Labs 83(lex)
          AbstractSyntactic UnitsStructuresProg Lang Semantics
          Data Communication
          ProtocolMessagesProtocolsZave 85, Naik & Sarikaya 92
          Path exprsCallsSynchronisationS/SL
          Ada TasksEntry namesStructureHemendinger 90
          InterfacesMethodsObjectsBotting 86a
          DictionaryData typesData filesDe Marco 80, JSP
          StructureData typesI/O PatternsWarnier/Orr, JSP,
          DynamicsEventsNeural netsKleene 1940s,DAD
          ?CommandsSystem BehaviorsBelli & Grosspietsch 91
          ELHEventsLife HistoriesRobinson 79, JSD,SSADM
          Logic GrammarTermsPredicatesAbramson & Dahl 89
          StructureC Function CallC FunctionsBaecker & Marcus 90

          (Close Table)

          The Traditional Theory of BNF

          The theory of EBNF has been the same for 30 years and is based on defining "string" and "sets of strings." Strings come from an empty string by concatenating symbols. I will show concatenation of strings by an exclamation mark (!). It is assumed to be an associative operation with a unit - the empty string "". Each string, by definition, has a unique sequence of atomic symbols, which when concatenated generate the original string. Temporarily we symbolize strings by lower case variables and sets of strings by upper case variables. Example strings will shown in the C notation (see later if necessary). We next define operations of union(|), and concatenation () on sets of strings by:
        1. A | B::={c || c in A or c in B}, -- set of strings that are in either A or B or both.
        2. A B::={c || c=a ! b and a in A and b in B}, -- the set of all c where c=a!b and a is in A and b is in B.

          A string is treated as a singleton set when it is in a context that needs a set of strings:

        3. For string c, c::sets_of_strings={c}.

          In this section I stands for the set of the empty string:

        4. I::sets_of_strings={""}.

          The definition of (#) takes more machinery.

        5. #A::= zero or more occurrences of A.

          We could write,

        6. #A = I | A | A A | A A A | ... .

          but this formula uses an undefined idea: "...". This makes it difficult to reason accurately about #.

          We could define the powers of a set (A^n) and then write an infinite union

        7. #A = A^0 | A^1 | A^2 | ... = Union{ A^i | i:0,1,2,...}. but first we would have to define infinite unions and powers.

          So we start from the desirable property

        8. #A = I | A #A

          and define #A as the smallest solution to the equation X = I | A X:

        9. #A::= the smallest { X || X = I | A X }.

          Note. In MATHS I write the set of x such that P as { x || P }.

          Kleene showed that by repeatedly applying the operation that replaces X by ( I | A X) we get closer and closer to #A in the obvious sense. So

        10. (K1): #A is the smallest value of X solving equation X=I | A X,
        11. (K2): Repeated substitution generates successive approximations to #A.

          K1 and K2 above give a paradigm for defining the meaning of any grammar. For instance, the grammar { L::= a L b | "". } has one definitionL::= a L b | ""., one defined_term "L" and two elements: "a", "b". We define the meaning of "L" to be M where M is the smallest set of strings such that the following equation is true:

        12. M = a M b | I.


        13. M= {c || for some x in M (c =a ! x ! b)} | I.

          The above gives a recursive process testing whether a string lies in M. It does not tell us how to find elements in M. By Kleene's work M is also the smallest fixed-point of the mapping g, where

        14. g(X) = a X b | I.

          So to find M we use the iterative process below to generate the Kleene Sequence( S(0). S(1), ...).

          1. S(0) = {},
          2. for all natural_numbers n, S(n+1) = g( S(n) ).

          The series gives successive approximations to M:
          1. S(0)={},
          2. S(1)= I | a{}b = I ,
          3. S(2)= I | a I b = {"","ab"},
          4. S(3)= I | a{"", "ab"}b = {"", "ab", "aabb"},
          5. S(4)= I | a{"", "ab", "aabb"}b = {"", "ab", "aabb", "aaabbb"},
          6. S(5)= I | a{"", "ab", "aabb", "aaabbb"}b = {"", "ab", "aabb", "aaabbb", "aaaabbbb"},
          7. ...

          (End of Net)

          It is intuitively obvious that these sets are tending toward a limit of
        15. M = { a^n ! b^n || n=0,1,2,... }

          Indeed M is a fixed point of g since M = g(M). Any proper subset of M is not a fixed point. The reason that the Ss seem to get closer to M is that as i tends to infinity we have to look at longer and longer strings to find a string in M that is not in S(i). Using a limit to define the meaning of grammar has been around in the literature for a long time (a bibliography is in section 6.7 of chapter 3 of my unpublished monograph). The fixed point definition came later and is similar to Scott's denotational semantics [ACM 86]. Fixed points, iteration, and topological spaces appear to be a vital part of the theory of software.


          XBNF is EBNF with a notation which can be used with other mathematical concepts and so more power. XBNF uses white space, bars ("|") and the symbol
          as in BNF. The "<" and ">" of the original BNF are used as relations and as parts of arrows and crosses. Parentheses "()" are used as they are in algebra. It adds "#" to mean any number of, including zero thus letting the brace symbols of EBNF be used for mathematical sets. The Ada EBNF symbols "[]" are used to show subscripts and bindings and so are not used for optional parts in XBNF. XBNF also has a standard dictionary that defines some simple functions: Ada EBNF { x } is #( x ) in XBNF and x #(x) is written N( x ) . [x ] in Ada EBNF is O(x ).

          Here is a comparison of BNF, Ada EBNF and XBNF:

           	BNF    	<number>::=<digit>|<number><digit>	[Naur et al 64]
          	EBNF   	number::= digit {digit}           	[ANSI 83 ADA]
          	XBNF	number::= N(digit)                	[Botting 9x]
          We take over the notation from section 2.3 above and add intersection (&) and complementation (~) by:
        16. A & B::={c || c ∈ A and c ∈ B},
        17. A ~ B::={c || c ∈ A and not ( c ∈ B) }.

          XBNF in XBNF

            This section is an XBNF dictionary describing XBNF
            1. XBNF_dictionary::= #( XBNF_definition | comment ).

              A dictionary has any number of definitions and comments.

            2. XBNF_definition::= defined_term definer XBNF_expression.
            3. definer::= colon colon equals,

              A definition has a definer between the term being defined and the expression defining it.

            4. XBNF_expression::=set_expression.

              In XBNF we are interested in sets of sequences:

            5. set_expression::= item | union | intersection | sequence | phase | element.

              A set_expression is either an item, or a union, or, ...

            6. item::= element | defined_term | "(" set_expression ")".

              An item is either an element (defined below), or a defined term, or any set expression in parentheses,

            7. union::= alternative #( "|" alternative ).

              A union has at least one alternative. Alternatives in a union are separated by vertical bars.

            8. alternative::= complementary_form | sequence.

              Each alternative is either a complementary_form or a sequence.

            9. sequence::= #phase.

              A sequence is a number of phases. The "number sign" (ASCII code hex(23), hash, sharp) shows the occurrence of any number of the next item - including none. A sequence can therefore be empty, one phase, or two phases, etc..

            10. phase::= ("#" | ) item.

              A phase is part of a sequence where an item occurs once, or the same item can occur any number of times including no times at all.

            11. intersection::= item #("&" item ),

              The ampersand character("&") shows that all the descriptions (items) must hold at once.

            12. complementary_form::= item "~" item,

              A complementary_form - A~B say - describes the set of As that are not Bs. Here is an example:

            13. comment::= (#character )~definition.

              Any number characters (in a dictionary ) that are not a definition form a comment. This paragraph is a comment in this XBNF dictionary.

                In a lexicon or lexical dictionary the following definition of element is used:
              1. element::=character_string | named_ASCII_char | function | natural_language_string,
              2. character_string::=quote #( char ~ (quote | backslash) | backslash char) quote,

                In MATHS the character names used in Ada are preferred

              3. named_ASCII_char::= See http://cse.csusb.edu/dick/samples/comp.ASCII.html.

                Here are some of the named ASCII characters:

                1. quote::="\"",
                2. backslash::="\\",
                3. colon::=":",
                4. comma::=",",
                5. equals::="=",

              Functions in XBNF

              A function call is written the usual way in XBNF. And the same form is used in defining functions:

            14. function::=identifier "(" List( arguments) ")",

            15. function_definition::= formal_parameters comma function definer expression

              Simple functions defined by non-recursive definitions do not change the expressive power but makes a practical difference. The following are a standard functions and can used in any lexical or syntactic dictionary:

              1. For all sets_of_strings x,
              2. List(x)= x #( comma x),
              3. non(x)= #char ~ x,
              4. N(x)= x #(x),
              5. O(x)= (x|).

              Introducing the ability to define and use syntactic functions allows context sensitive features to be handled elegantly and efficiently... See below.

              Another standard kind of element is the identifier. An identifier does not start or end with an underscore - it is made of letters, digits and break characters, and must always start and end with either a letter or digit:
            16. identifier::= ( (letter | digit ) #id_character ) & ( #id_character (letter | digit) ),
            17. id_character::=(letter | digit | underscore).

              Some identifiers are defined_terms:

            18. defined_term::= natural_identifier & defined |... .

              When the defined_terms are identifiers and the expressions have no intersections or complements then the dictionary is context free. The three dots (...) indicate that there a defined term can take other forms. A natural identifier is made up of words :

            19. natural_identifier::= word #(underline word) & (declared_identifier | defined_identifier | unknown_identifier).

              Words are either numbers or are made of letters. When made of letters they must be in a dictionary - either of a natural language or a special dictionary for the project,

            20. word::=number | ( (letter #letter) & in a dictionary ),
            21. number::=digit #digit,
            22. digit::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9".

              Rules for creating and using identifiers in general documentation are discussed in my monograph. Meanwhile note that it is common to have several names with one meaning - typically there is a mathematical variable or symbol (like "a", "+", "\λ", ...) which is used in formulae plus a longer natural_identifier .

            Often, a language is defined by two dictionaries - a lexicon that gives names to strings of symbols, and a syntactic dictionary or grammar. The grammar describes the structure of the language in terms of the tokens identified in the lexicon. In this presentation I combined both lexical and syntactic "shells" into a single presentation. Normally they would be split up into separate pieces of documentation - to do this I have experimented with a formalism that treats a dictionary as a module. This is described later. Meanwhile we will assume that the terms defined in the standard lexicon for the ASCII code can be used in future examples: thus terms like comma, r_paren, etc will be used in later syntax definitions.

            I would suggest that we extend EBNF to also be a glossary. A glossary definition is a definition in the form:

            1. term::=informal description.

            Syntactically define a glossary as a collection of these:
            1. glossary::=#( glossary_definition | comment )
            2. glossary_definition::= defined_term definer natural_language_string punctuation.

              So in a general piece of documentation a term may have two different definitions:

            3. natural_language_string::= back_quote #(non(back_quote)) back_quote,
            4. natural_language_string::=A description in a natural language of the meaning and/or purpose of something,
            5. back_quote::="`".

            A similar three level approach is useful in data processing applications - the analyst preparing a data dictionary that is equivalent to a lexical description of the data, the program designer working out the structures caused by logical and physical constraints, and a team thrashing out the glossary definition. It is possible and useful however to keep all definitions of a single term together rather than in separate files of sections of a document.

            The glossary definitions above should be used to make bridges between the notations being defined and other things. They should be used for designations in Michael Jackson's terms.

            Tools and Samples
            Such a three way approach has been tried out in class. Anybody with access to the World Wide Web can access documentation prepared this way for various subjects and classes. The HTML pages [ http://cse.csusb.edu/dick/samples/ ] and the searching tools are all generated by simple UNIX scripts that are available on the WWW as well [ http://cse.csusb.edu/dick/tools/ ]

            Cross-references and hyperlinks
            My notation allows dictionaries, grammars and glossaries to refer to each other.
            		.See URL
            My mth2html, define, and lookup commands take account of this feature. The effect is that the C++ syntax file inherits definitions from the C syntax plus a glossary of object oriented terms. The syntax inherits the definitions of the ASCII characters and the functions and notation in a meta- definition of EBNF. define always searches a general glossary of computer science. This is all transparent to the user.

            A recent addition is to allow a defined term to refer directly to part of (or the whole of) a document on the WWW:


            For example:

          1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html, refers to the standard definitions available to a person who uses MATHS.

          . . . . . . . . . ( end of section XBNF in XBNF) <<Contents | End>>

          Effect of Intersections

          The theory of defining a language as the intersection of a finite number of context free languages was developed by Liu and Weiner in 1973. For practical examples see: the Turing project [Holt & Cordy 88]. , S/SL, Jackson's work, etc.[Hehner and Silverberg 83]. Warnier's notation permits intersections but they are only used to derive conditions in programs. Intersections let us define languages that are not context free:
          1. L::=P&Q,
          2. P::= #a B,
          3. B::= O(b B c),
          4. Q::=A #c,
          5. A::=O(a A b).


        18. (B)|- (B1): B={b^m c^m || n=0..},
        19. (B1)|- (P1): P={a^n b^m c^m || n, m=0..},
        20. (A)|- (A1): A={a^n b^n || n=0..},
        21. (A1)|- (Q1): Q={a^n b^n c^m || n, m=0..},
        22. (P1, Q1)|- (L1): L={a^n b^n c^n || n=0..}.

          The last result (L1) shows that a dictionary with an intersection can describe a non-context free language. Since a complement of a union is the intersection of the complements the same effect can be got by permitting complementation and NO intersection. However this seems to be a useless restriction.

          Defining a language as the intersection of several grammatical constraints is neither new nor inefficient - Constrained Expressions are expressive and based on simple regular expressions [Dillon et al 86]. Hehner and Silverberg[83] use the term Communicating Grammars for a set of grammars with some terminals and non-terminals occurring in both. The model here is simpler - I propose the terms concurrent context free grammars (CCFG) for the dictionary model proposed here, and concurrent context free languages(CCFLs) for the family of languages defined by CCFGs. Hemendinger notes that Ada tasks have communication patterns that are CCFLs[Hemendinger 90]. Dictionaries with intersections define languages that are recognized by networks of parallel CFG acceptors. Psychologists use a network of "daemons" for modelling perceptual processes [ Human Information Processing, Lindsay & Norman, Pub Academic Press, 1970]. Finally: the hardest part of Jackson Structured Programming [JSP] is the use of semi-co-routines (in COBOL!) and to handle non-context- free problems by quasi-concurrency[Jackson 1975...].

          Effect of Functions

          Using functions in a grammar has the practical effect of letting us name and use short hand formulae for common constructions such as lists. However they permit the definition of context dependencies in a natural way. First we need a way to define a function and a way to express its image. The natural way to define simple functions is too allow the use a symbol like (_) as the place where the argument of the function must be written:
        23. List::= (_) #( comma (_) ),

          where List maps a set of strings into another set of strings. As in all mathematics a function has a domain and a codomain that are set:

        24. For function f, dom(f)::=the domain of f, and
        25. For function f, cod(f)::=the codomain of f. For each element in the domain there is precisely one in the codomain:
        26. For function f, x:dom(f), one y:cod(f), y=f(x).

          The image of a function F can be written post(F) - the set produced after F is applied to all the elements in it domain

        27. post(F)::= {F(x) || for some x }.


        28. pre(F)::={x || F(x) is defined }

          For example, if F is a map from the Positive_Integers into sets of strings defined by:

        29. F::=a^(_)b^(_)c^(_),


        30. (post, F)|-post(F) ={a^n b^n c^n || n=0..}.

          This technique leads to a way to express the context dependencies found programming languages. For example take the labelled loop in Ada. Suppose that loop_with_label is a function the maps identifiers into valid Ada loops:

        31. loop_with_label::= ( (_) ":" "loop" #( statement | "exit" (_) "when" condition ";" ) "end loop" (_) ";".

          (for example

        32. "SUM: loop x:=x+1/i; exit SUM when x>100; i:=i+1; end loop SUM"
        33. is a string in loop_with_label(SUM). )

          To be made precise the statement in the Ada grammar would also need to an argument representing the set of valid labels in internal loops.

          Now, this is a context dependent set of strings and yet the definition shows us a simple and efficient way to parse (and check the syntax) loops: First, use CFG a parser for

        34. loop::= ( label ":" "loop" #( statement | "exit" label "when" condition ";" ) "end loop" label ";".

          and check for the reoccurrence of label . Clearly functions get us to the level of attribute grammars. Indeed we can handle context dependent productions:

          Example ?? of context dependent XBNF


          In MATH '@' indicates the subsets of so we can define a complicated feature of a language in stages, first declare that it is a subset of a context free language and later provide the specific rules.
        35. Ada_loop::@ (label ":" "LOOP" #(statement|"EXIT"label"WHEN"condition";) "END LOOP" label ";").

        36. Here the "::" is split of from the "=" because it declares a new identifier but does not define a particular value. We can then express complex specifications and requirements one assumption or condition at a time.

          Combining intersection with functions is interesting. Suppose that we have already defined declaration(V), usage(V), and no_ref(V) as the strings in a language which (1) declare or introduce V, (2) make use of V, and (3) don't refer to V respectively then:

        37. valid_wrt::=#no_ref(_) declaration(_) #(usage(_) | no_ref(_) ),

          describes all sequences of components where the argument is declared before it is used - and is NOT re-declared. If we now define

        38. valid::= &valid_wrt,

          where the '&' is an intersection of all the valid_wrt(_) sets:

        39. (STANDARD)|-&F = { y || for all y (y in F(x) },

        40. then
        41. block::="begin" ( (statement # (";" statement )) & valid ) "end",

          defines a block with all its variables declared exactly once before they are used. This is a common context sensitivity in programming languages. Finally the '&'s in the definition imply that the parser would be structured as a number of parallel parsers, all with the same structure. This form concurrency is very easy to handle in both theory [Hoare 79 & 85] and in practice [Jackson 75, Andre Banatre & Routeau 81, Cameron 89].

          Definitions that include parameters are useful for defining and specifying maps and relations. Sets of definitions that include parameters are called Logical Grammars [ Abramson & Dahl 89 ]. A more general form of dictionary is the W-Grammar, or Two-level Grammar or Van-Wijngarten Grammar that contributed to the demise of Algol 68 yet is alive as a tool for documenting data structures[Gonnet & Tompa, Gonnet & Baeza-Yates 91]. The effect is that of a logic programming language [Ballance et al 90].

          Structural or Abstract XBNF

          In the theory of programming languages, some recent papers, in data bases, systems analysis and design, several programming languages, and in object oriented programming there is a need to describe the structure of something rather than its precise syntax. A very simple extension to XBNF allows it to describe abstract structures: Change the definition

        42. alternative::= complementary_form | sequence, to read
        43. alternative::= complementary_form | sequence | structure.


        44. structure::= base O("with" bindings).
        45. bindings::= binding #("&" binding),
        46. binding::=id_set | id ":" set | id:=expression | id:set=expression | predicate.
        47. base::=defined_term | universe.
        48. universe::= "logical" | "generic" | "standard" | "structure" | "syntax" | "semantics" | "abstract" | "algebra" | "ADT" | TBA.
        49. id_set::= name & defined_term & |[X:Sets]expression(X).

          An example is:

        50. List::= Atom | {Nil} | structure with car:List & cdr:List.

          which defines the structure of a LISP list. In a binding, an item like

          indicates that there is a map called car from the defined class structure with car:List & cdr:List to List.

          The optional base is used to get the effect of inheritance:

          1. Tree::= Leaf | Empty | structure with n:Number & branches:1..n->Tree,
          2. Binary_Tree::= Tree with n=2.

          1. Algebra::=standard with set:Sets,
          2. Semigroup::=Algebra with op:associative(set),
          3. Monoid::=Semigroup with u:unit(op),
          4. Group::=Monoid with inv:Set->Set & for all x:set(x op inv(x)=u).

          1. Person::standard,
          2. Student::=Person with major:Dept & GPA:Number ...
          3. Teacher::=Person with Dept & classes:@Class ...,

          1. Hypercard::structure,
          2. Object::=Hypercard with name:#char & id:Nat & Script,
          3. Script::=Text with Handlers,
          4. Stack::=Object with ....,
          5. Background::=Object with Stack & Graphic,
          6. Card::=Object with Background & Graphic,
          7. Button::=Object with type:{...}...,
          8. Card_Button::=Button with Card,
          9. Background_Button::=Button with Background,
          10. ...

          Predicates in a binding are essentially embedded intersections:
        51. B with P::={ b:B || P'} where P' has each id i is replaced by (b.i). We can interpret the following form:
          as a short hand notation for
           	term ::= base "with" bindings


          defines an object within the base universe, not a subset of it.

          This formal model of abstract structure can be used to model the kind of formal and semiformal documentation that we are used to seeing texts, papers, manuals, and scribbled notes [ Documentation] .

          Stretching too far

          Suppose XBNF permitted recursive definitions that involved the power set operator "@" where
        52. @X::={ S || S==>X }.

          Then we could write

          1. P::= A | @P

          for some finite set of Atoms A. This is only a little more complex than P=A| A P, or L= A|{Nil}|structure with car:L and cdr:L, or even P=A|#P.

          This definition leads to a paradox when we try to work out how big P is. The size(cardinality) of P is written |P|. Clearly

        53. |P| = |A| + |@P| = |A| + 2^|P|.

          However there is no number n such that:

        54. n = a+2^n.

          Indeed if P = A|@P then we would have a set that included a subset isomorphic to its power-set. Cantor has shown such sets to be impossible.

          Similarly when we use BNF to define function spaces:

        55. F::= Data | F->F

          We hit a similar paradox. Dana Scott replaces the above by

        56. F::=Date | (continuous)(F->F)

          and shows this to be consistent and meaningful.

          It seems wise therefore to not allow the use of '@X' (or X->) directly or indirectly to define 'X'. The normal mathematical forms can be used instead:

          1. Graph::=Algebra with F:set->@set & a:Data.

          In general recursive definitions have to be proved consistent - in the simplest case of BNF and EBNF we know that there are no paradoxes. Adding '@' in a simplistic manner leads to paradoxes indicated above.

          It can be shown however [ math_5_Object_Theory.html ] that when a set of equations can be modeled by an iteration of sets:

          1. X' = F(X)

          and this starts with a finite set of basic elements (F({})) and generates no more than a finite number of new elements each time, that the resulting set is countable -- isomorphic to a subset of the natural numbers. This means that the Cantor paradox does not arise. This approach is close to that taken by others

          Source: Date: Mon, 11 Mar 1996 11:45:00 -0600 (CST)// Message-Id: <199603111745.LAA26492@asia.cs.rice.edu>// From: Corky Cartwright <cork@cs.rice.edu>// To: dick@csci.csusb.edu (Dr. Richard Botting)// Subject: Re: Domains (was Re: CBS and Coq)

          Leverage and Reuse

          It is also possible to get a lot of leverage out XBNF style documentation by writing it in abstract rather than concrete terms. The most trivial example is the use of functional terms above.

          A more powerful form is to parameterize a complete set of documentation by indicating that certain terms are generic. There are two kinds of generic terms that are needed. The first are those supplied by the person who is reusing the documentation - call these "given". Then there are the terms that are constructed and made available by the documentation. Call these the "goals". The result can be called a template, generic or a lever.

          The syntactic extension is

          1. term::type= given.
          2. term::type= goal.

          A piece of documentation that has some terms defined as 'given' and others as 'goal' is called a lever.
        57. lever::documentation=document that has both given and goal terms.

          Semantically these do no more than declare the type of the term. However they imply that the document is designed to be reused with the given terms redefined and the goal terms generated as a result:

        58. Example::=following
          1. Set::Sets=given.
          2. PowerSet::Sets=goal.
          3. PowerSet=@Set.

        59. Example(Set=>Nat, PowerSet=>PNat)=following
          1. PNat::Sets= @Int.
          These levers are rather like C++ templates, SML functors, or Ada generics in allowing high quality work to be paid for across many projects. [ Reusable documentation ]


          We can extend BNF until it becomes a general tool for defining sets of things. However we must be careful to interpret the sets as being defined by finite processes only if we want to avoid paradoxes. It also possible to write sets of definitions and assumptions in a way that looks and feels like traditional mathematical presentations, and then "compile" these into a more abstract but equivalent system.

        . . . . . . . . . ( end of section Grammars and Dictionaries) <<Contents | End>>


          Dictionaries in Abstract

          Abstract models are easier to re-use than concrete ones. Any system that fits the theory of strings plus regular sets(A semiring with Kleene closure ) can use a similar kind of dictionary to those described above. This part of my presentation is a quick tour of such areas.


          Abstract models are easier to re-use than concrete ones. Any system that fits the theory of strings (a monoid) plus regular sets(A boolean algebra) with kleene closure can use dictionaries. The grammar can be put to work to describe files in terms of data in stead defining languages in terms of characters. The equivalence of a lexical dictionary is the analysts "data dictionary". The counterpart of the syntactic grammar is a Jackson or Warnier "data structure". All we need is an empty object and a concatenation operator. For example if T stood for a set of records and #T for files, then the empty string models the empty file (UNIX /dev/null) and concatenation models writing one file after another (UNIX: cat a b >c).


        1. magnetic_tape::=label #file end_of_tape_marker,
        2. file::=header #data_block sentinel.

          These define the magnetic tape's physical structure. If we were designing a program to process a file of student records we might describe a file sorted by sections as follows:

        3. file::=#section,
        4. section::=class_header #student,
        5. student::=A_student | student~A_student.

          Strictly speaking a definition of form

           	A::= B | A~B
          is a theorem |-A = B | A~B.

          If the domain has the words "file", "section" and "student" we use a similar structure, even if the class header is absent and a student record identifies the student's class instead. The result is called a logical structure.

        6. file::=#section,
        7. section::=#student,
        8. student::=A_student | student~A_student.

          If the problem is to summarize the data on each section then we might show the output as:

        9. output::= header_page #section_summary college_summary,

          and note that each section corresponds to exactly one section_summary and the input corresponds to the output. It is easy to combine these into one abstract structure:

        10. consume_file_and_produce_output::= produce_header_page # consume_section_and_produce_section_summary produce_college_summary.
        11. consume_section_and_produce_section_summary::= # consume_student
        12. consume_student::=consume_A_student | consume_non_A_student.

          The structure above becomes a program when operations and conditions are added (see my monograph or any good JSP book).

          A data dictionary is free of semantic and pragmatic structures because a file can be used for many purposes and hence is parsed into different structures. Typically:

        13. free_file::=# record,
        14. record::=type1 | type2 | type3 | ...,

          Now if a,b,c,... are elements then

        15. F::=#(a | b | c | ... ),

          is the free semigroup or unstructured structure. In categorical terminology this is a free, initial, or universal repelling object in the category of semigroups with units. Free dictionaries are the weakest useful dictionaries. In consequence a design that has two or processes that communicate by consuming and producing strings(files) can interpret or structure the files as they wish. This is the powerful form of information hiding that is implicit in Jackson's work.

          Data dictionaries can show a non-programmer what a program is expected to do in their own terminology not computer jargon. The canonical grammar/dictionary /glossary shows the user or client that we understand all their terminology. Canonical diagrams and dictionaries show how the user's data is handled in terms that the users and clients understand. The test of a canonical dictionary is that clients and users certify it as complete and accurate. Canonical dictionaries are the strongest useful dictionaries.


        16. Functions (in the pure mathematical sense) are a part of most software systems. Because they are there we need some simple conventions that let them be defined very easily. The result is close to the MIRANDA language developed in the United Kingdom[ ??] . The key idea is a simplification of the λ notation. In the λ notation a variable is introduced to indicate the value to which the function is to be applied. For example if we use the key- word 'map' to indicate such an expression we might write:
        17. double::= map[x] (x+x).
        18. square::= map[x] (x*x).
        19. cube::=map[x] (x*square(x)).
        20. ....

          These imply

        21. cube(double(square(2)))=cube(double(4))=cube(8)=8*square(8)=8*(8*8)=8*6 4=512.

          However, simple maps can be written with a constant blank space symbol (_) instead of the variable x:

        22. double::= (_)+(_).
        23. square::= (_)*(_)
        24. cube::=(_)*square((_)).

          As an immediate application are the STANDARD definitions of the syntax functions mentioned in the previous section:

        25. #::=( (_) #((_)) |).
        26. L::= (_) #( comma (_)), L::=List of (_).
        27. P::= l_paren L((_)) r_paren, P::=Parenthesized list of (_).
        28. non::= char ~ (_).
        29. N::= (_) #((_)), N::=Many (_).
        30. O::= ((_)|), O::=Optional (_).

          So if we wrote

        31. some_map::=(_),

          then some_map(x) = x. So, (_) must represent the identity map. Extend this line of thought further. Putting any function in an expression where a value is expected and we get an expression for a function instead of an expression of a value. So if g maps into the domain of f then

        32. f(g) = map[x](f(g(x)).

          If 1st, 2nd, 3rd, 4th, ... n.th ... are maps from n-tpls into their components:

        33. 1st(a,b,c,...)=a,
        34. 2nd(a,b,c,...)=b,
        35. ...

        36. then
        37. power::= (1st)^(2nd),

          implies that

        38. power(3,2) = (1st(3,2))^(2nd(3,2)) = 3^2 = 9.

          The result is a notation like the command line arguments in a C program, a UNIX shell script, ICL George 3 Macros, ... The same simple approach, starting with simple operations like successor (succ), predecessor(pred), and a constant zero(0) lets us develop the Peano arithmetic in EBNF_like definitions:

        39. +::= (2nd)=0; (1st) |(2nd)<>0; succ((1st))+pred((2nd)).
        40. *::= (2nd)=0; 0 | (2nd)=1; (1st) |(2nd)>1; (1st)+((1st)*pred(2nd)).
        41. ^::= (2nd)=0; 1 | (2nd)=1; (1st) |(2nd)>1; (1st)*((1st)^pred(2nd)).

          Here the semicolon acts like "if_then_": (;)=if (1st) then (2nd) but is actually the relational product described next.

          I have shown that BNF definitions can define functions in a natural way.

          Further if 1st and rest map a string into two parts so that x=1st(x)!rest(x), then

        42. reverse::=""+>"" | (strings~""); ( reverse((rest)) ! (1st) ).

          Binary Relations

          A relation R in @(T1,T2) can be defined in terms of a well formed formula W(x,y) by
        43. R::@(T1,T2)= W((1st), (2nd)).

          or any of the following forms

        44. For x:T1, y:T2, x R y::@= W(x,y).

          Given two binary relations R and S then For R: @(T1,T2), S:@(T2,T3),

        45. R; S::= for some z:T2 ((1st) R z and z S (2nd)),
        46. R; S::= The relation between x and y such that for some z, x R z S y,

        47. R | S::= (1st)R (2nd) or (1st) S (2nd),
        48. R | S::= `The relation between x and y such that either x R y or x S y`,

        49. R & S::= (1st)R (2nd) and (1st) S (2nd),
        50. R & S::= The relation between x and y such that both x R y and x S y.

        51. R ~ S::= (1st)R (2nd) and not (1st) S (2nd).
        52. R ~ S::= `The relation between x and y such that both x R y and not x S y`.

          /R is the converse relation to R. For example (_^2) is the 'square' function and /(_^2) is the square root relation, Similarly sin is the sin function and /sin includes the arcsin function. Further we want /parent_of=child_of. Therefore define:

        53. For R:@(T1,T2), /R::@(T2,T1)= (2nd) R (1st).

          In context, a set can also be used as a relation:

        54. For A:@T, A::@(T,T)=(1st) in A and (1st)=(2nd).

          Complex situations can be defined quickly using these notations in and EBNF- like way see [ rjb95a.Relations.vs.Programs.html ]

          Bindings and Schemata

          Nets are collections of assumptions not programs. Associated with a set of declarations is an abstract space. A declaration adds a dimension to the space and an equality removes a dimension. In consequence a definition that does not involve recursion leaves the system unchanged. Some recursive forms invalidate their universe but others(for example LISP) has a BCNF which is not recursive form. See [ Stretching too far ] above.

          Each document, package, or net can be have the formal content extracted and assembled into a binding:

        55. binding::="[" List( id ":" set | predicate ) "]".

          The extraction and assembly process being like compilation.

          Bindings are used in many other formula:

        56. map [ x:X, y:Y ] ( x^2+y^2).

          MATHS borrows an idea from the Ada package and the Z schema: networks can be named.. The original BNF notation is appropriate:

        57. NAME::= following
        58. .Box
        59. ...
        60. .Close.Box For example
        61. MONOID::=following
          1. 0::S.
          2. +::S><S->S.
          3. |- (assoc): For x,y,z:S(x+(y+z)=(x+y)+z).
          4. |- (zero): For all x:S( x+0=0+x=x).

          Nets are not interpreted as logic program. In many ways they can thought to define algebraic systems rather than a program,... indeed in most of these system the Unification Algorithm is not a valid deduction. MATHS provides the ability to show that the uncertain statements must follow from less doubtful ones. A special sign (|-) shows that the formula is either assumed or else that it can be derived from previous formulae. A complete inference engine or automatic theorem prover will be an uneconomic investment since the engineer can work interactively with a simpler proof checker. A proof typically has a Natural Deduction form like like the following, or an algebraic "Calculational" proof as praised by Shnieder and Gries.

          Sample Proof

          1. |-MONOID.
          2. (above)|-For all z:S, if for all x:S(x+z=x) then z=0
          3. Let{
          4. |- (1): z:S.
          5. |- (2): for all x:S(x+z=x).
          6. (2, x=>0)|- (3): 0+z=0,
          7. (zero)|- (4): 0+z=z
          8. (3, 4, Euclid)|- (5): z=0.
          9. }.

          [ logic_2_Proofs.html ]


          Documentation is an important part of software - but is often neglected. I believe that it needs to an integral part of any software development process. It is used by clients to ensure the get what the ordered, by customers to find out how to do things (where the HCI fails to be explicit), and by our colleagues when maintaining, modifying, correcting, reviewing, or reusing, or replacing our work.

          It would be good to have a standard ASCII notation for writing down our ideas as long as it was easy and natural to use. Given the notations developed so far I think this is possible. Further in many cases one can create tools that translate this notation in other equivalent forms for different readers:

          1. Tables -- For engineering complex systems
          2. Figures -- To get an overall picture of relationships
          3. Natural -- For "normal" people
          4. TeX -- For mathematicians and publishers
          5. HTML -- For online documentation

          All formal documentation techniques so far have one of two opposed failings. When mathematically powerful they are not expressible easily in ASCII. When expressible in ASCII they are an extension to a programming language rather than a mathematical model. Only "Spec" [ Berzins & Luqi ?? ] is both sophisticated and in ASCII.

          My attempt at solving this is to suggest that documentation has comments and more formal parts. The formal parts have precisely three kinds of element:

          • Declarations of variables
          • Definitions of terms
          • Well-formed-formulae
          These map into bindings, and so into descriptions of abstract structures.

          he detailed syntax is less important than the simple idea that documentation is itself a kind of more-or-less formal data. However I have developed several experimental syntaxes. One of these is documented in [ intro_documentation.html ] , . . . [ notn_00_README.html ] , . . . [ notn_10_Lexicon.html ] , . . . [ notn_11_Names.html ] , . . . [ notn_12_Expressions.html ] , . . . [ notn_13_Docn_Syntax.html ] , . . . [ notn_14_Docn_Semantics.html ] , . . . [ notn_15_Naming_Documentn.html ] , . . . [ notn_2_Structure.html ] , . . . [ notn_3_Conveniences.html ] , . . . [ notn_5_Form.html ] , . . . [ notn_8_Evidence.html] .

          Reusable documentation

          I have developed a calculus for constructing packages of documentation. They can be used in many ways - sets of object, proofs, data description, logistic systems, notes, ... [ notn_4_Re_Use_.html ]

          Thus EBNF has become a way to document mathematical and logical systems:

        62. PEANO::=
          1. Natural_numbers::Sets,
          2. succ::Natural_numbers->Natural_Numbers,
          3. 0::Natural_numbers.
          4. pred::(Natural_numbers~{0})->Natural_Numbers,

          5. |- (Axiom 1): pred(succ)=(_).
          6. |- (Axiom 2): For all n:Natural_numbers~{0} ( succ(pred(n)) = n ).
          7. |- (Axiom 3): For no n:Natural_numbers ( succ(n)=0 ).
          8. ...
          9. 1::= succ(0).
          10. <::= ((1st)=0) & ~( (2nd)= 0) | pred(1st)<pred(2nd).
          11. (above)|-ORDER( Set=> Natural_numbers, Relation=>(<) ).
          12. >::= (2nd)<(1st).
          13. <=::= <|=.
          14. >=::= >|=.
          15. ...
          16. |- (Axiom 4): For all S:@Natural_numbers, one n:S, all m:S ( n <= m).
          17. ...
          18. +::= (2nd)=0; (1st) | ~((2nd)=0); succ((1st))+pred((2nd)).
          19. *::= (2nd)=0; 0 | (2nd)=1; (1st) | (2nd)>1; (1st)+((1st)*pred(2nd)).
          20. ^::= (2nd)=0; 1 | (2nd)=1; (1st) | (2nd)>1; (1st)*((1st)^pred(2nd)).
          21. ...


          Once named and filed these systems can be referred to in other documents. For example, a group inherits the structure of a semigroup or monoid:

        63. GROUP::=

          1. |- (monoid): MONOID.
          2. m::=Inversion operator::S->S.
          3. |- (inverse): For all x:S( x+m(x)=0 ).


          The effect is to formalize what mathematicians have always done and simultaneously introduce inheritance into computer documentation. I have converted most of my notes on algebra and topology into this form on a 7K floppy disk.

          Here is an example of a practical application based on a recent publication:

          Source: [Snyder 93, Alan Snyder<alan.snyder@eng.sun.com>, The Essence of Objects: Concepts and Terms, IEEE Software V10n1(Jan 93)pp31-42]

        64. OBJECTS_0::=
            All objects embody an abstraction. Objects provide services. Clients issue requests. Objects are encapsulated. Requests can identify objects. New objects can be created. Operations can be generic. Objects can be classified in terms of their services. Objects can have common implementations. Objects can share partial implementations.


          We proceed by abstracting noun phrases from these sentences and replacing them by sets and relations:

        65. OBJECTS_1::=
          1. Objects::Sets,
          2. Abstractions::Sets,
          3. Services::Sets.
          4. embody:: Objects>->Abstractions, All objects embody an abstraction.
          5. provides:: @(Objects, Services),
          6. provides=(1st) provides (2nd) Objects provide services.
          7. ...


        . . . . . . . . . ( end of section Applications) <<Contents | End>>


        By extending EBNF to XBNF and then to MATHS we get a powerful way to document the domain in which software is or will be operating. "An application domain system model of the equipment and its intended environment of use is defined. This is a dynamic system model, and defines the overall states of the system as functions of time. Requirements are constraints on this model" [Hansen Ravn & Rischel 91 ]. Simple mathematics - sets, mappings, relations, definitions, assertions, etc.-

      1. can define important ideas. However, it takes time and experience to use the simple ideas effectively.

        MATHS is more abstract than any programming language. It is designed to be too powerful for any conceivable computer to use as a programming language because the language used at the sharp end of a project must be able to define problems well enough so that we can recognize that they are (1) hard, or (2) not computable. Problems of efficiency, computability, data vs algorithms, etc. are handled as part of the implementation. The MATHS description of the problem and the specification of a requirement should be independent of all implementations and technology. Ignoring efficiency etc. is difficult at first. It is essential to describe the purpose and qualities of something before choosing or testing techniques. Hence:

        • Formulae are descriptive, clear, and correct. Efficiency comes later.
        • Formulae specify results and properties but do not over determine an algorithm or data structure.
        • Some formula look like programs but they often take intelligence to interpret and/or code them.
        • Some formula can be implemented as data or program.

        MATHS & XBNF help solve several outstanding problems in the software process. First, we can show how the user's data is handled in terms that they understand. We can guarantee that this understanding is accurately modeled in the software by using rigorous design techniques. Second, Strachey pointed out the need to discover data structures before attempting functional design [Strachey 66]. The sets and maps found by formal analysis connect facts to conceptual data structures. Standard data base and data structures techniques can then implement the conceptual solution to the problem.

        Projects that use MATHS can "zero-in" on the best software. First: Define things that appear in the description of the problem and (1) are outside the software, (2) interact with the software, and (3) are individually identifiable by the software. Second: Define events, entities, identifiers, relationships, attributes, facts, and patterns. These steps are an exercise in stating the obvious. Facts are recorded and verified by experts and by observation. Simple facts lead to validation of algorithms, data structures, and data bases.

        If a system interacts with another system then it will have an internal model of the external system. An abstract model of the external system is a model for the internal system and so a structure for a design. Computer Science already teaches the techniques to implement the designs plus the calculus of sets, maps, and relations. So software design can be based on science. There is also a natural graphic representation (TEMPO). This is a basis for Software Engineering.



            Place in the Software Process

            This summarizes the notation (MATHS) I have developed for encoding discrete mathematics in ASCII so that software engineers don't have to make an investment in new hardware and software to do formal methods. It was developed to fit with notations that are already in use and to take advantage of programming language knowhow whenever possible. A formal definition has been developed and has been submitted to a series of publishers. I keep an online summary, dictionary etc in a directory called "maths" in my home directory on the World Wide Web, see [ http://cse.csusb.edu/dick/maths/ ] or (FTP) [ http://www.csci.csusb.edu/dick/maths/ ]

            Formal Analysis proceeds by stating the obvious and so certain truths. Simple facts often delimit the set of logically correct structures. Grammars and dictionaries are used to document the data and dynamics of a domain. Relations can specify processes in a structured dictionary. Sets and maps define entity types, abstract data types, and classes of objects of the problem domain and are used to document requirements and specifications. When implemented, maps become paths through the data structures and data bases. So they define the structure shared by solution and problem.

            Project documentation also describes the physical constraints caused by the technology used. Again there are two extremes: free and inconsistent. Some where between them is the best level. This records every assumption that can be made about the implementation technology. It is the canonical documentation of the technology being used when the software engineers are its clients and users.

            Levels of Documentation

            Some documentation says too little, and some says too much. Intuitively we have a category of logical systems. In this category of documentation we can distinguish two extremes. There is a free, initial, or universal repelling object in the category of documented objects. Free or initial documentation is the weakest useful documentation. At the other extreme there are final, inconsistent, or universally attractive documentation - this overdefines the situation to the point where it can not exist. In between there is the level of documentation that reflects exactly what the client understands the situation to be. I call this the canonical documentation. It forms the cannon or Bible for the project. It shows the user or client that we understand all their terminology. Canonical documentation shows the user's world in terms that the users and clients understand. The test of canonical documentation is that clients and users certify it as complete and accurate. Canonical documents are the strongest useful conceptual documentation.

            This annex summarizes the notation I have developed to express discrete mathematics in ASCII.

          . . . . . . . . . ( end of section Introduction) <<Contents | End>>

          Propositions and Predicates

          A proposition can have two possible meanings - true and false. In MATHS the symbol @ represents the Boolean type with two standard values {true, false}. [ logic_10_PC_LPC.html ]

          Equality is a special predicate that is defined for all universes of discourse. It is symbolized by "=". "<>" is (as in Pascal and BASIC) used for "not equal". [ logic_11_Equality_etc.html ] .Proofs [ logic_2_Proofs.html ]


          [ Sets in home ]

          Lists, strings and n-tupls

          [ More Advanced topics in Logic in home ]

          Classes & Entities

          [ Types in home ]

        . . . . . . . . . ( end of section Appendix) <<Contents | End>>

        Footnote {2}

        When one process generates the input to another parallel process it is not clear whether an empty input is merely as yet ungenerated data, or if the generator has terminated.


        [ Cantor's theorem ]

      . . . . . . . . . ( end of section Body of Paper) <<Contents | End>>

    . . . . . . . . . ( end of section How Far Can EBNF Stretch?) <<Contents | End>>