合金：使用断言检查约束时的arity问题-Java 学习之路

我最近开始为一个项目试验合金，我遇到了一个不平等的问题 . 这是一个简化的例子 . 我有四个签名：

Word
定义
文件：文件有文字（一系列文字）
字典：字典将一系列单词映射到一系列定义（为了保持简单，让我们说一个单词应该只有一个定义）

这是一个最小的代码示例：

module dictionaries

open util/relation as relation

sig Word {}

sig Definition {}

sig Document {
    text: seq Word
}

sig Dictionary {
    entries: seq Word,
    defseq: seq Definition,
    define: Word->Definition,
}{
    //dictionary maps word to def only for the word present in dictionary
    dom[define] = elems [entries] function [define, elems [entries]]
    //content of the list of defintions
    defseq = entries.define
}

//assert all word in a  dictionary have a definition
assert all_word_defined {
    all w: Word | all dict: Dictionary | some def: Definition |
    //w in dict.entries implies w->def in dict.define
}

check all_word_defined

所以我的问题是：

如何约束字典，以便字典中的每个单词都映射到一个定义？在上面的代码中执行它是否正确？
如何通过断言检查此约束是否得到遵守？显然代码 w in dict.entries implies w->def in dict.define 不起作用，因为 w in dict.entries 和 w->def in dict.define 没有相同的arity，我收到错误消息"in can be used only between 2 expressions of the same arity" ...

1 回答

0
我认为你正在努力争取 seq 和 assertions 而不是arity .
- seq 在Alloy中不常见，只有在需要更改元素的排序时才使用它 . 在这个例子中，我认为没有必要在当前的描述中进行排序 .
- 断言验证整个模型的不变量 . 你试图断言的更多是你在模型中陈述的事实而不是你断言的事实 . 如果您已定义操作并希望验证某些事情永远不会发生，无论这些操作如何执行以及按什么顺序，断言都很有用 . 即断言验证了模型的后果，而不是事实 . （虽然有时用其他词来验证某些东西很有用 . ）
- Alloy在浏览全局表时非常强大 . 尽管面向对象，但诀窍是要理解字段实际上是连接的全局表 . （这是我需要很长时间才能得到的 . ）
- 您不应该在模型中有冗余信息 . 您 entries ， defseq 和 define 可以使用 define 表上的函数建模 .
- 基本语言非常强大 . 对于这种尺寸的问题，您通常不需要任何实用程序 . 在你感受到Alloy的关系模型之后，特别是关系似乎是多余的 .
好的，一步一步：

文档是一系列单词：

我只是将一个文档作为一组Word，因为它更自然，更容易使用 . 在这个问题中，单词的排序不起作用，所以使用普通集似乎没问题？（计算单词需要seq . ）
```
sig Word {}
 sig Document {
   text: Word
 }
```
字典将一系列单词映射到一系列定义（为了保持简单，让我们说一个单词应该只有一个定义）

我认为你的意思是一个词典可以将一个单词映射到一个定义？每个单词都有条目吗？或者是否有一些词有条目？你说'a'我把它当作一些有一个定义的词？如果是这样：
```
sig Definition {}
 sig Dictionary {
   define : Word -> one Definition,
 }
```
define 表（ Dictionary->Word->Definition ）具有约束，对于给定的Dictionary-> Word组合，必须有 one Definition . 这意味着并非所有单词都必须在表中，但如果表中有Word，则必须只有一个定义 . （您也可以使用其他约束对此进行建模 . 最好是写出一个表并查看列 . ）

您将 entries 定义为字典中的Word集 . 您可以将其更好地建模为功能：
```
fun Dictionary.entries : set Word {
   this.define.univ
 }
```
第一个连接选择 define 表中的 this Dictionary并删除第一列 . 第二个连接删除最后一列 .

和 defseq 类似：
```
fun Dictionary.defseq : set Definition {
    this.define[univ]
 }
```
框连接 [] 只是将方括号的内部与其前面的表的第一列连接，离开“定义”列 . 那是：
```
(univ).(this.define)
```
如何通过断言检查此约束是否得到遵守

我认为你试图断言的不清楚 . （你发现这是一种形式语言的强大功能！）在Alloy中，你将字典中的Word映射到一个定义 . 断言你定义的事实是没有用的 . 在断言之前，首先需要更多定义 .

通常，您开始编写谓词，然后查找模型的示例 . 例如，如果我们想看到无限字典之一，那么我们可以写：
```
pred show( d : Dictionary ) {
     d.define.univ = Word
}
run show for 5
```
在此示例中，您将看到一个词典，其中每个单词都有一个定义 .

我写了一篇可能的博客对你有用：http://aqute.biz/2017/07/15/Alloy.html
回复于 2024-04-29T07:04:25+08:00

合金：使用断言检查约束时的arity问题

1 回答

相关问题