typedef with invariant 和 nomal typedef 之间有什么不同

Question

我在一个例子中遇到了一行代码，我不明白它是如何被使用的，以及使用这种类型的声明有什么好处。以下是从该示例中提取的部分代码

const uint16_t cycles = 8;
typedef uint8_t invariant(value < cycles) TIndex_t;

struct TData
{
uint16_t readings[cycles];
volatile uint16_t sum;
TIndex_t index;

void addReading(uint16_t arg)
writes(*this; volatile)
pre(invar())
pre(arg <= 1023)
post(invar())
{
   sum = sum - readings[index] + arg;
   readings[index] = arg;
   index = static_cast<TIndex_t>((index + 1u) % cycles);
}
void init()
writes(*this; volatile)
post(invar());

ghost(
    bool invar() const
        returns((forall r in readings :- r <= 1023) && sum == + over readings);
)

这是 GNU C++，据我所知，结构是一种 class 定义

Answer 1

这不是纯 C++。

看起来有人编写了编译器扩展或一系列宏，以允许为代码块指定前置条件和 post 条件。

你将不得不问那个人。

（顺便说一句，这就是为什么仅 "extracting code" 常常不足以理解；您需要观察 完整上下文 以便知道发生了什么。在这种情况下，上下文包括定义 and/or 在别处找到但未包含在您的问题中的文档。）

typedef with invariant 和 nomal typedef 之间有什么不同

What is different between typedef with invariant and nomal typedef

c++

gnu

avr

atmel