如何创建100％声明模型？

Question

我正在创建一个简单的网络模型。网络包含节点。节点发送和接收数据。

这是建模网络的一种方法：每个节点都有一个“数据”字段，表示节点在时间t拥有的数据。每个节点还有一个“发送”字段，记录在时间t发送给其他节点的数据。

sig Node {
    data: Data -> Time,                   
    send: Data -> Node -> Time   
}

在100％声明性和100％强制性之间的范围内，我不认为该签名是在100％声明性方面。在我的第一段中，我没有提到有数据存储的节点，也没有关于保存已发送数据的记录。

还有，不是“发送”动词吗？这不是表明模型不像声明那样的标志吗？声明模型不应该只使用名词吗？

我希望我的模型处于频谱的100％声明端。要实现这一点，我必须简单说明“是”。我们开始做吧！

有什么节点：

sig Node {}

什么是在任何时间t，节点都有数据。

sig Node {
    data: Data -> Time
}

什么是网络在节点之间有线路。

sig Network {
    wire: Node -> Node
}

什么是数据d在时间t和t'之间的导线上...

让我到此为止。我描述的第二种方法是否更具说明性？有没有一种方法更具说明性？

如何以100％声明的方式建模网络？

Answer 1

我认为你需要将模型的语义内容（它是一个问题）与其中使用的名称分开。对我而言，声明性模型的本质是它记录观察 - 可能是关于状态，或关于转换等动态事物 - 用逻辑表达。另一种操作模型是通过构建原始动作序列来描述行为和状态。一个简单的例子：建模一个动作，从一个集合中非确定地选择一个元素。操作规范可能会将集合视为有序，然后使用循环遍历集合，在每一步抛掷硬币，并在折腾首次出现时返回给定元素。这模拟了直观的操作描述：“一次浏览一组元素，然后选择一个返回”。声明性规范只是说返回的值是集合的一个元素 - 没有其他需要说的。

关于在您的特定模型中使用名称，似乎对我来说更大的问题是这些名称是否直接传达了它们的含义。所以send对我来说不是一个非常有用的名字;一个更好的将是sentAt。