合金术语：签名“声明”和签名“引入”原子

Question

考虑一下：

sig A{}

那是什么？

答案：这是一个签名声明。

它有什么作用？

答案：它引入一组原子。 （参见软件抽象的第 93 页）

声明和引入轻量级正式建模社区中的标准术语吗？

为什么术语不是这样：

这是什么？答：这是一个签名定义。

它有什么作用？答案：它创建一组原子。

或其他一些术语。

Answer 1

“声明”是编程或规范语言中的一个标准术语，用于引入 (-;) 一个变量而不给它一个值。我使用术语“引入”而不是“创建”来避免暗示会立即产生操作效果（因为原子集是由约束求解确定的）。