Invocation
The Invocation behavior represents an action or machine invocation.
Syntax Definition
Invocation ::= [ ! ] [ AtomicQualifier ] Target [ ( ArgList ) ] [ / Expression ] .
AtomicQualifier ::= call | return | event .
Target := new [ Expression . ] Type | Expression . Ident | QualIdent .
ArgList ::= [ out | ref ] Expression { , [ out | ref ] Expression } .
Remarks
An invocation can be negated using the exclamation mark (!). Negation is allowed only for action invocations. A negated action invocation denotes the union of all action invocations built from atomic actions in the context signature that do not match the specified action invocation.
An action invocation can be prefixed by any of the modifiers for calls, returns, and events. If a modifier is used, the invocation denotes the according atomic action invocation, which must be a member of the context signature. If a modifier is not used, the declaration of the corresponding action in the context signature determines the interpretation, as follows:
If the action is declared as an event, an event invocation is implicitly denoted.
Otherwise, an implicit sequence of call and return invocations is denoted. Thus, if A is not an event action, the following syntactic reduction is valid:
A(x)/y -> call A(x); return A/y.The target of an invocation can be either a constructor application, an instance method application, or an application of a simple name. The target is interpreted as follows:
If the target is a simple name and a machine declaration of that name exists, a machine invocation is denoted.
Otherwise, argument arity (the number of arguments) and type information is used to resolve the name in the context signature. If a receiver argument is specified, it is used for overloading resolution, as well.
In contrast to usual programming language syntax, the name of the constructed instance must be specified as the receiver of a constructor application. This reflects the fact that behavior let T t in new t.T(1,2), for example, does not actually describe the construction of a new object, but the action of running the constructor for some object, bound to symbol t.
Each argument in the argument list can correspond to an in, ref, or out parameter. The usage of keywords out and ref for invocation arguments follows C# syntax.
The offered signature of an invocation is defined as follows:
For a machine invocation, it is the machine context signature.
For an action invocation, it is the signature containing only the specified action.
For a negated action invocation, it is the context signature of the behavior.