DeclaredAction

An action is declared in a Cord configuration to represent an activity of the system being modeled or tested.

Declarations can be either strictly or weakly bound to existing methods in a referenced .NET assembly. A weakly bound action declaration is marked with the abstract keyword. It is bound if a matching method is found. A strictly bound action declaration causes a validation error if it is not bound to a method in the implementation (or harness/adapter). Configurations should bind actions only to implementation (or harness/adapter) methods, never to model methods. The link between actions and model methods is established through annotations to the model methods.

The implementation name and the action in Cord implicitly match exactly. However, the relationship between model method name and the action is determined by explicit annotation. It is possible to have a model method associated through action attributes of a different name. This is transparent to the Cord script.

Syntax Definition

DeclaredAction ::= action [ exclude | abstract ] [ event ] [[ Namespace. ] Class. ] Method [ where ConstraintList ] .
Method ::= [ static ] Type [ QualIdent ] ( [ ParameterList ] ) .
ParameterList ::= [ out | ref ] VarDeclaration { , [out | ref ] VarDeclaration } .
VarDeclaration ::= Type Ident .
ConstraintList ::= ( Ident in Domain { , Ident in Domain } ) | EmbeddedCode .

Atomic Actions

An action can consist of either a call-return pair of atomic actions or a single observation of an event. Calling a method on the system being tested is a control action. Returning from a method call is an observation action.

When an action is declared without the event keyword, the atomic call-return actions are included in the configuration's signature. Actions declared as events result in a single atomic action.

Examples

Example 1

An implementation assembly is referenced that contains the compilation result of the following C# code:

namespace Microsoft.Test
{
   public class MyClass
   {
      public static int MyMethod(int x) { ... }
   }
}

Tip

The model assembly uses another namespace.

The following Cord script passes validation with references to MyClass:

using Microsoft.Test;
config MethodAndEvent
{
   action static int MyClass.MyMethod(int x);
   action abstract event void MyClass.MyEvent(int x, int y);
}

This configuration has the following signature (set of atomic actions):

call Microsoft.Test.MyClass.MyMethod(int)

return Microsoft.Test.MyClass.MyMethod(int)/int

event Microsoft.Test.MyEvent(int,int)

Note

The call and return are part of the name of their respective actions.

The abstract action declaration does not have a binding in the C# code and, being an event, has only one associated atomic action.

Example 2

Declarations containing the keyword exclude allow hiding actions introduced in this configuration or in a parent configuration. exclude applies only to an atomic action.

using Microsoft.Test;
config OnlyEvent : MethodAndEvent
{
   action exclude static int MyClass.Method(int x);
}

This configuration has the following signature: event MyClass.MyEvent(int,int). For more information about using the exclude keyword, see Excluding Actions from a Configuration.

Action Parameter Types

Only certain types can be used as action parameters. They are:

1. Any value type. Includes integers, enums, floats and doubles, structs.

2. Strings. While string is a reference type, not a value type, Spec Explorer itself automatically treats this as a NativeType.

3. Reference types declared as native by the user. Reference types that are declared as native (in the model program) using the NativeType attribute.

4. CompoundValue and its derived types. The Spec Explorer type CompoundValue, and types derived from it, can be used as action parameter types.

5. User-defined reference types that have a type binding. User-defined reference types that are bound to an implementation type may be used. Use the TypeBinding attribute to establish a binding from a user-defined type in the model to an implementation type.

Action Parameter Domains

An action declaration can attach domains to its parameters. A domain is a set value that a variable may assume during exploration and test code generation.

Example 1

The following configuration declares parameter domains for x and y.

config Domains 
{
   action abstract int MyAbstractAction.Action(int x, int y)
      where x in {1..10}, y in {1..10};
}

Example 2

The following Cord configuration declares a parameter domain for x calculated by the (state-dependent) method MyClass.MyGenerator. This method is shown within the Cord action declaration as embedded C# code.

config CustomDomain
{
   action abstract int MyAbstractAction.Action(int x, int y)
   where x in (. MyClass.MyGenerator().);
}

using System.Collections.Generic;
namespace Microsoft.Test
{
   public class MyClass 
   {
      static int state;
      public static IEnumerable<int> MyGenerator()
      {
         yield return state+1;
         yield return state+2;
      }
   }
}

See Also

Reference

Configuration
TypeBinding Attribute

Concepts

Cord Syntax Definition
NativeType Attribute

Other Resources

Cord Scripting Language