Language Details - Grammar

stmt ::= ...
       | foreach (fmla) {stmt+}
       | if (fmla) {stmt+} else {stmt+}
       | cond (fmla) {stmt+}+ else {stmt+}
       | switch (expr) (ptrn:fmla) {stmt+}+ default {stmt+}

dcln ::= ...
       | predicate id(T x1, ..., T xn) [mode]+ {fmla}+
       | predicate T id(T x1, ..., T xn) [mode]+ {fmla}+

ptrn ::= expr
       | T id
       | T
       | *
       | expr.id(ptrn+)
       | e[ptrn]
       | ptrn binop ptrn

fmla ::= T id
       | fmla && fmla
       | fmla || fmla
       | forall (fmla) {fmla}
       | exists (fmla) {fmla}
       | expr.id(ptrn+)               // id names a predicate
       | ptrn bincomp ptrn

bincomp ::= == | != | < | <= | > | >=

binop ::= + | - | * | / | %

Language Details - Statement Translations

Foreach

S  �foreach (F) {s}‘ = F_M�F‘s

If

S  �if (F) s₁ else s₂‘ =
     boolean flag = true;
     F_S�F‘{flag=false; s₁};
     if (flag) s₂;

Cond

S  �cond (F₁) {s₁} (F₂) {s₂} ... default s_d‘ =
     boolean flag = true;
     F_S�F₁‘{flag=false; s₁};
     if (flag) { F_S�F₂‘{flag=false; s₂};
                ...
                   if (flag) s_d ...}}

Language Details - Mode Determinations

Language Details - Formula Translations

Variable Introduction

F_S[T id]s = {T id; s}

F_M[T id]s = {T id; s}

Formula Conjunction

F_S�F₁ && F₂‘s = F_S�F₁‘(F_S�F₂‘s)

F_M�F₁ && F₂‘s = F_M�F₁‘(F_M�F₂‘s)

Notes: We need to create a dependency graph for two reasons:

1. During type checking, it allows us to determine if formula is even solvable.
2. Gives us an ordering on the conjuncts for translation.

Given a graph, two resulting errors are possible:

1. No start state, meaning that not enough values exist to begin solving the formula.
2. Not all nodes are reachable from the start states, meaning the formula is too complicated.

Ordering of the conjuncts is determined by a modified topological sort on the graph.  Edges in this graph are determined by looking at the modes of each conjunct. A mode has a set of knowns and a set of unknowns.  Any conjunct will have a mode that looks like X ! Y.  An edge in the dependence graph, (F, F') exists if:

• X' ² Y
• F: X ! Y
• F': X' ! Y'

When the mode has an empty set of unknowns (the set on the left of the arrow), this corresponds to a start state in the graph

Formula Disjunction

F_S�F₁ || F₂‘s₁s₂ = F_S�F₁‘s₁(F_S�F₂‘s₁s₂)

The above should be revised to avoid code duplication.

F_M�F₁ || F₂‘s = F_M�F₁‘s; F_M�F₂‘s

Notes: It must be the case that the yielded variables of F₁ are the same as the yielded variables of F₂.

Formula Universal Quantifier

F_S�forall (F₁) {F₂}‘s =
     F_S�F₁‘ {T v₁ = yielding of F₁};
     F_S�F₂‘ {
            boolean flag = true;
            F_M�F₁‘ {if (!F₂) {flag=false; break;}}
            if (flag) {s}
           }

F_M�forall (F₁) {F₂}‘s =
     F_S�F₁‘ {T v₁ = yielding of F₁};
     F_M�F₂‘ {
            boolean flag = true;
            F_M�F₁‘ {if (!F₂) {flag=false; break;}}
            if (flag) {s}
           }

Formula Existential Quantifier

 

Predicate Invocation

F_S�id(p₁, ..., p_n)‘s =
     Iterator g = new id$();
     if (g.hasNext()) {
          (x₁, ..., x_n) = g.next();
          s;
     }

F_M�id(p₁, ..., p_n)‘s =
     for (Iterator g=new id$(); g.hasNext(); ) {
          (x₁, ..., x_n) = g.next();
          s;
     }