CLASS and SINGLE CLASS

C++ Test Script Language

Syntax

[SINGLE] CLASS <native class signature> { <class assertions>* }

Location

C++ Contract Check Script

Description

The CLASS statement introduces a block describing assertions for a specific C++ class. This block is called a class contract. Assertions described in a CLASS statement also apply to derived classes, unless the SINGLE keyword is used.

Use SINGLE CLASS to describe assertions only for the <native class signature> class.

<native class signature> is a qualified C++ class name. It can refer to template classes.

For instances of template classes, the signature must follow the pattern:

template<> class_name<actual_parameters>

Note: The template<> sequence may be omitted in order to comply with deprecated usage, but it is best to specify it.

For template classes with generic parameters, the signature must follow the pattern:

template<formal_parameters> class_name

Note: The template<...> sequence may be omitted, but in that case it is not possible to use the formal parameters in the nested WRAP signatures).

<class assertions> can be one of the following:

WRAP
INVARIANT
STATE
TRANSITION

Examples

C++ source code example:

class A {

class B {

// ...

};

// ...

};

template<class T,int N> class C

{

// ...

};

C++ Contract Check Script example:

CLASS A

{

INVARIANT (/*...*/);

// ...

}

CLASS A::B

{

// ...

}

CLASS template<class T,int N> C

{

// ...

}

CLASS template<> C<char*,255>

{

// ...

}