Appendix

Here we describe relations between PSL/IDL conventions and underlying PSL constructs. We first introduce an expanded notation for representing situations as named, parameterized predicates of the form

Name(Parameters){ Predicate}.

For example, a situation describing the state of a File being open is:

OpenFileSituation(File f){ isOpen(f) }

OpenFileSituation names the situation. The argument list declares all variables and types used in the defining predicate.

The standard PSL/IDL form is abbreviated in that:

• Situations are not named.
• Situations are defined only within the scope of rules declarations, and implicitly take the handles declared in their rules declaration as parameters.
• Situation predicates may include in-line local declarations to name values inside expressions. These are added as implicit parameter declarations.
• Message arguments are implicit, with values bound according to IDL conventions, as described below.

A realization may be represented as a tagged set of values. A realization r matches situation S (i.e., r S) if there exists a consistent assignment of the values in r to the arguments in S in accord with all constraints such that S's predicate is true. Value assignments must be consistent across all situations in the same scope. Realizations obey one or more rules if the rules hold under applicable assignments of values to rules parameters.

Variants.

To accommodate the range of options available in CORBA systems, PSL/IDL rules may also be described at the level of individual activations of individual operations rather than the implementation objects that they are normally defined under. Handles of the form Interface :: Operation denote abstract activations (executing instances) of the indicated operations. For example, an instance of the form aFile::read is a handle to an abstract activation of a given File aFile's read operation as defined in the File interface. (Among other alternatives, this handle might be mapped to an implementation-level pointer to a stack frame.)

In addition to the message forms described in Section 3, PSL/IDL procedural messages may include from( src ) designation indicating the ``return address'' of a sender:

m = < dest-> op( args) from( src) >

Also, in and out event predicates may be annotated with by( Handle ) to indicate the participant issuing or receiving a message. For example,
in(<aFile->write(c)>)by(aFile::write w)
allows a shift to an activation-level description focused on a single write operation. Note that from could be different than by in systems supporting implicit forwarding of delegated messages.

Message types may also be made explicit. They may be given names using a typedef convention analogous to the inline declaration style. Required fields have the same names as their arguments; sources and destinations are called _src and _dest respectively. For example, to represent the type of File::write messages:

 typedef  <File::write(in char c)> WriteMsg;

Bindings.

Argument bindings in messages follow normal IDL conventions, which are related to underlying PSL constructs as follows. Any situation containing an in or out predicate implicitly takes a message of the corresponding type as a parameter, and message fields are implicitly equated with named variables according to their use. When by is omitted, it is also added an parameter simply of type Object, the base of the IDL interface hierarchy. For example, consider PSL/IDL situations:

 {in( <aFile->write(c)> ), c == 'a'}

 {out( <aFile->write('a')> )}

These may be expanded as:

typedef <File::write(in char c)> WriteMsg;

Sin(File aFile, WriteMsg m, char c, Object rcvr) {
  m._dest == aFile, 
  in(m) by(rcvr),
  c == 'a', c == m.c
}

Sout(File aFile, WriteMsg m, Object sndr) {
  m._dest == aFile, m.c == 'a',
  out(m) by(sndr)
}

IDL-level attributes are also treated as operation declarations in PSL, with message selector names formed by prepending get_ and set_ for the ``read'' and ``write'' forms of the operation respectively, in accord with common language mapping conventions [52,55].

Scopes.

Pairs of situations related by ordering rules must be normalizable under a common set of symbols, each assuming a unique value in realizations. All successor situations carry all parameters from their rules and predecessors as well as all non-negated event predicates in predecessors. Consider, for example:

rules x(P p) {
 {in( <p->op1(a, b)> ), long i == attr(p)} 
 lead
 {out( <a->op2(b, i)> )}
};

The situations may be tediously expanded as:

typedef <P::op1(in A a, in B b)>    op1Msg;
typedef <A::op2(in B b, in long i)> op2Msg;

S1(P p, op1Msg mop1, long i, A a, B b, Object s1rcvr) {
 in(mop1) by(s1rcvr), 
 i == attr(p),
 a == mop1.a,
 b == mop1.b 
}

S2(P p, op1Msg mop1, long i, A a, B b, Object s1rvcr, 
   op2Msg mop2, Object s2sndr) {
 in(mop1) by(s1rcvr), 
 out(mop2) by (s2sndr),
 mop2._dest == a,
 mop2.b == b,
 mop2.i == i 
}