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

Question

我最近开始尝试用于一个项目的合金，并且遇到了一个问题不均匀的问题。这是一个简单的例子。我有四个特征：

• 字
• 定义
• 文件：文件有一个文本（单词序列）
• 字典：字典单词序列映射到一个定义序列（保持简单，让我们说，一个词应该有一个确切的定义）

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

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 

所以我的问题是：

1. 如何约束字典，这样的字典映射每个单词只有一个定义？在上面的代码中做它是正确的吗？

2. 如何通过断言检查此约束是否受到尊重？显然的代码位不起作用，因为w in dict.entries和w->def in dict.define不具有相同的参数数量，和我“中，可以使用相同的元数只有2倍之间的表达”得到错误信息......

Answer 1

我认为你正在努力与seq和assertions多于arity。

• seq在合金中不是很常见，您只有在需要更改元素排序时才使用它。在这个例子中，我没有看到当前描述中需要排序。
• 断言验证整个模型的不变量。你试图断言的更多的是事实你在模型中声明的比你断言的更多。如果您定义了操作并且想要验证某些事情永远不会发生，那么断言很有用，无论这些操作如何执行以及以何种顺序执行。即该断言验证模型的后果，而不是事实。 （尽管有时用换句话来验证某些东西是有用的。）
• 合金在通过全球表导航时非常有用。尽管看起来面向对象，诀窍是了解这些字段实际上是连接的全局表。 （这是我花了很长时间才得到的。）
• 模型中不应该有冗余信息。您可以使用define表中的功能对entries,defseq和define进行建模。
• 基本语言非常强大。对于这种大小的问题，您通常不需要任何实用程序。特别是在你感受到合金的关系模型后，关系似乎相当多余。

好了，一步一步：

一个文件是单词的序列：

我只想做一个文档，因为这更加自然和轻松了许多组字的使用。在这个的问题，单词的顺序不起作用，所以使用正常设置好像看起来好吗？ （算上的话就需要一个起）

sig Word {} 
sig Document { 
    text: Word 
} 

字典单词序列映射到的定义（保持它的简单，让我们说，一个词应该有一个确切的定义）

序列

我认为你的意思是说一个词典可以将一个这个词翻译成一个定义吗？每个字是否都有条目？还是有一些词有条目？你说'我'作为一些单词有一个定义？如果是这样的：

sig Definition {} 
sig Dictionary { 
    define : Word -> one Definition, 
} 

的define表（其是Dictionary->Word->Definition）具有约束，对于给定Dictionary->字组合，必须有one定义。这意味着并非所有的单词都必须在表格中，但是如果一个单词在表格中，那么必须有一个定义。 （你可以用其他约束来建模，最好是写出一张表并查看列）

您可以将entries定义为词典中的Word集。您还可以模拟这更好的功能：

fun Dictionary.entries : set Word { 
    this.define.univ 
} 

第一个加入选择在define表this词典并删除第一列。第二次加入删除最后一列。

而且类似的defseq：

fun Dictionary.defseq : set Definition { 
    this.define[univ] 
} 

盒加入[]刚刚加入方括号与之前的表的第一列内，留下定义列。那就是：

(univ).(this.define) 

如何检查此约束得到尊重与断言

我认为这是不明确的，你尝试断言什么。 （这是你发现的一种正式语言的力量！）在合金中你状态作为一个事实，词典中的一个词映射到一个定义。没有必要断言你定义为事实的东西。在你断言你首先需要更多的定义之前，

通常你会开始编写一个谓词，然后查找模型的例子。例如，如果我们想看到的无限词典的那么我们可以写一个：

pred show(d : Dictionary) { 
    d.define.univ = Word 
} 
run show for 5 

在这个例子中，你会看到一个字典，每一个字都有一个定义。

我写了一个博客，可能对您有用：http://aqute.biz/2017/07/15/Alloy.html