Other Semantic Issues

The formal semantics given in the previous subsections are mostly dealing with PJ's language elements. Due to lack of space, we left out many conditions specifying more complex semantic issues. In the following we roughly sketch out important notions concerned with these issues:

• Connectivity: With the exception of argument ports of agents or rules, every port has to be linked to another port. This feature is expressed with the help of recursive predicates transitively verifying the connectivity.

• Reachability: List elements (i.e. their reference ports) that are outside of rules have to be reachable from argument ports of rules via a (possibly empty) chain of other list elements. Of course, connectivity is a necessary condition for reachability.

• Askers: Channels, links, and data terms which are reachable parts of preconditions of rules are classified as askers.

• Tellers: Channels, links, and data terms which are reachable parts of rule bodies are classified as tellers.

• Rules: Ports of rules are either unused or linked to reference ports of askers or tellers.

• Agent calls: The number of argument ports of agent calls and their denoted agents have to be equal.

The complete set of specifications is sufficient to describe semantics of static PJ programs. This property is verified through the analysis of example programs resulting in a semantic network which can be used to create executable PJ programs.