Next: Translation to Description
Up: Formal Specification of
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
- 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.
Wed Jan 31 15:50:43 MET 1996