理论计算机科学电子笔记184（2007）171-187www.elsevier.com/locate/entcs从谓词到程序：方法语言的语义David Faitelson，James Welch和Jim Davies牛津大学计算实验室Wolfson Building，ParksRoad，Oxford OX1 3QD UK摘要本文解释了如何声明性的方法语言，基于Z和B的形式符号，可以作为自动代码生成的基础。语言用于描述预期效果对象模型组件上的操作或方法;每个方法由一对谓词定义：一个前置条件和一个后置条件。在自动合并模型不变量之后，包括那些从类关联中产生的不变量，这些谓词在被翻译成命令式程序之前被扩展-再次自动扩展-以解决一致性，定义和依赖性问题。其结果是一个正式的方法转换成完整的对象模型，工作系统。保留字：形式化方法，声明式编程，对象建模，最弱前提1引言从更高级别的规范生成代码的实践，有时被称为自动编程，可以追溯到20世纪70年代初。尽管任意组合程序的开发（如排序和搜索算法）仍然过于复杂，无法有效地机械化[6]，但在特定应用领域可以取得相当大的进展。一个早期的例子是用于流处理的Model II语言[13]，其中程序可以从传入和传出记录之间的预期关系的描述中生成。最近的一个例子是笛卡尔语言[9]，它已被用于从关闭要求的正式描述中生成控制系统的一部分。在不久的将来，我们可能会看到更多的例子：从领域特定语言的精确描述中生成代码是微软正在开发的“软件工厂”方法的本质1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.03.021172D. Faitelson等人理论计算机科学电子笔记184（2007）171这里解释的方法语言，在以前的SBMF研讨会[5]中一般描述的方法的一个方面，旨在生成对象数据库：数据存储，其中信息被组织为对象的集合，并通过相关的方法进行操作。它的语法基于Z [16]和B [1]语言的各个方面;它的语义基于Z [16]和精化演算[11]。生成过程的第一阶段的正式基础已经建立[18]，其中方法被扩展以考虑不变量和引用本文的贡献是给出了扩展方法语言的形式语义，从而精确地解释了扩展谓词如何转换为程序语句。本文首先解释了助推器的方法。然后，我们介绍了一种原始方法和组合子的语言。第4节给出了这种语言的形式语义，使用了类似于Z [4]提出的最弱前提的概念，以及Dijkstra保护命令语言的修改版本在第5节中，我们解释了如何分析和转换方法，以考虑后置条件中的一致性，依赖性和定义性问题2一种正式的、特定领域的建模语言在[5]中首次描述的booster语言旨在生成软件组件，其设计是：• 转换-操作的预期效果可以根据操作执行之前和之后的输入、输出和属性的值来描述。• 顺序-在任何一个时间，最多只能有一个操作作用于组件中的数据;当前操作必须在下一个操作开始之前完成读取或更新数据。在语言的应用中，组件被描述为对象模型，其中数据被组织成类，并通过相关的方法进行操作每个方法都被声明为一个三元组：一个在调用方法之前必须满足的前提条件;一个可以更新的属性的更改列表;一个描述预期结果的后置条件。其中第一个是属性值和输入的谓词。最后一个是对输入、输出和操作前后的值的谓词。例如，下面的声明引入了一个方法M，该方法仅在a的当前值小于1时才适用。该方法可能会改变b的值，并应确保b和c具有相同的（后）值。M（a<1|B|b=c）D. Faitelson等人理论计算机科学电子笔记184（2007）171173类会议属性参与者：SET（人。出席者：SET（Person. 介绍）时间表：时间表。会议容量：NAT方法添加Presenter（person_in：与会者|主持人|person_in：presenters）替换Presenter（existing_in：演示者&new_in：与会者|主持人|existing_in/：presenters&new_in：presenters）程晓波（真正|日程表.AddTalk ANDAddPresenter）添加额外容量（extra_in> 0|能力|容量= capacity_0 + extra_in）Fig. 1. Booster中的类声明数据属性的值可以是连续的--数字，字符串，或者它可以由一个或多个对象（SET或OSET）引用组成。在引用值属性的声明中，我们在目标类中标识相应的属性：类之间的关联是双向的。图1显示了类Conference声明的一部分。这个类的每个对象都包含一些属性，用来表示注册为出席者或演示者的人员;在每种情况下，属性的值都是对Person类型对象的一组引用。还有一个对Schedule对象的引用，描述了会谈和活动的时间表，以及一个容量数据：可以注册参加的最大人数。每个属性声明的附加组成部分-句点“后面的名称。'-标识目标类中相应的属性。例如，Person类的每个对象都有一个attending属性，其值记录了他们计划参加的会议集。AddPresenter仅适用于person_in已注册参加的情况，并且它具有将他们添加到演示者列表的效果ReplacePresenter替换现有演示者与新演示者的交互，前提是新演示者正在出席会议。ScheduleTalk将一个演讲添加到日程表中，并确保一个人被记录为演讲者之一;它是根据Schedule类的方法定义的，称为schedule.AddTalk，以及来自Conference的方法AddPresenter。AddExtraCapacity的定义表明后置条件可以在操作发生之前引用属性的值：capacity_0表示之前的capacity属性的值，capacity表示之后的值。174D. Faitelson等人理论计算机科学电子笔记184（2007）171图二. 生成过程图的文本1，结合适当的声明人和时间表，足以定义一个完整的工作系统。 模型的过程转换和编译--从声明性模型到可执行代码--如图所示。二、这个代码生成过程分为四个阶段：首先，属性和方法名称被完全限定，以考虑它们声明的范围;其次，方法前置和后置条件被扩展，以确保模型不变式得到维护。第二阶段的正式基础是早期论文的主题[18]。在该过程的第三阶段，分析方法定义以确定以下必要条件：• 每种方法的后置条件在对后置值和输出的要求方面是一致的;• 不同的、改变的属性的后值之间没有相互依赖性;• 任何出现在前置条件和后置条件中的表达式都要定义好。然后将这些条件添加到相关方法的现有前提条件中。最后，在第四阶段，完全扩展的定义被编译成可执行代码。这两个阶段的形式化基础方法语言的语义是本文的主题。3方法语言一个方法的前提条件可以是任何基于in-puts和before值组合的谓词，使用一系列布尔运算符形成。 更改列表只是一个属性列表。然而，后置条件必须由原语构成，这是该方法的一个• att= exp：属性att的值应该等于表达式exp的值，• exp：sAtt：表达式exp的值应该是集值属性sAtt的元素，• exp/：sAtt：表达式exp的值不应该是集值属性sAtt的元素，连同平凡的后置条件skip，使用conjunction（），implications（=>）和universalquantitation（forall），如下所示：D. Faitelson等人理论计算机科学电子笔记184（2007）171175CLASS方法示例方法方法1（a/= 0|甲乙丙 |a= a_0 + 1& b = b_0 +a）方法2（pre 2|方法3和方法4（d_in = e）属性a：NATb：NATC：SET（其他）。方法方法5（方法6，然后方法7）方法7（方法8或跳过）端图三. Booster中的方法• 职位1& post 2：post 1和post 2都应保持;• cond => post 1：如果conditioncond为true，则post应该保持;• 对于所有b_each：B. post1：对于从集合B中提取的每个b_each值，后置条件post1都应该为true。在上面，cond可以是任何谓词，但是post1和post2应该形成为原始后置条件（的合取）。强制性修饰用于识别输入、虚拟变量和• _in：来自方法上下文的输入• _each：量化中使用的虚拟变量;• _0：属性的前两个可能出现在任何条件下;_0，然而，只在后置条件中看到：例如，参见图3的方法Method 1，它将具有递增a的效果，并将b的值增加a的新值。有些方法，如上面的方法1，将在扩展中定义，具有显式的前置条件，后置条件和更改列表。其他将使用方法组合子定义：对于方法M1和M2，• M1 AND M2是一种方法，只要M1和M2都可用，它就可用;它具有两种方法的综合效果;• 只要M1或M2可用，则M1 OR M2可用;它具有M1的效应如果该方法可用，则它具有M2效应。• M1 THEN M2具有M1的效应，然后是M2的效应;它在以下任何时候都可用：M1可用，M1的效应将使M2可用。• ALL C each：C WHERE P DO M具有所有从M实例化的方法的组合效果，用于C的每个绑定，每个绑定满足谓词P。这个combinator是ANDcombinator的推广。176D. Faitelson等人理论计算机科学电子笔记184（2007）171我们要求AND的两个参数是独立的，在这个意义上，变量出现在一个变量的变化列表中，不会出现在另一个变量的前置或输入变量可以在执行时从环境中获取在实例化该示例，方法4：输入d_in的每次出现被e的值替换。一个方法表达式可以用在例如，方法2是通过预处理方法3和方法4（的实例化版本）的组合来定义的。基本方法SKIP总是可用的，它的执行对系统的状态没有影响。它可以与OR结合使用，以形成始终可用的复合方法。 方法7总是可用的，但是在方法8的前提条件之外没有效果，并且（因此）方法5的可用性仅受方法6的可用性的约束。如本例所示，方法可以在类级别声明，也可以在单个美德.先知-愿4方法的语义4.1一种部分程序我们使用部分程序语言（Dijkstra的保护命令语言的变体）给我们的方法语言一个语义我们的语言类似于Nelson [12]定义的语言，但具有不同的最弱前提概念。如果 你... 不再需要od运算符;任何程序都 可以可以用任意的守卫来前缀;任何一对程序都可以用作广义选择运算符Q的参数。该语言的语法由下式给出：命令|工作分配|guard|命令|命令|“input“输入变量列表“·”输入命令“|“var“变量列表“·”变量命令|“D. Faitelson等人理论计算机科学电子笔记184（2007）171177顺序组合有传统的解释，就像局部变量的声明一样：特殊的声明输入和输出表明值将从方法的环境（通常是事务管理器，但也可以通过实例化提供输入这种语言最弱的前提语义部分由以下子句定义：wp（skip，p） =pwp（a：=e，p） =p[a：=e]wp（g→c，p）=gwp（c，p）wp（c1 Qc 2，p）= wp（c1，p）wp（c2，p）wp（c1;c 2，p）=wp（c1，wp（c2，p））wp（decdec·c，p）=decdec·wp（c，p）其中dec可以是var或input，p[a：=e]表示用e替换p中的a所产生的谓词。wp的这个概念反映了我们的假设，即当守卫为false时，方法将不可用：任何执行尝试都将被阻止。因此，g→c实现p的最弱前提条件是守卫与命令的其余部分实现p的最弱前提条件的合取：wp（g→c，p）=gwp（c，p）这与Nelson [ 12 ]采用的概念完全不同，在Nelson[12wp（g→c，p）=<$gwp（c，p）在choice操作符的语义中有一个相应的区别：不需要天使的非确定性;任何后续守卫的约束将被包含在每个选择的wp4.2从谓词到程序为了获得方法的程序语义，我们将后置条件转换为命令，并将前置条件转换为附加的保护。第一个转换是复杂的，因为需要考虑两个组件的保护，第二个是需要考虑顺序组合中第一个组件的程序语义（THEN）。178D. Faitelson等人理论计算机科学电子笔记184（2007）171用扩展编写的方法的后置条件对应于一系列（可能是条件）赋值。在下面，我们写assign[[p]来表示与后置条件p对应的一系列赋值：赋值[[x = e]]=x：=e赋值[[skip]]=skipassign[[e：s]]=s：=s{e}赋值[[e/：s]]=s：=s\{e}赋值[[c => p]]=c→赋值[[p]]Q<$c→跳过[[p q]]=assign[[p]];assign[[q]]assign [[for allc_each：C. p]]= allceach：C·assign [[p]]4.3泛量化与迭代在我们在SBMF会议上提出的语义学的原始版本中，我们对泛量化器的使用施加了一个约束，即要求任何量化的表达式都应该对应于对不同属性的赋值序列。例如，这意味着我们不能实现以下后置条件对于所有a_each：A. p => a_each/：B它表达了这样的要求，即A中满足谓词p的任何元素都应该从B中删除，因为这个后置条件对应于对同一属性B的一系列赋值。然而，通过将量化谓词视为对应集合表达式上的等式，我们可以允许对这样的后置条件进行量化。我们首先观察到，如果量化的主体是一个合取，那么量化的表达式可以被认为是一个合取：对于所有i：I. conj1conj2（for alli：I. conj1）&（对于所有i：I. conj2）因此，我们只需要考虑体是一个可能受保护的原始后置条件的量化。如果主体是一个受保护的集合成员谓词（或其否定），则它等价于特征集是（或不）的子集的陈述D. Faitelson等人理论计算机科学电子笔记184（2007）171179不相交）所讨论的集值属性;在集合论术语中，我们观察到，i：I·P |P·e} si：I·P|P·e} s=其中，索引变量i在表达式e中可以是自由的，但在集值表达式s中不是。因此，这些条件可以安全地实现为我们的保护命令语言中的简单赋值：分配给所有人：I. P => e：s]]=s：= s{i：I|P·e}分配给所有人：I. P => e/：s]]=s：= s\ {i：I|P·e}每个赋值右侧的集合表达式可以反过来实现为对所讨论的集合的迭代。在任何一种情况下，最弱的前置条件很容易计算，作为一个简单的替代。4.4原始方法我们写execute[[M]来表示与方法M的后置条件相对应的受保护命令。如果M是用extension写的，那么这可以通过用局部变量declara前缀相应的赋值序列来获得。问题：执行[[（pre|变化|[email protected]]varchange0·change0：=change;assign[[post]]临时变量数组用于保存任何可能更改的值，因此，随后的赋值语句可以引用相关变量的前值和后值。4.5组合子的语义AND和THEN的保护命令语义都是按顺序组合给出的.这两个组合子之间的区别是AND的参数需要相互独立：两者都不需要更新出现在另一个的前置或后置条件中的任何属性180D. Faitelson等人理论计算机科学电子笔记184（2007）171execute[[SKIP]] =跳过执行[[（pre |M）]]=执行[[M]]执行[[M（i =e）]]=（执行[[M]]）[i：=e]执行[[M1AND M2]]=执行[[M1]];执行[[M2]]执行[[M1 OR M2]]=保护[[M1]]→执行[[M1]]Q<$guard[[M1]]guard[[M2]]→执行[[M2]]执行[[M1 THEN M2]]=执行[[M1]];执行[[M2]][[ALL C_each：C WHERE PDO M]]=allCeach：C·execute[[M]]OR的语义是一个确定性的选择：对应于每个组件的赋值序列由任何早期组件的否定保护前缀，从左到右阅读方法M的程序语义是通过用一个输入声明来前缀execute[[M]]，并从前提条件计算出一个guard：程序[[M]]inputinput[[M]]·保护[[M]]→执行[[M]]方法的输入变量可以通过递归检查方法语法来确定，取组件输入的并集-例如，inputs[[M1 AND M2]]=inputs[[M1]]inputs[[M2]]- 在除实例化以外的所有情况inputs[[M（i=e）]]=（inputs[[M]]）\{i}其中封装被替换的输入。D. Faitelson等人理论计算机科学电子笔记184（2007）171181对应于扩展中的方法的保护仅仅是所述前提的音译。合取或析取的守卫分别是简单的合取或析取组件守卫：保护[[（前|变化|post）]]= preguard [[SKIP]]= true保护[[（前|M）]]=预保护[[M]][[M（i = e）]] =（guard[[M]]）[i：=e]保护[[M1 AND M2]]=保护[[M1]]保护[[M2]]保护[[M1 OR M2]]=保护[[M1]]保护[[M2]]guard[[M1 THEN M2]]=wp（program[[M1]]，guard[[M2]]）[[ALL C_each：C WHERE PDO M]]=[[M]][[M]]为了获得顺序组合的保护（THEN），我们必须考虑第一个组件的程序语义，然后计算最弱的先决条件，以实现第二个组件的保护。4.6正确性我们的语义有一个自然的正确性标准：计算的守卫应该足够强大，以确保计算的程序将实现所述后置条件，被视为属性的前值和后值的谓词。如果生成过程的输出要与源模型中给出的规范一致，这正是方法语言语义所需要的。我们写post[[M]来表示方法M的后置条件，作为一个predicate来计算在这个计算中，AND、OR和ALL被替换为它们的逻辑等价物;THEN对应于一个合取，其中第一个方法的后值被第二个方法的前值标识，然后使用存在性隐藏。量化。我们对最弱前提条件wp的表述反映了这样一个假设，即我们软件组件的（自动生成的）接口将阻止一个方法被调用，除非它的（发布的）保护得到满足。因此，我们的语义的正确性标准可以表述为：guard[[M]]guidwp（program[[M]]，post[[M]]）182D. Faitelson等人理论计算机科学电子笔记184（2007）171对于由膨胀过程产生的任何方法MAND和ALL的参数应该是独立的，这一要求足以确保每个组合子都是保持正确性的，读者可以通过以下计算放心，正确性结果适用于用扩展编写的方法的简单示例。 考虑方法M1定义为M1（b=0|一|a=1）我们可以计算出保护[[M1]]=b= 0，wp（program[[M1]]，post[[M1]]）（b= 0→a：= 1，a = 1）优惠b=0wp（a：= 1，a = 1）优惠b= 0确认所需的含义成立。将此方法的语义与M2的语义进行比较是很有趣的，M2的定义如下：M2（真|一|b = 0 => a = 1）在这里，我们得到guard[[M2]]=true，wp（program[[M2]]，post[[M2]]）惠wp（b= 0→a：= 1 Qb/ = 0→skip，b = 0a = 1）惠wp（b= 0→a：= 1，b = 0<$a = 1）wp（b= 0→skip，b = 0→a = 1）优惠b=0wp（a：= 1，b = 0a = 1）b/=0wp（跳过，b= 0a = 1）优惠b=0真b/= 0（b= 0a = 1）惠真如果b= 0，这两种方法的效果相同：属性a的值将被设置为1。然而，如果b/= 0，那么M1（以及任何需要调用它的方法）将被阻塞，而M2将保持可用。然而，正确性结果并不适用于用extension编写的每个方法。一个方法的后置条件可能包括一个不可能的要求，或者我们没有办法计算出必要的赋值序列。此外，可能存在输入值和属性值的组合，对于这些组合，后置条件中的某些表达式的值是未定义的。D. Faitelson等人理论计算机科学电子笔记184（2007）1711835一致性、依赖性和定义性为了确保生成的实现是正确的，生成过程的编译阶段（其形式基础是上面定义的程序语义）之前是分析阶段，其中前置条件被加强以确保相应的方法不会被调用，除非它们的后置条件可以实现。5.1一致性后置条件有两种方式可以表达一个不可能的需求：它可以坚持一个属性取两个不同的值，或者它可以坚持某个值既是同一集合的元素，又不是同一集合的元素 如果这个要求是无条件的，那么我们别无选择，只能将方法的前提条件设置为false。否则，我们可以为后置条件确定一组充分条件一致--为了不出现不可能的要求--并将这些添加到方法的前提条件中。我们这样做，考虑现有的程序语义的方法，并计算最弱的先决条件，以满足后置条件。作为一个例子，考虑由下式定义的方法MM（真|一|a = 0&（c = 0 => a = 1））M的程序语义由下式给出：a：= 0;（c= 0→a：= 1，c/ = 0→skip）而实现a= 0<$（c= 0<$a = 1）的最弱前提是c/= 0。 在分析阶段，M的前提条件将被加强以产生以下声明：M（c/= 0）|一|a = 0&（c = 0 => a = 1））作为另一个例子，考虑图中给出的ReplacePresenter的定义。1.一、这里，如果两个输入existing_in和new_in具有相同的值，则后置条件是不可能实现的在分析阶段，这将被检测到，并且约束existing_in/= new_in将被添加到前提条件。生成的接口将不允许使用相同的值调用此方法对于两个输入。术语重写系统可以用来增加方法定义的可读性，并提高后续实现的效率。例如，后置条件x：sy/：s184D. Faitelson等人理论计算机科学电子笔记184（2007）171用程序语义s：=s{x};s：=s\ {y}，产生额外的计算前提：x∈（（s<${x}）\{y}）<$y∈/（（s<${x}）\{y}）一个合适的项重写系统会将其简化为x y。5.2依赖如果一个方法可以改变两个不同属性a和b的值，那么我们的程序语义可能无法实现任何后置条件，其中这些属性的after值是相关的。例如，方法M的程序语义，定义为M（真|甲乙丙|a = b& b = c）由a：=b;b：=c给出的，将无法实现后置条件，除非b的初始值等于c的初始值。和前面一样，我们可以通过计算程序语义的最弱前置条件（在本例中，b=c）来实现所述后置条件，并将其添加到方法声明的前置条件部分，来确保任何实现的正确性。然而，对于上述M等方法，结果可能达不到最初的预期。我们可以通过构造依赖图、进行拓扑排序和重新排序后置条件中的表达式来改进这一点，以便尽可能地在每个属性的值被用于确定任何其他属性的值之前确定它。例如，M的定义可以转换为M（真|甲乙丙b = c a = b）|&对于该方法，保证程序语义实现后置条件，并且不需要额外的前置条件5.3确定性后置条件中的表达式的值可能会因输入值和属性值的某些组合而被定义例如，在后置条件中，a = b/c当c的值为0时，表达式b/c的值将被定义。为了确保生成的实现的正确性，我们可以在后置条件中添加额外的约束，断言每个表达式的值正确地位于允许的范围内。在上面的例子中，我们将添加约束integer（a），断言a的after值是一个整数。这些约束对程序语义或生成的代码没有直接贡献D. Faitelson等人理论计算机科学电子笔记184（2007）171185然而，将它们包括在内使我们能够确定是否需要一个更强有力的先决条件例如，a =b/c&integer（a）的程序语义就是a：= b/c，但要实现后置条件（包括附加约束）的最弱前提是b/c∈integer。这可以通过合适的测试系统来简化，以c / = 0，并且可以将c/=0的结果添加到方法声明的前提条件部分。6讨论6.1应用在本文中，我们已经展示了如何在一个正式的，谓词符号语句可能会自动翻译，以产生可执行程序。这是可能的，因为后置条件的限制形式，它确保任何更新的属性的值是完全确定的;这似乎降低了符号作为抽象规范语言的价值，但经验表明情况并非如此。在计算方法的程序语义之前，我们扩展其定义以包括上下文信息：模型中其他地方描述的不变属性，以及关于正在开发的应用程序性质的假设例如，如果属性s在类A中由s：SET（B. t）的范围内并且方法M要求将对类B的对象b的引用添加到s，则如果需要，将扩展M的后置条件以包括将对当前对象的引用添加到对象b的对应属性a的值的要求。如果t是可选属性，则M的前提条件将被扩展为包括t当前未被设置的条件。此外，前置条件和后置条件都可以扩展，以考虑引用s或t的任何全局不变量，以及在类B中声明的用于添加对t的引用的任何前置条件。期望规范的作者包括足够的信息来确定任何被认为足够重要的属性的值，以包括在组件状态的描述中，这并不是不合理的：至少，如果规范旨在描述抽象设计，则不是这样。此外，我们可以很容易地推广方法符号以允许非确定性后置条件，并定义一个关系语义，允许使用熟悉的顺序数据细化概念来比较模型。在实践中，我们已经发现，符号是足够抽象的简明描述复杂的需求在预期的应用领域。我们相信这种方法具有更广泛的适用性，因为目前在开发大型应用程序时遇到的大多数编程问题并不需要发明复杂的算法[9]。相反，他们要求186D. Faitelson等人理论计算机科学电子笔记184（2007）171简单要求的组合的一致实现（通常是相当复杂的）6.2进一步发展对于基本方法语言的进一步开发有几种选择我们正在探索它作为UML类图中的动作语言的使用，作为对象约束语言OCL的替代[17]。我们正在考虑删除更改列表：在大多数情况下（见下文），它包含的信息可以从后置条件中推断出来。我们希望在后置条件中允许嵌套的泛量子化和存在量子化。然而，进一步发展的最大潜力在于设计建模语言的其他方面。在这里，我们的目标是提供更广泛的全球不变量的理论和实践支持我们也在考虑使用状态图来描述预期的工作流程，并以[15]的方式自动描述它们所包含的信息。一个早期的目标是扩展关联的概念，以包括一些指示，当删除对链接对象的特定引用时，是否应该删除该对象。目前，这可以从任何删除引用的方法的声明的更改列表的内容中推断出来：如果链接对象的类存在，那么该对象将被删除。然而，这是一种笨拙的记录意图的方法，因此增加了有价值的数据可能被无意中删除的风险;这也是源模型的方法声明必须包含显式更改列表的唯一原因。如果这种信息更直接地表达，作为协会的财产，那就更好了。即使改变列表从方法语言中删除，我们也希望从后置条件中提取相应的信息：它为设计者提供了有价值的确认，即方法只会改变预期的属性列表;它允许编译器确定哪些方法组合可以被允许并发执行。6.3相关工作在本文中，我们给出了一个语义的方法语言的设计是部分基于Z符号。在这样做的过程中，我们遇到了Cavalcanti和Woodcock在Z的最弱前提语义中描述的许多问题[4]。我们语言的局限性使我们能够以不同的方式解决这些问题：特别是，我们更容易推理连词和顺序组合。然而，他们的工作可以作为扩展这里提出的语义的基础。booster表示法与Object-Z [ 14 ]有共同的特性：引用类型的使用;类内操作的范围;使用点'引用属性和方法的能力。'符号。然而，定义语义的方法是相当不同的，反映了语义的顺序性质。D. Faitelson等人理论计算机科学电子笔记184（2007）171187系统正在考虑中。这里介绍的工作与Spec#编程系统[2]的最新工作以及Barnett和Naumann [3]描述的Boogie方法的扩展非常吻合。结合生成和验证技术将使我们能够处理更广泛的规范：不能成为程序的谓词可以作为断言包含在代码中。引用[1] J. - R.阿布里尔B书：赋予程序意义。 剑桥大学出版社，1996年。[2] 迈克·巴内特，K。鲁斯坦·M Leino和Wolfram Schulte。Spec#编程系统：概述。在CASSIS 2004中，LNCS。Springer，2004.[3] 作者：Mike Barnett，David A.瑙曼朋友需要更多：在共享状态上维护不变量。在MPC 2004年，LNCS。Springer，2004.[4] A.卡瓦尔康蒂和伍德考克。Z的一个最弱前提语义。 计算机杂志，41（1），1998年。[5] J. Davies，C. Crichton，E.克莱顿湾Neilson，and Ib H.索伦森形式、演化和模型驱动的软件工程.载于Alexandre Mota和Arnaldo Dalla，编辑，2004年SBMF会议记录，ENTCS，2005年。[6] E. W. Dijkstra和W.H. 费金一种编程方法。Addison-Wesley，1988年。[7] J. Green field，K.肖特，S。Cook和S.肯特软件工厂：用模式、模型、框架和工具组装应用程序。Wiley，2004.[8] A. Kleppe，J. Warmer，and W.百斯MDA解释，模型驱动架构：实践和承诺。Addison-Wesley，2003年。[9] J. - Y.卢卡斯，J。- L.多莫瓦湾吉努角Jimenez-Dominguez和L.皮埃尔如何调和形式规范和自动编程：笛卡尔系统。在98年的亚太安全会议IEEE Press，1998.[10] Z. Manna和R. J·华丁格自动程序合成。 Commun. ACM，14（3），1971年。[11]C. C. Morgan. Programming From Specifications（2nd ed.）. Prentice Hall，1998年。[12] G. 尼尔森 Dijkstra演算的一个推广。 ACM翻译计划。Lang.系统，11（4），1989.[13] N. Prywes，S. Amir和S.沙斯特里在软件开发中使用一种非过程化的规范语言和相关的程序生成器。ACM翻译计划。Lang.系统，1（2），1979.[14] G.史密斯Object-Z Specification Language。Kluwer，2000年。[15] C.斯努克和M.管家UML-B：UML辅助的形式化建模和设计。技术报告，电子和计算机科学，南安普敦，2004年。[16] J. M. 斯皮维Z符号（第二版）。普伦蒂斯·霍尔1992年[17] J. Warmer和A.克莱珀对象约束语言：为MDA准备好模型。艾迪森·韦斯利2003年第二版。[18] J. Welch，D. Faitelson和J. Davies。自动维护关联不变量。2005年SEFM会议记录。IEEE Press，2005.地出现。
