Alloy数组模型

Question

我刚开始学习 alloy 模型语言，并试图在 Alloy 中编写自己的数组模型。但是，我无法从关系中提取索引。这是我的签名和事实：

sig Element {}

one sig Array {
  // Map index to element
  IdxEle: Int -> Element,
  // Length of the array.
  length: Int
}

fact Index {
    all r : IdxEle | r.Int >= 0 and r.Int < length
}

我遇到的错误是

This must be an integer expression.
Instead, it has the following possible type(s):
{none->none}

我查看了参考指南，但找不到提取关系的 idx 字段的方法。有人可以帮帮我吗？谢谢

Answer 1

首先，您模型中的 r 是 Array->Int->Element 类型，因此无法计算 (Array->Int->Element).Int，因为元组中的最后一列是 Element 类型，而不是您看起来的 Int期待。 (加入Alloy时，左边最后一列必须和右边第一列类型相同。)

其次，有更简单、更灵活、更易读的方式来表达你想要的：

sig Element {}

let range[start,end] = {  i : Int | i >= start and i < end }

one sig Array { index : Int -> Element } {
    index.Element = range[ 0, len[this] ]
}

fun len[ array : Array ] : Int { # array.index }

第三...有一个内置类型供您使用，名为 seq。它拥有您想要的一切，甚至更多。

Alloy数组模型

Alloy Array Model

testing

modeling

alloy