We have already shown Olaf’s concrete syntax, syntax which the programmer enters into their emacs buffer. Such syntax, however, especially with infix notations, can be hard to reason about as concrete syntax can be ambiguous.

Instead we will begin by presenting an abstract syntax, designed to be unambiguous.

Types

For values:

t := int | bool | string | unit | &t

For methods:

mty := { t_0,..., t_n } -> t

Constants

c := i            -- integers
   | s            -- strings
   | true | false -- booleans
   | unit         -- unit

Expressions

e := mref               -- Variables pointing to methods
   | xref               -- Local variables point to the stack
   | c                  -- constants
   | bop(e,e)           -- binary operations
   | cop(e,e)
   | uop(e)             -- unary operations
   | cast(t,e)          -- casting to strings
   | &e                 -- dereferencing memory
   | mref({e_0,...,e_n) -- method calls

where

uop := not

bop := add | mul | sub | div -- numerical operations
     | and | ior | xor       -- boolean operations

cop := lt | lte | gt | gte   -- comparison operations
     | eq

Statements

s := return e               -- return a value
   | print e                -- print a string
   | xref = e               -- mutate memory
   | let xref : t = e; s    -- binders
   | var xref : t = e; s
   | if e { s } else { s }  -- control flow
   | while e { s }
   | s ; s

Methods

m := (\{ xref_{0} : t_{0},..., xref_{n} : t_{n}} => s)

Programs

mdecl := mref = m

p := m --- main method
  | mdecl ; p

We have presented an inductive representation of programs as this is somewhat easier to reason about. Other representations use a more compact construction:

p := { mdecl_{0}, ..., mdecl_{n} } m