CAPSL Abstract Syntax

node: node-label arg1 arg2 ...

node: node1 | node2 ...

where arg1, arg2, etc. are the subtrees below the node.

At this stage in the parsing, type checks and other semantic checks have not been performed. Bracketed encryptions have been converted to "crypt" function calls on cat or con function calls, but have not been resolved into se or ped.

Nonterminals and node labels in this grammar are related to, but not the same as, nonterminals in the concrete grammar. The only terminals occurring in this grammar are the node labels. Terms and other expressions that are not expanded here are essentially the same as in the concrete grammar.

If x is a nonterminal symbol, x* is a possibly empty sequence of subtrees of type x. If S is the name of a nonterminal symbol, there is implicitly a rule Ss: Ss S*, unless Ss is defined explicitly some other way. Thus, since "decl" is a nonterminal, and "decls" is not explicitly defined, we automatically assume a rule

decls: decls decl*

A vertical bar | separates choices. Brackets are not used. Comments in this rule list are surrounded by /* and */, e.g., /* this is a comment */.

The Syntax

specification: specification component*

component: typespec | protocol | environment

typespec: typespec id decls axioms

protocol: protocol id decls asserts phrases goals

environment: environment id decls axioms agents exposed order

decl: typedec | funcdec | vardec | denote | import | constant

phrase: phrase acts message acts | include id | select

select: select stmt phrase phrase

act: stmt | assume assert | prove assert

prove: prove assert

goals: goals assert*

typedec: types ids id

funcdec: func id ids id props

/* a function has a name, argument types, value type, and properties */

vardec: var ids id props

denote: denote term term

import: imports ids

constant: const ids id

stmt: equation | term | if

assert: holds | believes | knows | secret | precedes | agree | stmt

equation: eqn term term

if: if stmt stmt stmt

message: msg id id id terms

term: fncall | id | lowe

lowe: lowe term term

fncall:  id term*

holds: holds id ids

believes: believes id assert

knows: knows id assert

secret: secret id ids

precedes: precedes id id ids

agree: agree ids ids ids

agent: agent id eqns

exposed: exposed terms

order: order order