The Pda Protocol Derivation Language

Protocol Instantiations

Protocol instantiations can be used to instantiate agent, function, and action parameters of abstract protocols. An example of a protocol instantiation is

CRI[A,B](c) = CR[A,B](c=c,r[A,B](x)=x)

which means that the protocol CRI is defined in terms of CR by declaring the r parameter to be the identity function. The syntax rules for protocol instantiations are as follows:

ProtDecl	::=	...
		ProtInst
ProtInst	::=	SimpleProtDect '=' ProtTerm
ProtTerm	::=	ProtTermInst
		`

The protocol term for instantiations is defined as follows:

ProtTermInst	::=	ProtocolNameIdentifier StaticParams FunctionAndActionInsts
FunctionAndActionInsts	::=	( '(' (FunctionInst `

A function instantiation provides a definition for a function parameter of the abstract protocol that is being instantiated. There are two variants that can be used to instantiate the functions of an abstract protocol:

• If only function identifiers are used in the instantiation list, then the functions parameters are mapped to the arguments according to the order in the parameter list. For instance, an instantiation

  CRH[A,B](r1) = CR[A,B](H,r1)

  would instantiate the c parameter of CR with H and the r parameter of CR with the local parameter r1 of CRH.

  FunctionInst	::=	< identifier >
  		`

• Complete function definitions can be specified in those cases where the simple form can’t be used; each function instantiation resembles a function definition for the parameter on the left-hand side. The function instantiation list must in any case give instantiation for all parameters in the abstract protocol, in either of the formats.

  FunctionInst	::=	...
  		`

  An example of a function definition of the second form is given in the above instantiation example: r[A,B](x)=x;

In either of the forms all function parameters must be mentioned in the argument list of the instantiation.

Action instantiations can be used to replace an action variable attached to a local agent edge in the abstract protocol. The syntax for an action instantiation is

ActionInst	::=	<identifier> '=' '{' AgentAction '}'

Because, function and action instantiations can occur in any order in the instantion list, the use of an action instantiation implies that use of the second variant for function instantiations, i.e. action instantiations cannot be mixed with function instantiations using only identifier and the argument position. An example of an action instantiation would be:

a = {new x}

---