ContextFreeGrammar.dfy

// A brief formalization of context-free grammars in Dafny.

// Terminals (i.e. tokens).
type T = string

// Names of nonterminals.
type Nt = string

// The right-hand side of a production is a sequence of terminals and nonterminals.
datatype Symbol = T(T) | Nt(Nt)

// A grammar is just a set of productions; but we represent it as a
// map from left-hand sides to the set of corresponding right-hand sides.
type Grammar = map<Nt, set<seq<Symbol>>>

// Like so:
function ExampleGrammar(): Grammar {
  map [
    "expr" := {
      [Nt("term")],
      [Nt("expr"), T("+"), Nt("term")],
      [Nt("expr"), T("-"), Nt("term")]
    },
    "term" := {
      [Nt("factor")],
      [Nt("term"), T("*"), Nt("factor")],
      [Nt("term"), T("/"), Nt("factor")]
    },
    "factor" := {
      [Nt("prim")],
      [T("-"), Nt("factor")],
      [Nt("prim"), T("^"), Nt("factor")]
    },
    "prim" := {
      [T("NUM")],
      [T("VAR")],
      [T("("), Nt("expr"), T(")")]
    }
  ]
}

// Now we define the "Produces" relation, which tells when one string of
// symbols can "expand to" another string by expanding a nonterminal using a
// production, zero or more times. First, the step relation:

predicate SingleStepProduces(grammar: Grammar, orig: seq<Symbol>, dest: seq<Symbol>) {
  exists i, lhs, rhs :: (
    0 <= i < |orig| &&
    orig[i] == Nt(lhs) &&
    lhs in grammar &&
    rhs in grammar[lhs] &&
    dest == orig[..i] + rhs + orig[i + 1..]
  )
}

// Now the transitive closure of that relation, which is what we're really after.
//
// (Regarding the keyword "inductive": Dafny would normally make us prove that
// the recursion on Produces terminates, i.e. that the predicate is
// "well-founded". That would be a pain to prove in this case, because there
// might be cycles in the grammar. "inductive" tells Dafny that we want the
// least upper bound on this predicate: we mean to require a finite chain of
// steps that actually reaches `dest`.)
//
inductive predicate Produces(grammar: Grammar, orig: seq<Symbol>, dest: seq<Symbol>)
{
  orig == dest ||
  exists step :: SingleStepProduces(grammar, orig, step) && Produces(grammar, step, dest)
}