**Beyond PROLOG:**
**Software Specification by Grammar**

**Walter W. Wilson**
**The University of Texas at Arlington**

**1. Introduction**

In the programming language PROLOG, one writes software by functionally specifying it in a form of logic [Bowen 79, Kowalski 79]. This paper proposes a language similar to PROLOG in which software is specified by a type of grammar that generates hierarchical expressions. This language, which is called "axiomatic language", was developed with the following objectives:

1. **very high level** -- It should be a formalism for functionally
specifying software without specifying an implementation -- the programmer
tells the computer what to do without telling it how to do it [Wulf 80].
The programmer's task is simplified since the implementation details are
assumed by the (intelligent) language processor. Furthermore, the
resulting programs are more comprehendible since they are pure functional
specifications without implementation information.

2. **minimal** and **extensible** -- It should be a "minimal"
language, instead of large and complex, yet capable of defining any computable
function in a way that is clear to the human user. The arguments
in favor of simple, elegant languages as opposed to complicated ones have
been well stated by computer scientists [Dijkstra 72, Backus 78].
A language that is minimal must of necessity be extensible; that is, those
needed capabilities which are not built-in must be easily definable and
then as easily usable as if they had been built-in. Extensibility
means that one can reuse previously defined software components in the
definition of new software -- an important requirement for improved software
productivity.

3. **metalanguage** -- It should enable one to define arbitrary
language constructs, which can then be used as tools in the specification
of software. Different languages have a variety of features suited
to different problems. The ideal language would be one capable of
simulating, and thus incorporating the advantages of, any other language.
With such a metalanguage capability, one could not only define any computable
function, but one could define it in nearly any way. The programmer
could express a function in whatever formalism that is most suitable by
accompanying it with a definition of the syntax and semantics of that formalism.
A language with this property would be general purpose, yet would allow
the programmer to define useful specialized language constructs for particular
applications.

PROLOG is a very high level language and is simple and extensible. Since axiomatic language uses the same basic construct as PROLOG, it shares these properties. Axiomatic language, however, can also function as a metalanguage, allowing one to define arbitrary syntactic and semantic forms for the specification of software. This is claimed as its primary advantage over PROLOG.

Section 2 defines axiomatic language
as an abstract formal system and section 3 gives examples of its use and
merits. Section 4 shows how this formal system is interpreted, with
programs defined in a more nonprocedural manner than in PROLOG. Section
5 defines a proper subset of axiomatic language, called primitive axiomatic
language, which has the same power, and section 6 gives conclusions.

**2. Axiomatic Language**

In axiomatic language a function or program is specified by a finite set of "axioms", which generate a (usually) infinite set of "valid expressions", analogous to the way productions in a type-0 grammar generate strings or the way axioms in logic generate theorems. An "expression" is defined to be

an "atom" -- an abstract, primitive element,

an "expression variable",

or a "sequence" of zero or more expressions or "string
variables".

This differs from PROLOG with the addition of string variables and a different hierarchical structure, adopted from functional programming [Backus 78].

An atom is represented syntactically by a symbol consisting of letters, digits, and special characters: X3, +. Expression and string variables are represented by symbols preceded by '%' and '$', respectively: %expr, %x, and $str, $1. A sequence is represented by a string of expressions and string variables, delimited by blanks and enclosed in parentheses: (M %y), (abc () $2 (*)). It should be mentioned that these syntax details are somewhat arbitrary.

An axiom consists of zero or more "condition" expressions followed by a "conclusion" expression:

if <cond1> and <cond2> and ... and <condn> then <conclu>.

where the <cond> are the condition expressions and <conclu> is the conclusion. If there are no conditions, the axiom is represented '<conclu>.'. Long axioms may be written in free format over multiple lines to improve readability and a comment may be written on the right side of a line, following a dash. This syntax can be compared with the corresponding PROLOG syntax:

<conclu> :- <cond1>, <cond2>, ..., <condn>.

where the conditions come after the conclusion. The difference is just a minor issue. The syntax used in this paper is considered more representative of the way people think.

A finite set of axioms generates valid expressions by first generating an infinite set of axiom "instances" through the substitution of values for the expression and string variables. Each occurrence of an expression variable in an axiom can be replaced by an arbitrary expression, the same expression replacing the same variable throughout. Likewise, each string variable can be replaced by a string of zero or more expressions and string variables. For example, the axiom

if (A %x) and ($str1 B $str2) then (C $str1 %x $str2).

has an instance

` if (A (%y)) and (* $str B) then (C * $str (%y)).`

by the substitution of '(%y)' for %x, '* $str' for $str1, and '' (the null string) for $str2.

The generation of valid expressions from axiom instances is governed by the simple rule that if all the conditions of an axiom instance are valid expressions, then the conclusion is a valid expression. By definition, the conclusion of an "unconditional" axiom is automatically a valid expression. For example, the two axioms

` (a b).
-- an unconditional axiom`
` if (%expr $str) then ((%expr) $str $str). -- a conditional
axiom`

generate the valid expressions (a b), ((a) b b), (((a)) b b b b), ....

**3. Some Examples**

This section shows how the simple formal system defined above is used to specify functions. In section 3.1 axiomatic language is used to define natural numbers and their addition and multiplication. In section 3.2 the very high level nature of axiomatic language is illustrated by using it to define sorting -- not by an algorithm, but by a formal definition of what sorting is. In section 3.3 axiomatic language is used as a metalanguage to define the syntax and semantics of a small language in which software can be specified. The examples presented are written in a somewhat "wordy" style to show how axiomatic language can be made self-documenting.

**3.1 Natural Number Arithmetic**

One defines a function in axiomatic language by using axioms to generate valid expressions for each combination of arguments and results. This is illustrated by the familiar inductive definitions of natural number arithmetic. Natural numbers can be represented by strings of asterisks:

` (() is a natural number).
-- zero is a natural number`
` if (($I) is a natural number)
-- if I is a natural number`
` then (($I *) is a natural number).
-- then so is I's successor`

These axioms generate valid expressions such as '((* * *) is a natural number)', which represents the statement "3 is a natural number". Note that the symbols 'is', 'a', 'natural', and 'number' are all abstract atoms with no inherent meaning -- they simply serve for self-documentation. The addition of natural numbers is defined by the following axioms:

` if (%I is a natural number)
-- if I is a natural number`
` then (%I plus () equals %I).
-- then I + 0 = I`
` if (%I plus ($J) equals ($K))
-- if I + J = K`
` then (%I plus ($J *) equals ($K *)).
-- then I + (J+1) = (K+1)`

These axioms generate expressions such as '((* * *) plus (* *) equals (* * * * *))', which says that "3 + 2 = 5". Of course, the mathematical symbols '+' and '=' can be substituted for the words 'plus' and 'equals'. The multiplication of natural numbers is similarly defined:

` if (%I is a natural number)
-- if I is a natural number`
` then (%I times () equals ()).
-- then I * 0 = 0`
` if (%I times ($J) equals %K)
-- if I * J = K`
` and (%K plus %I equals %L)
-- and K + I = L`
` then (%I times ($J *) equals %L).
-- then I * (J+1) = L`

The definition of other numeric data types and operations is done in a similar way. One can also define decimal digit representations for numbers, such as '((3 5) times (1 8) equals (6 3 0))', where the digits are abstract symbols. As a further convenience, a syntactic rule could be adopted allowing one to write numbers as, for example, '1234', in place of the expression '(1 2 3 4)'.

**3.2 Sorting**

As stated earlier, the objective of very high level languages is to allow one to define what a program does without specifying how it does it. The very high level nature of axiomatic language can be illustrated by the problem of sorting. There are many algorithms for sorting, but they all deal with how to sort. In axiomatic language, sorting is defined by formally specifying what it is. A sort of a sequence of elements can be defined as a permutation of that sequence such that the resulting sequence is ordered in some way. This is formally stated by the following axiom:

` if (%y is a permutation of %x) and (%y is ordered)`
` then (the sort of %x is %y).`

The permutation relation for arbitrary sequences is defined as follows:

` (() is a permutation of ()).`
` if (($str1 $str2) is a permutation of ($str3 $str4))`
` then (($str1 %expr $str2) is a permutation of
($str3 %expr $str4)).`

The ordering predicate as it applies to sequences of arbitrary expressions is defined from the binary relation '<=':

` (() is ordered).
-- the empty sequence is ordered`
` ((%expr) is ordered).
-- so is a sequence of one expression`
` if (($X1.. %Xn) is ordered) -- if the
sequence X1 .. Xn is ordered`
` and (%Xn <= %Xn+1)
-- and Xn <= Xn+1`
` then (($X1.. %Xn %Xn+1) is ordered). --
then X1 .. Xn+1 is ordered`

The '<=' relation is defined from the '<' relation:

` (%expr <= %expr).
-- an expr is less than or equal to itself`
` if (%x < %y) then (%x <= %y).`

The '<' relation for natural numbers is defined as follows:

` if (($I) is a natural number)
-- if I is a natural number`
` then (($I) < ($I *)).
-- then I < the successor of I`
` if (%I < %J) and (%J < %K) then (%I < %K).`

These axioms generate expressions such as '(the sort of ((* * *) () (*)) is (() (*) (* * *)))', which states that the sort of (3 0 1) is (0 1 3). This definition of sorting is simpler and clearer than any algorithm one could write in a conventional language. Furthermore, it has the advantage of being "generic". It automatically applies to any data type for which the '<' relation is defined. In section 4.1 the sorting of character strings is illustrated.

**3.3 Definition of Language Semantics**

Used as a metalanguage, axiomatic language enables one to define the syntax and semantics of arbitrary language constructs, which can then be used as tools in the specification of software. One can thus express functions and programs in whatever formalism that is most suited to the problem. One can even define the syntax and semantics of an entire language and then write software in the language. In this section a small language is defined that allows one to specify functions of natural numbers algorithmically. As an example, the factorial function is specified by the following algorithm, represented as an unconditional axiom:

` (function FACTORIAL (N) is`
` variables I FACT ;
-- list of local variable names`
` begin
-- arguments & local variables are untyped`
` I := () ;
-- = 0`
` FACT := (*) ;
-- = 1 (= 0!)`
` while I < N loop
-- loop until I = N`
` I := I + (*) ;
-- increment I`
` FACT := FACT *
I ; -- FACT := I!`
` end loop ;`
` end FACTORIAL return FACT).
-- since I = N, FACT = N!`

The axioms presented below define a language that generates, from this unconditional axiom, valid expressions such as '(FACTORIAL (* * *) equals (* * * * * *))', which states that 3! = 6. Other natural number functions can be similarly defined in this language using algorithms expressed as unconditional axioms. The "top level" axiom defining this language is the following:

` if (function %fn_name ($arg_names) is -- function
name, arg names`
` variables $loc_names
; -- local
variable names`
` begin`
` $stmts
-- algorithm statements`
` end %fn_name return $result_expr)
-- result of function`
` and (length ($arg_names) = length ($arg_vals)) --pair
names & values`
` and (executing ($stmts) with vars ($arg_names $loc_names)
and initial`
` state ($arg_vals $dummy_vals)
yields final state %final_vals)`
`
-- local variables initially have arbitrary dummy values`
` and (expr ($result_expr) with vars ($arg_names $loc_names)
having`
` values %final_vals equals
%result) -- evaluate the result`
` then (%fn_name $arg_vals equals %result). --
generate valid expr`

The length predicate used in the above axiom is defined as follows:

` (length () = length ()).`
` if (length ($str1) = length ($str2))`
` then (length ($str1 %expr1) = length ($str2
%expr2)).`

The syntax and semantics of statements are defined by valid expressions of the form "(executing <statements> with vars <variable names> and initial state <variable values> yields final state <variable values>)". Each name in the sequence of variable names is paired with a corresponding value in the sequence of variable values. The axioms that generate these expressions are as follows:

-- sequentially executed statements: <stmts1> <stmts2>

` if (executing ($stmts1) with vars %names and initial
state %vals1`
` yields final state %vals2)`
` and (executing ($stmts2) with vars %names and initial state
%vals2`
` yields final state %vals3)`
` then (executing ($stmts1 $stmts2) with vars %names and initial
state`
` %vals1 yields final
state %vals3).`

-- assignment statement: <var_name> := <expr> ;

` if (expr ($expr) with vars ($names1 %name $names2) having
values`
` ($vals1 %old_val
$vals2) equals %new_val)`
` and (length ($names1) = length ($vals1)) -- pair var
name with value`
` then (executing (%name := $expr ;) with vars ($names1 %name
$names2)`
` and initial
state ($vals1 %old_val $vals2)`
` yields final state
($vals1 %new_val $vals2)).`

-- while loop: while <condition> loop <stmts> end loop ;

` if (expr ($cond) with vars %names having values %vals equals
false)`
` and (executing ($stmts) with vars %names and initial state
%vals1`
` yields final state %vals2)
-- make sure skipped stmts are legal`
` then (executing (while $cond loop $stmts end loop ;) with
vars %names`
` and initial state %vals yields final state
%vals). --loop 0 times`

` if (expr ($cond) with vars %names having values %vals1 equals
true)`
` and (executing ($stmts) with vars %names and initial state
%vals1`
` yields final state %vals2)
-- loop 1 ..`
` and (executing (while $cond loop $stmts end loop ;) with
vars %names`
` and initial state %vals2 yields
final state %vals3) -- or more`
` then (executing (while $cond loop $stmts end loop ;) with
vars %names`
` and initial state %vals1 yields
final state %vals3). -- ..times`
`
-- note that loops must terminate to be defined`

The syntax and semantics of expressions are defined by valid expressions of the form "(expr <expression> with vars <variable names> having values <variable values> equals <expression value>)". The axioms are as follows:

-- <expr> ::= <expr> + <expr> | <term>

` if (expr ($expr1) with vars %names having values %vals
equals %num1)`
` and (expr ($expr2) with vars %names having values %vals
equals %num2)`
` and (%num1 plus %num2 equals %num3)`
` then (expr ($expr1 + $expr2) with vars %names having values
%vals`
` equals %num3).`

` if (term ($term) with vars %names having values
%vals equals %num)`
` then (expr ($term) with vars %names having values %vals
equals %num).`

-- <term> ::= <term> * <term> | <primary> (similar to <expr>)

-- <primary> ::= <name> | <constant>

` if (length ($names1) = length ($vals1)) -- pair
var name with value`
` then (primary (%name) with vars ($names1 %name $names2)
having values`
` ($vals1
%val $vals2) equals %val). -- value of a variable`

` if (%num is a natural number)`
` then (primary (%num) with vars %names having values %vals`
` equals %num).`

The syntax and semantics of boolean expressions are defined as follows:

-- <boolean_expr> ::= <numeric_expr> < <numeric_expr>

` if (expr ($expr1) with vars %names having values %vals
equals %num1)`
` and (expr ($expr2) with vars %names having values %vals
equals %num2)`
` and (%num1 < %num2 equals %true_or_false)`
` then (expr ($expr1 < $expr2) with vars %names having
values %vals`
` equals %true_or_false).`
` if (%I < %J) then (%I < %J equals true).
-- definition of ..`
` if (%J <= %I) then (%I < %J equals false).
-- .. the < operator`

-- the other relational operators are similarly defined

It should be evident that any language
construct can be defined in this manner, allowing for certain low-level
syntax rules such as the space required between tokens. As a contrast
to the conventional language defined here, a portion of Backus' functional
programming has been defined. Axiomatic language compares favorably
with other formalisms for defining programming language semantics [see
Cleaveland 80, Marcotty et. al. 76, Stoy 77], with the added advantage
of being machine executable. To define the semantics of a language
in axiomatic language is to make it available for use. The programmer
thus has the capability to create whatever language tool is desired for
a problem. Axiomatic language is intended to be a single language
which can incorporate the features of any other language.

For other examples of how axiomatic language could be used, one should see examples of how PROLOG is used in such applications as AI knowledge representation and problem solving and database definition and queries [Gallaire & Minker 78, Kowalski 79].

The extensibility of axiomatic language
is seen from the way previously defined functions and relations are used
to define new ones. In an actual programming environment using axiomatic
language, there would be a large database of axioms defining various functions
and features. Programmers would build upon this existing software
by simply combining the axioms of their programs with those in the database.
This is simpler than the linking and calling of subroutines in conventional
languages. Furthermore, axiomatic language is more modular since
each axiom is essentially a small module -- a statement of a "truth", the
correctness of which is largely independent of the other axioms.

**4. Interpreting Axiomatic Language**

Axiomatic language has been presented thus far as an abstract formal system capable of defining "pure" functions and relations. Real computing, however, involves state changes and input/output. PROLOG has language primitives for this, but in axiomatic language this is achieved simply by interpreting the valid expressions in different ways. Section 4.1 shows how axiomatic language defines a program that processes an input file to produce an output file and section 4.2 shows how it defines a program that does interactive input/output.

**4.1 Processing a File**

This example defines a program which reads an input file of character strings and produces an output file consisting of those character strings sorted alphabetically. The axioms for sorting given previously are assumed defined. It is necessary only to define the binary relation '<' on character strings.

Characters can be represented by atoms with symbols consisting of the character preceded by a single quote: 'A, '3. The set of characters and their alphabetical ordering is defined by the following axioms:

` (Chars: ' '0 .. '9 'A .. 'Z ... ).
-- desired alphabetical order`
` if (Chars: $str1 %char1 $str2 %char2 $str3)
-- definition of < ..`
` then (%char1 < %char2).
-- .. between chars`

A character string is just a sequence of character atoms. The lexicographic ordering of arbitrary sequences of expressions is defined as follows:

` (($prefix) < ($prefix %expr $str)).`
` if (%expr1 < %expr2)`
` then (($prefix %expr1 $str1) < ($prefix %expr2
$str2)).`

These axioms generate valid expressions such as '(('A 'B 'C) < ('A 'B 'D))'. From these valid expressions the axioms defining sorting generate expressions such as

` (the sort of`
` ( ('C '1) ('Z) ('A 'B
'C) () )`
` is`
` ( () ('A 'B 'C) ('C
'1) ('Z) ))`

representing the sorting of the file of strings "C1", "Z", "ABC", "" to produce the file "", "ABC", "C1", "Z".

The execution of this sorting "program" would consist of the language processor matching the contents of a specified input text file with the unsorted sequence of one of the valid expressions for sorting, and then putting the corresponding sorted sequence into a specified output file. The details of how one would initiate this procedure are not important here. In a similar manner one can define programs that process multiple files of arbitrary data types by associating the files with components of valid expressions. The language processor would find the valid expression that matches the specified input files and from that generate the output files. Note that there may be multiple valid expressions which match the specified input files. If so, then one of the valid expressions is selected nondeterministically and the corresponding outputs are produced. If there is no valid expression matching the specified input files, the execution "aborts".

**4.2 Interactive Programs**

Interactive programs are defined by axioms which generate valid expressions for all possible sequences of inputs and outputs. Consider a program which reads an arbitrary string of characters (terminated by a carriage return) and then types it back in reverse. If a null string is entered, the program halts. A particular execution of this program could be represented by the following valid expression:

` (begin
-- program execution begins`
` (input: 'A 'B 'C 'D)
-- user types "ABCD"`
` (output: 'D 'C 'B 'A)
-- program echoes "DCBA"`
` (input: 'X ' 'Z)
-- user types "X Z"`
` (output: 'Z ' 'X)
-- program echoes "Z X"`
` (input:)
-- user enters a null string`
` end)
-- program halts`

This program is defined by the following axioms, which generate valid expressions such as the one above for all possible sequences of inputs the user might type:

` (the reverse of () is ()).
-- definition of the`
` if (the reverse of ($str1) is ($str2))
-- reverse function`
` then (the reverse of ($str1 %expr) is (%expr
$str2)).`

` (begin (input:) end).
-- definition of the`
` if (begin $i/o end)
-- begin .. end expressions`
` and (the reverse of ($str1) is ($str2))`
` then (begin (input: %expr $str1) (output: $str2 %expr) $i/o
end).`

These axioms define input/output sequences containing arbitrary expressions, but only those expressions with characters are considered.

The above axioms generate abstract expressions that, when interpreted by the language processor, define in a nonprocedural manner a program that does interactive input/output. At a given instant during the execution of this program, a particular sequence of inputs and outputs has occurred. From the set of "(begin ... end)" valid expressions, the language processor finds those that have a prefix that matches the inputs/outputs thus far. The next expression in those valid expressions specifies whether the program should input a string or output a string. Nondeterministic interactive programs are possible, such as when two "(begin ... end)" valid expressions have different output strings immediately following a common prefix.

One may also define programs that do not terminate, by adopting the convention of leaving off the "end". The following program, for example, simply outputs the string "ABC" in an infinite loop.

` (begin).`
` if (begin $str)`
` then (begin $str (output: 'A 'B 'C)).`

As with the other syntactic details of
axiomatic language, the representation of characters used here is arbitrary.
A more convenient syntax could be adopted, such as allowing one to write
'(Output: "abcde")' in place of '(Output: 'a 'b 'c 'd 'e)'.

**5. Primitive Axiomatic Language**

Axiomatic language is intended to be a minimal language, but in fact it is not. This section defines a proper subset of axiomatic language, called primitive axiomatic language, which has the same power. Primitive axiomatic language is just "regular" axiomatic language with string variables eliminated and sequences always of length two (called "pairs"). Expressions are thus binary trees with atoms and expression variables as the leaf nodes. Axioms are defined the same as in regular axiomatic language and the rules for generating valid expressions from axioms likewise correspond. The same syntax is used for expressions and axioms.

As an example of primitive axiomatic language, the definition of natural numbers and their addition are presented:

` (Number 0).
-- zero is a natural number`
` if (Number %I)
-- if I is a natural number`
` then (Number (succ %I)).
-- then the successor of I is also`

` if (Number %I)
-- if I is a natural number`
` then (Plus ((%I 0) %I)).
-- then I + 0 = I`
` if (Plus ((%I %J) %K))
-- if I + J = K`
` then (Plus ((%I (succ %J)) (succ %K))).
-- then I + (J+1) = (K+1)`

These axioms generate valid expressions such as '(Plus (((succ 0) 0) (succ 0)))', representing the statement "1 + 0 = 1". Because of the difficulty of reading deeply nested parentheses, primitive axiomatic language is interesting more for theoretical and implementation purposes than for actual programming.

It was said earlier that even though
primitive axiomatic language is a proper subset of regular axiomatic language,
it has the same power. This can be shown by simulating regular axiomatic
language using primitive axioms. It can also be shown that axiomatic
language is equivalent in power to Turing machines, type-0 grammars, and
other formalisms for defining the computable functions. That axiomatic
language is as powerful as these other formalisms is easily demonstrated
by using it to simulate type-0 grammars. That axiomatic language
is no more powerful than these other formalisms is shown by the fact that
an algorithm that simulates axiomatic language can be written in a conventional
programming language. Thus axiomatic language is another distinct
formalism for representing the set of computable functions.

**6. Conclusions**

Axiomatic language is presented as a
simple, elegant, and powerful tool for software development. It would
reduce software costs by eliminating the implementation details from software
specification and by simplifying and encouraging the reuse of software
components through its extensibility. It allows one to define arbitrary
language constructs for the specification of software in optimal ways.
The price for all this is its difficulty of implementation. To efficiently
execute a program from just its functional specification requires considerable
intelligence on the part of the language processor. Currently, primitive
axiomatic language has been implemented in a simple fashion. Future
work will be applied to the problem of efficiency.

**Acknowledgements**

The author wishes to thank Bill Buckles
and Ted Sparr of the University of Texas at Arlington for their helpful
comments.

**References**

Backus, John, "Can Programming Be Liberated from the von Neumann Style?", Comm. ACM, August 1978.

Bowen, Kenneth A., "PROLOG", ACM79 Conference Proceedings.

Cleaveland, J. Craig, "Mathematical Specifications", SIGPLAN, December 1980.

Dijkstra, Edsger W., "The Humble Programmer", Comm. ACM, October 1972.

Gallaire, H. and Minker, J., Eds., Logic and Data Bases, Plenum Press, 1978.

Kowalski, Robert A., Logic for Problem Solving, Elsevier North Holland, 1979.

Marcotty, M.; Ledgard, H. F.; and Bochmann, G. V., "A Sampler of Formal Definitions", ACM Computing Surveys, June 1976.

Stoy, Joseph E., Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, 1977.

Wulf, William A., "Trends in the Design and Implementation of Programming
Languages", Computer, January 1980.