理论计算机科学电子笔记128（2005）37-52www.elsevier.com/locate/entcsAlloy中数据无关系统的一个小模型定理Lee Momtahan1牛津大学计算实验室，牛津OX1 3QD，英格兰摘要Alloy是一阶逻辑的扩展，用于建模软件系统。Alloy有一个全自动分析器，它试图通过在有限范围内搜索反例来反驳Alloy公式。 然而，找不到反例并不能证明公式正确。的系统在类型T中是数据独立的，如果在类型T的变量上允许的唯一操作是输入，输出，赋值和相等测试。本文用与Alloy密切相关的语言给出了一个定理，它适用于数据独立系统的模型。 该定理为这样的类型T计算阈值大小。如果在阈值处没有发现反例，则该定理保证将T上的范围增加到阈值之外仍然不会产生反例，并且可以完成对数据独立系统的分析。保留字：数据独立性，模型发现，合金。1介绍自动化的逻辑公式检验工具是一种重要而通用的工具。许多实际问题可以归结为某个公式在某个逻辑理论中是否有效的问题。模型发现是一种替代定理证明的常用方法。模型发现者试图通过寻找反例来反驳一个公式。这种搜索是由用户确定的有限范围限制的，虽然存在反例表明公式无效，但找不到反例并不能证明公式有效。分析不完整。1电子邮件：leemo@comlab.ox.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.00338L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）37Alloy [3，4]是用于软件建模的一阶逻辑的扩展合金分析器是相关的模型查找器，需要一个范围来确定每个相关的类型变量，用于搜索反例的载体集的最大大小。运行合金分析仪时，用户必须为每个类型变量本文的贡献是给出了一个小模型定理（SMT），它适用于合金的特定情况下。SMT为某些公式生成阈值范围。如果合金分析仪确定在阈值范围内不存在反例，则SMT证明在任何范围内都不存在反例，从而完成分析。SMT通过利用Alloy Analyser为Alloy的一个片段带来可决策性结果。事实上，该定理通常不会为所有类型变量产生一个整体阈值范围当前定理通常在单个类型变量T上产生阈值，并且一旦用户确定了其他类型变量的大小，该定理给出阈值范围，并保证如果在该范围内没有找到反例，则通过仅增加T的载体集的大小而不存在。这使用户不必确定作用域的某些方面，并且如果用户可以确定其类型变量集的先验边界，则可以完成检查。未来的工作将着眼于改进该定理，以在更广泛的情况下处理多个类型变量。概况. 第2节简要介绍了Alloy，并介绍了一阶逻辑的数据独立性和可判定片段的相关工作。第3节给出了Alloy的内核语言的稍微修改版本的正式定义然后在第4节中给出了一个示例问题，使用非正式参数为问题中的一个基类型确定。下面的部分给出了SMT的形式证明。最后一节讨论了如何为未修改的Alloy内核语言生成SMT，以及SMT的其他可能增强2合金及其他相关工作。合金Alloy [3，4]是一种建模语言，由一阶逻辑和集合及关系组成。它大致上是Z符号的子集[8]，并且与UML的OCL [5，10]有相似之处Alloy旨在将模型检查器所提供的自动Alloy Analyser是Alloy语言的模型查找器分析器首先将Alloy语言中的公式翻译成更小的Alloy内核语言（AKL）[3]。因为分析器被赋予有限范围，所以它可以将AKL公式转换为布尔公式，使得布尔L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）3739当Alloy内核语言公式（以及原始公式）在给定范围内具有模型时，公式具有模型[2]。 测试对于布尔公式，Analyser包装了现成的SAT求解器，如SATO [12]或RelSAT [1]。数据独立性。非正式地说，一个系统对于类型T是数据独立的，如果它只能输入、输出和存储这种类型的值，以及在它的变量中复制它们。这种系统的控制流程不受不同值的影响;除了相应的输出数据外，改变输入数据不会改变行为。由于控制流程与使用的类型无关，因此可以在此类系统的验证中加以利用。这些严格的数据独立性条件通常可以放宽，以允许类型变量之间的相等测试，以及类型上的未解释常数数据独立系统非常常见，例如通信协议通常在通信类型中是数据独立的。存储器或数据库系统在它们存储的值的类型以及地址的类型可以通过有限实例化方法检查数据独立系统可以发展阈值定理，它表明一旦一个系统在其数据独立类型的所有大小上都被验证到一个特定的值，那么这个系统对于该类型的所有非空实例化都是正确的。一阶逻辑的可判定片段。一阶逻辑（的扩展）的片段的判定过程已经被数学家和形式验证的背景下广泛研究如引言中所述，SMT有时会对与特定配方相关的每种类型变量给出阈值，其与合金分析仪一起产生该配方的决策程序。虽然在这种情况下，硬币与已知的可判定性的结果，这项工作的价值是把这些结果到特定的框架和合金的设置当公式中的一些类型变量满足允许SMT给出阈值的限制时一旦模型查找器的用户在自由使用的变量上设置了范围，SMT就可以在其他变量上生成阈值。这并没有给出所讨论的公式的判定过程，也不能被视为与已知的可判定性结果相一致，但当然仍然有利于用户。40L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）379--2{|{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}3改进的Alloy内核语言在做了一些初步的定义之后，本节介绍了一种基于Alloy内核语言（AKL）[2]的语言，称为Modified Alloy内核语言（AKL-M）。这是第5节中的小模型定理所适用的语言。 AKL和AKL-M非常相似，但差异的原因以及如何在未来版本的SMT中消除差异，将在第6节中讨论。图像和前像。 给定关系r：P（A×B），对于任意a0：A，a0在r下的像，记为a0r，定义为{（a，b）：r|a=a0·b}。类似地，对于任何b0：B，b0在r下的原像，记为r ≠b0，定义为{（a，b）：r|b=b0·a}。关系运算符。 如果r：P（A×B），则r表示r的转置。若r：P（A×A），则r+表示r的传递闭包. 如果r：P（A×B）和s：P（B×C），则ros表示r和s的关系合成。多重标记。设M=*，+，！、、怎么样？.符号 *、+、！、、怎么样？称为多重性标记，分别用于表示：任何，至少一个，正好一个，至多一个。对于每个m∈M，定义谓词σm如下：σ*（n）惠True，σ+（n）惠n ≥ 1，σ！（n）n = 1，σ？（n）优惠n≤1类型语法。让TypeVar表示类型变量的名称集合，让Unit∈TypeVar是一个可分辨名称。类型的语法是TypeExp：：=TypeVar M->M TypeVar对于任何类型表达式Y m->n Z，定义Free（Y m->n Z）={Y，Z}。原子，集合映射和载体集合。设原子是一个集合，其元素称为原子。集合映射是从TypeVar到原子集合的部分映射，它：具有有限域;使得其域的任何两个不同元素映射到不相交的集合;并将Unit映射到单例集合。在这个映射下的类型变量的图像被称为它的载体集。类型表达式语义。 对于任何类型表达式t和任何集合映射δ，使得Free（t）domδ，t关于δ的指称语义，写作[t]]δ，定义如下：[[Y m-> n Z]] δ ={r：P（δ（Y）× δ（Z））|（δy：δ（Y）·σm（#yr））（[2]这个符号基于Z标准[8]。 一套理解 X：Xp（x）f（x）是通过将f应用于X中的每个x而形成的，其中p（x）保持不变。参见[9] sec.5.2.L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）3741联系我们例如，Y* -> *Z表示Y和Z之间的关系，Y* ->！Z表示从Y到Z等的全部功能。Z表示Z的元素，并且Unit *->*Z表示Z的子集。表达式和公式语法。设Var表示一组变量名。表达式和公式的语法定义如下：Expr：：=Expr+ Expr联合公式：=| 高速&公路高速公路交叉口| Expr-Expr差异| 快递 快递导航| ~Expr转置| +Expr闭包|Forrmul a } c o m p r e h e n s ion|Formula}comprehension| VAR变量Expr子集中的Expr| ！公式否定| 公式&&公式连接| 式||公式析取|福尔穆拉|Form ula 乌尼河|为您提供最佳使用体验。|Formulaexistential类型映射和签名。类型映射是从Var到具有有限域的TypeExp签名是一个对（r， r），其中r是TypeVar，r是一个类型映射，而r是一个类型映射，并且r（v）：dom r·Free（r（v））是一个类型映射。减少类型表达式。虽然多重性标记对于类型表达式的语义很重要，但它们不用于类型判断。下面的函数是为了从类型表达式中剥离多重性标记而定义的：Strip（Y m->n Z）=Y->Z。类型判断。 给定一个类型映射，Γ，语言的类型系统由自然演绎定义，如下表所示。 在表中：W，Y，Z表示类型变量，v表示变量，e，d表示表达式，F，G表示公式。类型映射Γ，v：Y->Z表示Γ v（Y*->*Z）即与Γ相同的类型映射，但是将v映射到Y*->*Z。d&e和d-e的规则就像d+e。F的规则||G就像F&&G。一些v：Y的规则|F就像所有的V：Y|F.为简洁起见，将其省略。42L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）37δ--Γ，v：单位->YFY{v：Y}|F}：单位->YΓd：Y->Z，Γe：Y->Z在e中的rΓF你好！FΓF，ΓGΓFG&&Γ，v：单位->YFV：Y|F[Strip（r（v））=t]中文（简体）Γd：Y->Z，Γe：Y->ZΓd+e：Y->ZΓd：W->Y，Γe：Y->Z你好。e：W-> ZY->ZΓπ~e：Z->YY：Y->YΓ+e：Y->Y一个表达式e被定义为相对于Γ是良类型的，只要存在Y，Z∈TypeVar使得可以导出Γe：Y->Z。类似地，公式F被定义为关于Γ是良型的，只要Γ≠F。兼容的签名和公式。一个签名（f， r）和一个公式F（resp.表达式）被定义为兼容的，前提是F相对于Γ是良好类型的，并且出现在F中的任何类型变量（即通过量化或集合理解构造引入的）都属于Γ。实例化。签名（σ， Γ）的实例化是有序对（δ，η），其中δ是具有域σ的集合映射，η是具有域dom Γ的全函数，使得：σv：dom Γ·η（v）∈[[Γ（v）]]δ。语言语义学。给定一个签名和一个公式F（分别为表示，对于签名的任何实例化（δ，η），F相对于（δ，η）的指称语义，写为[F]]η由下表定义。在表中，单位=δ（单位）。（注：因此，表达式被解释为关系;公式被解释为布尔值）L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）3743δδ∀·≤[[d+e]]η=[[d]]η[[e]]ηδ δ δ[[de]]η=[[d]]η[[e]]η&δ δ δ[[d-e]]η=[[d]]η\[[e]]ηδ δ δ[[d. e]] η=[[d]] ηo [[e]]ηδ δ9δ[[~e]]η=（[[d]]η）δδ[[+e]]η=（[[d]]η）+δ δ[[v]]η=η（v）δ[[dine]]η=[[d]]η[[e]]ηδ δ δ[[！F]]η=<$[[F]]ηδ δ[[FG]]η=[[F]]η[[G]]η&&δ δ δ[[F ||G]] η=[[F]] η[[G]] ηδ δ δ[[{v：Y|F}]]η={y：δ（Y）|[[F]]η<${v→{（u nit，y）}}·（u nit，y）}δ δ[[所有v：Y|F]]η=δy：Y·[[F]]η{v <$→{（unit，y）}}δδ[[somev：Y|F]]η=δy：Y·[[F]]η{v <$→{（unit，y）}}δδ一致和有效的公式。 给定一个相容的公式F和签名（δ，Γ），F被定义为相容的当且仅当存在（δ，Γ）的实例化，比如（δ，η），使得[F]]η。F被定义为有效提供！F不一致。Scope. 给定一个签名（，Γ），（，Γ）的作用域Θ被定义为从到N∞的全函数。一个作用域Θ被定义为无限当且仅当∞ ∈ran Θ，否则它是有限的。在范围内一致且有效。给定一个公式F和签名（f，r）是相容的，并且（f，r）有一个作用域Θ，F被定义为在Θ内是相容的当且仅当存在（f，r）的一个实例化，比如（δ，η），使得[F]] η和Y：domδ#（δ（Y））Θ（Y）。F在Θ内有效，当且仅当！F在Θ内不一致。4生日簿示例在本节中，Alloy被用来建模一个简单的生日书程序3，并检查了关于该程序的一些断言。阈值生成的非正式的参数。签名姓名{}签名日期{}sig birthday Book {known：set Name，birthday：known ->！Date} fun AddBirthday（bb，bb’.birthday = bb.birthday ++}fun DelBirthday（bb，}fun FindBirthday（bb：生日簿，n：姓名，d：日期选项）{ d= bb.birthday[n]}[3]这个例子来源于[8]，Alloy的翻译是在www.example.com上找到的Alloy发行版中给出的一个例子http://alloy.mit.edu/。44L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）37assertAddWorks {allbb，bb'：日期簿，n：姓名，d：日期，d'：选项日期|AddBirthday（bb，&&b b ' ， n ， d ）F i n d B i r t h d a y （ b b ' ， n ， d ' ） = > d = d '}assert删除撤销{所有bb1，bb2，bb3：星期日Book，n：Name，d：Date|AddBirthday（bb1，bb2，n，d）&&DelBirthday（bb2，bb3，n）=> bb1.birthday = bb3.birthdaybb1.known=bb2.known}检查AddWorks（3个但2个工作日）Book检查DelIsUndo（3个但2个工作日）Book因此，Name、Date、Date Book被定义为类型变量。对于birthdayBook的每个元素，known是Name的子集，birthday是 从已知到日期的总函数。（->在此上下文中表示一般关系，并且！是一个多重性标记，使这个关系成为一个全函数。）AddBirthday为添加条目的操作建模（mapletn->d）到生日簿上覆盖操作符（++）用于覆盖可能已经存在的名称（n）的任何 条 目 。DelBirthday 对 删 除 指定 名 称 的 条 目 的 操作 进 行 建 模 。FindBirthday函数模拟了查找一个人的名字以查找其生日的操作。AddWorks断言，如果一个人DelIsUndo断言，如果一个人语句check DelIsUndo for 3 but 2 DelidayBook给出了DelIsUndo断言的检查范围：Name和Date有3个元素，而DelidayBook，2。在合金分析仪中运行此检查时，可获得以下反例：日历= {日历0，日历1}日期= {日期0，日期1，日期2}Name = {Name_0，Name_1，Name_2}已知= {ReaddayBook_0->{}，生日= {生日Book_0->{}，dayBook_1-> {Name_2 -> Date_2} }bb1@1 =bb2@2 = dayBook_1 bb3@3= dayBook_0 n@4 = Name_2d@5 =日期_2对此解释如下。最初，生日簿包含一个条目：Name_2的生日是Date_2。然后，添加一个条目，L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）3745都是一样的因为是同一本生日簿，所以没有变化。然后删除Name_2的条目这将导致一个空的生日簿。因此，生日簿的初始状态和最终状态是不同的，产生了一个反例。变量bb1@1、bb2@2、bb3@3、n@4、d@5是斯科伦变量，代表了公式中的泛量化变量在反例中取的值。回想一下，合金分析器的工作原理是试图找到一个否定有效性受到质疑的公式的模型。在对公式求反之后，将其转换为求反范式（NNF）并进行skolemized [2]。为了转换为NNF，使用德摩根定律将否定推到量化器中。Skolemization消除了存在量化变量。 如果一个变量在一个公式中被存在性地量化，而这个公式没有被泛量化器包围，那么它可以被一个标量代替如果一个变量在一个公式中被当然，一个公式有一个模型，当且仅当它的skolemized NNF有一个模型。当Alloy Analyser运行AddWorks检查时（在相同的范围内），没有发现任何反例。然而，这并不能证明断言有效，并回避了一个问题：在更大的范围内可以找到反例吗？ 特别是，是否可以通过仅增加Date的范围来找到反例？Date上的阈值由以下参数生成。首先，否定AddWorks断言，将其转换为NNF并skolemized。这产生了skolem变量bb@0、然后，假设这个公式有一个模型，当日期的范围是无限的。无论模型中的变量如何分配，涉及日期的变量分配都由一个表表示，其中每行对应于日期的特定值。例如，以下变量的赋值：Date = {Date_0，Date_1，Date_2，.} Date ={Date_0，Date_1，Date_2，. 个 文件夹名称 = {Name_0， 名称_1，名称_2}已知的= {ReadyBook_0-> {Name_0，Name_1，Name_2}，ReadyBook_1-> {Name_0，Name_1，Name_2}}birthday = {birthday Book_0->{Name_0 -> Date_0，Name_1 -> Date_1，Name_2 -> Date_2}，日历簿_1->{Name_0 -> Date_0，Name_1 -> Date_1，Name_2 -> Date_3} }bb@0 = dayBook_0bb’@1 = BirthdayBook_1n@2 =d@3 =日期_4将在表中表示（具有无限多行）为：46L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）37星期一预订0第一册d@3d'@4姓名0名称1名称2姓名0名称1名称2日期0√√日期1√√日期2√日期3√月4√√日期5...日期∞然后，将该表转换为新表：星期一预订0第一册d@3d'@4姓名0名称1名称2姓名0名称1名称2{日期0}√√{日期1}√√{日期2}√{日期3}√{日期4}√√{日期5.. .日期∞}这个结果表是通过选择Date的值形成的，这些值是在前一个表中具有等效行的Date值的类。Date的这些实际值（即原子）对于作业是否是模型并不重要;重要的是它们有六个，它们是不同的。上述转换可以在任何潜在的分配上重复。在前一个表中，列（由于多重性约束），因此不超过8行，其中不包含' '（即空白）。因此，任何赋值都不会有超过9个等价类，因此后一个表中最多有9行。因为所讨论的公式没有在Date类型上使用quantifier或set builder构造，所以当且仅当转换后的赋值是模型时，原始赋值才是模型（表中未包含变量的赋值，即不涉及Date，未更改）。因此，9是日期的阈值。合金分析器在日期范围为9时未找到模型。(This包括当由于语言的单调性属性范围小于9时搜索模型。可以肯定的是，在搜索模型时增加Date的范围是徒劳的。如果要增加日历簿或名称上的作用域，L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）3747×∀·Datewouldincreaseacordinglyto#DecidayBook#Name+3. 尚未生成所有阈值范围，但这在未来的工作中可能是可能的。5小模型定理在本节中，推导了关于AKL-M的SMT（第3节）。给出了证明的总体结构，但为了简洁起见，引理的推导仅作了概述。完整的推导可以在[7]中找到。可分辨类型变量。不失一般性，假设SMT为其生成阈值的类型变量是X。 这是一个固定的实体在整个证明，因此使用粗体字。在整个证明过程中，对X的使用提出了各种限制，并在本节末尾进行了总结。等效原子。 在签名（X， Γ）和集合映射δ的上下文中，δ（X）上的一族等价关系定义如下。这些关系由类型表达式t和这些类型表达式val：[[t]]δ的可能含义索引，并写成一个整型运算符：（val，t）。xx（val，Y m->n Z）xJ惠（（Y=X）xval=xJval）（（Z=X）valx=valxJ）在签名（δ， η）和它的实例化（δ，η）的上下文中，δ（X）上的另一个等价关系，写为δ，定义为：x<$xJ惠矩（v<$→t）：Γ ·x<$（η（v），t）xJ为了便于记法，将“0”的定义扩展到每个载波集。在除X以外的类型变量的载体集合上，X是恒等关系。等价类。对于任何原子y，设[y] n表示y的等价性clas。如果Y是任意可变的，则l et[]Y表示该元素{y：δ（Y）·[y]}。实例化的商。在给定签名S=（δ， η）和它的实例化I=（δ，η）的上下文中，I的商表示为I=（δ，η），并且由下式定义：domδ = 0Y：δ（Y）=[]Ydomη=domηv：domη·η（v）={（y，z）：η（v）·（[y]48L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）37SSSS我我δSS商集映射和商实例。设原子=P原子。商集映射的定义与集映射（第3节）完全相同，只是用Atom代替了Atom。类似地，商实例化的定义与实例化（第3节）完全相同，只是用商集映射代替了集映射。为简洁起见，这些定义不再重复。引理5.1设S是一个签名，I是它的一个实例，则I是S的一个商实例。证明大纲：为了证明I是一个实例化，需要检查dom Γ·η（v）∈ [[Γ（v）]]δ.Q与实例化及其商相关的函数。如将示出的，表达式关于实例化及其商实例化的语义可以使用以下函数来关联。 让S=（δ， r）是一个签名，而I=（δ，η）是它的一个实例。让Y m->n Z是类型表达式.定义：KI（Y->Z）：[Y->Z]]→[[Y->Z]]δLI（Y->Z）：[Y轴->Z轴]]→[[Y轴->Z轴]]δKI（Y->Z）（r）={（y，z）：r·（[y]n，[z]n）}LI（Y->Z）（r）={（y，z）：r·a×b}注意，[[Y *->* Z]]·K（Y-> Z）（L（Y-> Z）（r））= r。被禁止的建筑一组有限的公式可以与上述函数相联系。被禁止的构造如下，其中v：Var：所有v：X|......这是什么？ ，一些v：X|......这是什么？ ，{v：X|......这是什么？个文件夹即X上的量化或集合理解。但是，在以下特殊情况4中，集合解析不是被禁止的构造：{v：X|vinv}。下一个引理只适用于不使用禁用结构的公式。引理5.2设e是一个不使用禁止结构的表达式。设F是一个不使用禁用结构的公式 设S =（π，Γ）为4完整的Alloy语言的语法允许在表达式中使用类型变量，并使用此构造将它们转换为AKL因此，期望SMT容纳它。δδL. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）3749δδ一个相容签名，I =（δ，η）是它的一个实例。然后又道：（r_e：Y->Z）L_I（Y->Z）（[[e]]η）=[e]]ηSδδ（ΓF）（[[F]]η惠[[F]]η）证明大纲：这个引理的证明使用了表达式或公式的结构归纳法。作为变量的表达式的基本情况或在未被禁止的特定模式中使用集合理解，遵循实例化的商的定义Q尺寸以下函数将用于生成划分类型变量的载体集的等价类数量的X. 它的第一个参数是签名，第二个参数是作用域。如果π（v<$→（Ym->nZ））：Γ·Y=XπZ= X，则Size（S，Θ）=π∞尺寸（S，Θ）=（v<$→t）∈ΓSum（t）+（v<$→t）∈ΓProd（t）其他wis e其中Sum（t）被定义为0，除了任何Y：TypeVar\ {X}和任何标记m：{*，+，！、、怎么样？}：Sum（Y m->！ X）= Θ（Y），Sum（X！- > m（Y）= Θ（Y）Sum（Y m->？ X）= Θ（Y），Sum（X？- > m（Y）= Θ（Y）并且Prod（t）被定义为1，除了任何Y：TypeVar\ {X}和任何多重性标记m：{*，+}：Prod（Y！->mX）= Θ（Y），Prod（X m->！ Y）= Θ（Y）Prod（Y？- > m X）= Θ（Y）+1，Prod（X m->？ Y）= Θ（Y）+1 Prod（Y *-> m X）= 2Θ（Y），Prod（Xm-> *Y）= 2Θ（Y）Prod（Y +-> m X）= 2Θ（Y）-1，Prod（X m->+ Y）= 2Θ（Y）-1N.B. 虽然Size依赖于Θ，但它与Θ（X）无关引理5.3设S是一个签名，I =（δ，η）是它的一个实例，则#[]<$X≤Siz e（S，#<$δ）.证明大纲：回到第4节中的表格结构，我们可以看到，如果表格有有限个列，那么就有有限个等价类，当然不超过2的列数幂。使用多重性标记信息获得更紧的界限。Q50L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）37（Y）和（？ηη定理5.4（小模型定理）设F是一个不使用禁止结构的公式，S是一个相容签名。 设Θ是S的作用域。 令Θ J= θ {X <$→ Size（S，Θ）}。 如果F在Θ J内有效，则F在Θ内有效。证明证明等价的陈述是足够的：如果！那么F在θ内是一致的！F在ΘJ内是一致的。所以假设！F在Θ内是一致的。然后选择一个实例I=（δ，η），使得δY：dom δ·（δ（Y））≤δ通过定义一个实例化的量和引理5.3，得出#δ（X）=#[]<$X≤Siz e（S，#δ）. 但在逐点情况下，从它的定义可以看出，函数Size在其第二个参数中是单到n e的。因此，Size（S，#δ）≤Size（S，Θ），因此#δ（X）≤Size （S，Θ）=ΘJ（X）。由于将原子间的等价关系推广为除X以外的载流子集的恒等关系，故有：δ Y：dom δ X·δ（Y）= δ（Y）. Th建立了θj（Y）：domδ·#（δ（Y））≤Θ J（Y）。但是[！5.2.[2019 - 05 - 15 00：05：05] F]]。 就这样！F是一致的δδ在ΘJ内。Q回顾X的条件。在公式的检查中获得关于X的阈值的条件如下。兼容签名不能使用任何Xm->nX类型的变量。此外，公式不能在X上使用量化或集合理解构造（除非在特殊模式下允许-参见：禁止构造）。然而，在转换为否定范式之后，通过在应用上述定理之前对公式进行skolemizing，可以有效地允许X6进一步工作在未来，它是希望实现自动阈值生成的合金分析仪使用SMT的结果。然而，当前的SMT适用于Modified Alloy内核语言（AKL-M），而不是真正的Alloy内核语言（AKL）。AKL和AKL-M之间的区别涉及类型的语法。AKL中类型的语法是：TypeExpAKL= TypeVar-> TypeVar |TypeVar => TypeExpAKLAKL类型表达式是类型变量之间的关系，或者是从类型变量到类型表达式的总函数。这是唯一的区别。[5]事实上，在这种语言中，不允许在X上的存在量化嵌套在多个泛量化级别（在X以外的类型变量上），但是为将来的工作提出的更丰富的类型语法将允许这样的嵌套。L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）3751AKL和AKL-M之间除了语言语法的相应函数应用构造之外。使用递归定义的类型语法增加了证明的复杂性的SMT。具有这种类型语法的SMT的关键似乎是逻辑关系，如[6]中所使用的。尽管AKL-M有多重性标记，但AKL没有，在某种意义上，这里介绍的SMT比要求的更通用。Alloy分析器将完整Alloy语言公式中的多重性标记替换为公式的合取词，给出适当的限制（参见[3]）。但是，类型表达式中多重性标记信息的丢失会产生更宽松的阈值，可能导致状态爆炸。这个困难可以通过将完整的Alloy语言问题编译成基于AKL但带有多重性标记的语言（重用大多数现有编译器）来克服然后，SMT可以被应用于生成阈值。进一步的工作是提高小模型定理处理多类型变量的能力目前，该定理可以重复应用于多个类型变量，只有当它们之间没有关系时。当施加额外的限制时，可以处理多个类型变量。确认作者要感谢Andrew Martin、Jeremy Gibbons、RankoLaz i'c、GavinLowe和BillRoscoe对他们的贡献，以及英国EPSRC的支持。引用[1] 小罗伯托·J Bayardo和Robert C.施拉格使用CSP回看技术来解决现实世界的SAT实例。在第十四届全国人工智能会议（AAAI'97）的会议记录[2] 丹尼尔·杰克逊。自动化一阶关系逻辑。第八届ACM SIGSOFT软件工程基础国际研讨会，第130-139页北京：人民出版社，2000年。[3] 丹尼尔·杰克逊。Alloy：一种轻量级对象建模符号。ACM Trans. Softw.工程师，Methodol。，11（2）：256[4] 丹尼尔·杰克逊。软件的微观模型：轻量级建模和合金分析。技术报告，麻省理工学院计算机科学实验室，2002年。[5] 伊瓦尔·雅各布森、詹姆斯·兰博和格雷迪·布奇。统一建模语言参考手册。Addison-Wesley，1999年。[6] RANKOLAZI'C和D AV IDNOWAK. AUnifying i ng Apr oachtoD ata-ind epe n c e. 在第11届并发理论国际会议（CONCUR 2000）的出版物中，计算机科学讲义第1877卷，第581-595页Springer-Verlag，2000年8月。52L. Momtahan/Electronic Notes in Theoretical Computer Science 128（2005）37[7] 李·蒙塔汉一个简单的Alloy小模型定理技术报告，牛津大学计算实验室，2004年6月。[8] J. M.斯皮维 Z符号：参考手册。 Prentice-Hall，1992年。[9] 吉姆·伍德考克和吉姆·戴维斯使用Z：规格化，细化和证明。Prentice Hall，1996年。[10] 乔斯·沃默和安妮卡·克莱普对象约束语言：用UML精确建模。Addison-Wesley，1999年。[11] 皮埃尔·沃尔珀在命题时态逻辑中表达程序的有趣性质。 在第13届ACM SIGACT-SIGPLAN编程语言原理研讨会上，第184-193页ACM Press，1986.[12] 张汉涛。SATO：一个有效的命题证明者。自动演绎国际会议论文集（CADE'97），LNAI第1249卷，第272-275页，1997年
