Formal Descriptions of Programming Languages

Introduction

Let’s see how one can give a formal programming language definitions by actually writing some. We’ll define a small imperative programming language, and will call it Iki. We’ll look at several different definition styles. Don’t worry, though, each of the definitions define the same language.

Syntax

The source of an Iki program is a Unicode string. Here is a formal definition of Iki syntax using Ohm:

Iki {
  Program     =  Block
  Block       =  (Stmt ";")+
  Stmt        =  var id ":" Type             -- declaration
              |  VarExp "=" Exp              -- assignment
              |  read VarExp ("," VarExp)*   -- read
              |  write Exp ("," Exp)*        -- write
              |  while Exp loop Block endw   -- while
  Type        =  int | bool
  Exp         =  Exp or Exp1                 -- binary
              |  Exp1
  Exp1        =  Exp1 and Exp2               -- binary
              |  Exp2
  Exp2        =  Exp3 relop Exp3             -- binary
              |  Exp3
  Exp3        =  Exp3 addop Exp4             -- binary
              |  Exp4
  Exp4        =  Exp4 mulop Exp5             -- binary
              |  Exp5
  Exp5        =  prefixop Exp6               -- unary
              |  Exp6
  Exp6        =  boollit
              |  intlit
              |  VarExp
              |  "(" Exp ")"                 -- parens
  VarExp      =  id

  var         =  "var" ~idrest
  read        =  "read" ~idrest
  write       =  "write" ~idrest
  while       =  "while" ~idrest
  loop        =  "loop" ~idrest
  endw        =  "end" ~idrest
  int         =  "int" ~idrest
  bool        =  "bool" ~idrest
  true        =  "true" ~idrest
  false       =  "false" ~idrest
  or          =  "or" ~idrest
  and         =  "and" ~idrest
  not         =  "not" ~idrest

  keyword     =  var | int | bool
              |  read | write | while | loop | endw
              |  true | false | or | and | not
  id          =  ~keyword letter idrest*
  idrest      =  "_" | alnum
  intlit      =  digit+
  boollit     =  true | false
  addop       =  "+" | "-"
  relop       =  "<=" | "<" | "==" | "!=" | ">=" | ">"
  mulop       =  "*" | "/" | "%"
  prefixop    =  ~"--" "-" | not

  space      +=  comment
  comment     =  "--" (~"\n" any)* "\n"
}

We can also define the same language using syntax diagrams. While Ohm distinguishes lexical from phrase categories using lower and uppercase starting letters, respectively, syntax diagrams make their distinction with rounded rectangles vs. rectangles. They also assume that a “lexical analysis” or “tokenization” pass was previously done, using a maximal munch process:

Other forms of syntax definition include BNF, EBNF, and ABNF. There are many others.

Abstract Syntax

A grammar, whether written in Ohm or some other notation, defines a concrete syntax. A semantics will be defined based on an abstract, rather than a concrete, syntax (because punctuation, spacing, and comments just get in the way), so we have to define how to generate abstract syntax trees from concrete ones. In other words, we want to turn this string:

-- An Iki program
var x: int;
var y: int;
while y - 5 == 3 loop
  var y: int;
  read x, y;
  x = 2 * (3 + y);
end;
write 5;

into this tree:

(Program
  (Block
    (Declare x int)
    (Declare y int)
    (While
      (== (- y 5) 3)
      (Block
        (Declare y int)
        (Read x y)
        (= x (* 2 (+ 3 y)))))
    (Write 5)))

There are many ways to formally specify the relationship between the grammar and the abstract syntax tree. The first way shoves a lot of notation into the grammar itself. The idea is that as you parse a string by walking the grammar rules, you emit chunks of trees as you go. Let’s show it via an example:

Program =  Block:b                                        ^{Program b}
Block   =  (Stmt::s ';')+                                 ^{Block s}
Stmt    =  'var' id:i ':' Type:t                          ^{Var i t}
        |  VarExp:v '=' Exp:e                             ^{Assign v e}
        |  'read' VarExp::v (',' VarExp::v)*              ^{Read v}
        |  'write' Exp::e (',' Exp::e)*                   ^{Write e}
        |  'while' Exp:e 'loop' Block:b 'end'             ^{While e b}
Type    =  'int':t                                        ^t
        |  'bool':t                                       ^t
Exp     =  Exp1:e1 ('or':o Exp1:e2 {Binary o e1 e2}:e1)*  ^e1
Exp1    =  Exp2:e1 ('and':o Exp2:e2 {Binary o e1 e2}:e1)* ^e1
Exp2    =  Exp3:e1 (relop:o Exp3:e2 {Binary o e1 e2}:e1)? ^e1
Exp3    =  Exp4:e1 (addop:o Exp4:e2 {Binary o e1 e2}:e1)* ^e1
Exp4    =  Exp5:e1 (mulop:o Exp5:e2 {Binary o e1 e2}:e1)* ^e1
Exp5    =  prefixop:o Exp6:e                              ^{Unary o e}
        |  Exp6:e                                         ^e
Exp6    =  boollit:b                                      ^{Boollit b}
        |  intlit:n                                       ^{Intlit n}
        |  VarExp:v                                       ^v
        |  '(' Exp:e ')'                                  ^e
VarExp  =  id:i                                           ^{VarExp i}

Each grammar rule is augmented with tree productions; you might be able to infer the metalanguage for this, but if not, here are the highlights:

• AST nodes are represented as {A B C ...} where A is the root and B, C, ... are the ordered children.
• Tree nodes can be simple strings or numbers.
• The evaluation of a grammar rules produces a node; we indicate that the node is produced or returned, with the ^ symbol.
• During a parse, the evaluation of categories, tokens, and tree nodes can be bound to variables. The : binding overwrites the current value of the variable, if any; the :: binding accumulates values into a list.

A second way to define an AST for a grammar is to use Ohm. Ohm separates operations from the grammar, so things aren’t messy at all. The operations that produce the AST are written in an actual programming language, so they are executable and testable. Here’s the Ohm specification for generating the AST for Iki, using JavaScript:

const astBuilder = grammar.createSemantics().addOperation('ast', {
  Program(b) {
    return new Program(b.ast());
  },
  Block(s, _) {
    return new Block(s.ast());
  },
  Stmt_declaration(_1, id, _2, type) {
    return new VariableDeclaration(id.sourceString, type.ast());
  },
  Stmt_assignment(varexp, _, exp) {
    return new AssignmentStatement(varexp.ast(), exp.ast());
  },
  Stmt_read(_1, v, _2, more) {
    return new ReadStatement([v.ast(), ...more.ast()]);
  },
  Stmt_write(_1, e, _2, more) {
    return new WriteStatement([e.ast(), ...more.ast()]);
  },
  Stmt_while(_1, e, _2, b, _3) {
    return new WhileStatement(e.ast(), b.ast());
  },
  Type(typeName) {
    return typeName.sourceString;
  },
  Exp_binary(e1, _, e2) {
    return new BinaryExpression('or', e1.ast(), e2.ast());
  },
  Exp1_binary(e1, _, e2) {
    return new BinaryExpression('and', e1.ast(), e2.ast());
  },
  Exp2_binary(e1, op, e2) {
    return new BinaryExpression(op.sourceString, e1.ast(), e2.ast());
  },
  Exp3_binary(e1, op, e2) {
    return new BinaryExpression(op.sourceString, e1.ast(), e2.ast());
  },
  Exp4_binary(e1, op, e2) {
    return new BinaryExpression(op.sourceString, e1.ast(), e2.ast());
  },
  Exp5_unary(op, e) {
    return new UnaryExpression(op.sourceString, e.ast());
  },
  Exp6_parens(_1, e, _2) {
    return e.ast();
  },
  boollit(_) {
    return new BooleanLiteral(this.sourceString === 'true');
  },
  intlit(_) {
    return new IntegerLiteral(this.sourceString);
  },
  VarExp(_) {
    return new VariableExpression(this.sourceString);
  },
});

Another way is to use something called an attribute grammar. There are other ways, too.

Semantics

This section defines the semantics of Iki. Semantics generally has a static and a dynamic part; the static semantics describes rules that can be checked at compile time but that are impossible (or ridiculously inconvenient) to put into a context free grammar. The dynamic part defines what the program actually does when it runs. This is done on a macro as well as a micro level.

Static Semantics

The functions below transform an abstract syntax tree into a semantic graph. The semantic graph is almost identical to the abstract syntax tree; the only exceptions (in Iki, anyway) being that:

1. All Exp nodes have a new field (type)
2. All VarExp nodes have a new field (referent) that refers to a Var node.

The functions mathematically encode the rules we intuitively know as:

• Identifiers must be declared before being used
• Inner declarations hide outer ones
• Variables local to a block are invisible to sibling and ancestor blocks
• Only ints may be read and written
• Only ints may appear as operands to arithmetic and relational operators
• Only bools may appear as operands to logical operators
• Types must match across assignments
• Types must match across == and != operators

The definitions make use of environments which are mappings from variable names (strings) to actual variables. At any point in time we have of stack of environments corresponding to the nesting of the block currently being processed. Every time we enter a block we push a new, empty environment on this stack, which will get filled with the declarations of this block. When leaving a block, the topmost environment is popped. When resolving a variable reference, we search the environments from the top of the stack to the bottom.

This static semantics can be viewed as adding a type field to every expression node, and a referent field to every variable expression node.

Note that the functions may fail to produce a semantic graph for a given abstract syntax trees. In such a case we have a program which is syntactically valid (possesses no syntax errors), but semantically invalid.

Dynamic Semantics

The dynamic meaning of an Iki program is some transformation from an input file to an output file. For example, the meaning of var x: int; read x; write x+1; end is “the function that takes in an arbitrary input file, and returns an output file containing a single element whose value is one more than the first item on the input file.”

Macrosemantics

The meaning is given here by a functions from semantic graphs to their “meanings.” The meaning of a program is a mapping from inputs to outputs. Statements change the state of the computation; the state is the aggregation of (1) its current data store (mapping from its variables to their values), (2) the current input file, and (3) the current output file. The meaning of an expression is the value it produces, relative to a store, of course. Declarations in Iki have no dynamic effect.

The style in which we’ve been writing our semantic descriptions is called a Denotational Semantics. We can also write an Operational Semantics:

Microsemantics

The meaning of a program is a mapping from an input file to an output file; these correspond to the environment’s standard input and standard output files respectively. Integers are read from standard input as digit strings optionally prefixed by a single - and separated by whitespace. The first integer in the file may be preceded by whitespace and the last integer may be followed by whitespace. Note that the macrosemantics does allow a program to terminate without reading the entire input file; in this case an implementation must ignore the unread portion of the input file. If an error occurs during reading, the program aborts and must signal its environment in some fashion (e.g. it may set an exit status value, or write a message). Integers are written to the output file as digit strings, prefixed by a single - if negative, separated by a single space. There may be whitespace before the first integer and after the last.

Implementation Permissions

Sometimes there are things left unspecified in a syntax. In Iki, we didn’t mention a couple things, so a definition would probably include language like the following: “An implementation may fix a maximum length for identifiers, and may fix a maximum bit length for integers. Arithmetic may be signed or modular.”