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>
{
// ...
}
}
Related Topics
Inheritance | Template classes