面向对象信息系统中的数据模型：建构逻辑与信息存储

理论计算机科学电子笔记153（2006）55-75www.elsevier.com/locate/entcs一种结构化的面向对象信息系统Mario Ornaghia，1 Marco Beninib Mauro FerraribCamillo Fiorentinia Alberto MomiglianoaaDipartimentoodiScienzedellbDipartimentodiInforormaticaeComunicazione，Universita`degliStudidell摘要信息系统中的一个核心方面是外部世界中数据的含义以及它们所携带的信息我们提出了一个建设性的面向对象的建模语言（COOML）的信息系统，基于建设性的逻辑件的信息。重点是定义适合于组织存储在OO系统中的信息的数据模型。基本的建构逻辑支持一种正确的存储、交换和阐述信息的方式。关键词：面向对象数据模型，构造逻辑。1引言软件信息系统S允许用户存储、检索和处理关于外部世界的信息，通常是数据库。我们可以在S所阐述的数据中区分出两个独立的方面：第一个涉及数据类型，而第二个涉及数据所携带的外部“现实世界”的准确地说，数据类型是一组数据以及相关的操作，其中重点是操作。相比之下，存储在S中的数据所携带的信息与它们的1CONT T AC T INGAU T HOR：OR N A G H I@ D SI. 联合国它1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.08.00656M. Ornaghi等人理论计算机科学电子笔记153（2006）55在现实世界中的意义。由于互联网上交换的信息量很大，因此根据数据的含义正确处理数据的需求变得越来越重要[6，15]。 引用[15]：“最近的统一愿景之一是语义Web，它提出了数据的语义注释，以便程序可以理解它，并帮助做出决策。基于语义的解决方案的范围也从数据和信息转移到服务和流程。语义注释数据的规范和正确处理是我们工作的基本动机：我们提出了一种面向对象的构造性建模语言（COOML，简而言之），其中数据的语义注释通过信息片段的构造性语义来形式化。这为我们提供了一个适合于OOIS（代表OO信息系统）的数据模型和一个构造性逻辑，形式化了带注释的信息片段的正确操作和交换我们在这里给COOML的主要特点，它的数据模型和一般架构的简要我们区分数据类型、信息类型和对象类型。 像往常一样，数据类型引入了一组数据和对它们的可计算操作。在COOML规范中，数据类型的选择是开放的。它们可以根据问题域和实现COOML规范所采用的编程语言来选择一个数据，比如说整数2，本身不携带任何信息为了获得信息，我们必须将其与问题域句子相关联，例如结构化句子指的是结构化的信息片段例如，句子COOML的数据模型基于信息类型，我们将其定义为与结构化句子类型相关的结构化信息片段类型。信息类型的元素称为信息值。COOML结构化句子是第4节中解释的构造性逻辑Ecom l（简称为Ecoml）的逻辑句子，[12]中提出的逻辑E的推广我们可以将类正规化，并可以用一种特殊的E_c_for_mula来表示。通常，对象具有动态的生存期和状态;类使用常见的属性和方法。我们的数据模型将对象状态形式化为可以根据外部世界解释的信息值，其预期含义（即信息值）在相应类的COOML规范中得到反映。这允许我们以人类可读的方式自动提取由OO系统的当前状态表示的信息片段由于逻辑Ec是构造性的，是S1∈C的一个推广问题中的S2M. Ornaghi等人理论计算机科学电子笔记153（2006）5557现实世界计算程序....DB域逻辑逻辑建设性COOML规范字典和世界属性（意义，本体）数据结构（DataStructure）Fig. 1. COOML架构域隐含地包含一个算法，用于将一个规范S1的信息值正确地转换为另一个规范S2的信息。因此，Ec语言的推理引擎支持根据以下内容进行信息提取：不同的信息类型（或视图）。COOML的多层体系结构增强了处理信息值的多视图和不同含义的可能性，如图1所示。计算层包括支持基本数据和操作的数据类型层和支持信息值计算的信息类型层。COOML规范级别在计算塔和问题域塔之间架起了一座桥梁它使我们能够根据问题域来理解信息值在顶部，我们有COOML逻辑层，它允许我们对规范进行推理。COOML对于问题域逻辑是开放的，即，对问题域的推理可以基于不同的逻辑，或者甚至可以是非正式的。我们在这里不承诺为问题域使用固定的语言，但是，为了具体起见，我们有时使用JML规范风格[3]，由关键字JML表示。我们提出COOML使用Java类（JL）语法。在第2节中，我们解释了信息片段的语义，并介绍了语言。在第3节中，我们展示了COOML规范如何转换为一组Java类。在第四节中，我们给出了一个自然演绎演算。那我们最后就今后的工作方向提出一些意见58M. Ornaghi等人理论计算机科学电子笔记153（2006）552COOML的数据模型在本节中，我们将解释COOML的数据模型。我们将各个方面分开对待。在2.1小节中，我们解释了问题域逻辑所要满足的最低要求。然后，在2.2小节中，我们介绍了信息类型和相关的语义。接下来（2.3小节），我们介绍COOML中的类规范和我们描述系统快照的方法（2.4小节）。第2.5节介绍了继承。2.1问题逻辑与意义存储在软件系统中的数据与它们在“真实世界”中的含义之间的联系通常（参见例如，[8]），分析必须生成一个包含规范中使用的抽象概念的字典，并选择数据类型（可能取决于实现语言）。分析阶段应该产生一种（正式或非正式）语言来谈论世界及其状态。我们称问题公式为这种语言的句子问题公式F可以依赖于具有来自所选数据类型的排序的变量，并且它可以通过接地替换来实例化。世界国家可以被形式化为经典解释。然而，也可以使用其他的问题逻辑，甚至允许非正式的解释。我们只需要假设实例Fσ可以被最终用户理解为在世界状态w可能成立或不成立的属性。在问题公式中，我们可能有与实现语言相关的表达式由于我们对OO方法感兴趣，COOML引入了一种对象标识有一个特殊的预定义数据类型Obj。排序为Obj的常量标识形式为o.C（）的对象和类谓词，具有以下含义：o.C（）在世界状态wi中成立，o是w的活对象。由于对象很少是孤立的实体，因此我们也使用以下形式的类谓词：o.C（e1，.，e n），通过环境变量e1，.，将类C的对象o链接到其外部环境， e n.例2.1作为一个例子，我们考虑一个简单的“收银机问题域”。该词典提供的术语包括：• 收银机，收银机对象的类，带有类谓词c.CashRegister（）。• 收据，收据对象的类;由于收据r是由收银机c绘制的，我们引入类谓词r.收据（c）。• Item，收据的项目类，具有（自解释）类谓词i.Item（r）和谓词i.inCatolog（）（项目i可用）。M. Ornaghi等人理论计算机科学电子笔记153（2006）5559∗--• 成本，不包括增值税的项目成本。我们引入非正式表达“cost：float is thecost of item：Obj“，其中“. . ” indicates a variable in an informal• 价格，包括增值税的项目价格。我们引入非正式表达式• 总计，一张收据的总金额。我们引入非正式表达在分析过程中，人们还必须设计出对手头的应用感兴趣的世界的一般性质在我们的例子中，我们指出，一个项目的价格p是由它的成本c通过问题公式p=c+c V AT/100获得的虽然是非正式的，但前面的陈述是严格的，使我们能够对问题域进行推理 我们称问题域逻辑为分析阶段的总体（正式或非正式）结果，包括问题公式的语言和一般问题域属性。2.2COOML规范在COOML中，对象包含根据规范（SP）结构化的信息值我们使用类似Java的符号; τx表示不同变量x1，.，类型τ1，.，τ n，对于c：τ也是如此。SP的语法定义如下：AT：：=PF| QSPBUP：：=对于{τ x|G（x）：SP}SP：：= AT|BUP|（SP。. . SP}|或{SP. . . SP}|EXI{τ x：SP}原子（AT）由任意问题公式PF和Q-公式组成.后者（对应于[12]的T-公式）的目的是在我们的建设性设置中嵌入经典真理。在我们的语言中，就像在JML中一样，泛量化是有界的（有界泛属性（BUP））。生成元G（x）是一个特殊的问题公式，对于有限多个基本实例c1，...，cm的封闭项;我们称之为项gen，由G（x）表示。我们假设术语生成是可判定的，源于分析阶段。我们写EXI{τx：P1. Pn}而不是EXI{τx：和{P1. P n}}和类似的缩写a FOR{. ：和{.. . }}specification;EXI{τ！x：P}表示唯一存在。我们现在讨论原子的非正式语义问题公式Aσ所携带的关于世界状态w的唯一信息是基本信息值真。这仅仅意味着Aσ在w中成立，如前一节所解释的对于Q公式，Q（或{P1. P n}）σ在一个有界的世界态中成立P j σ中的至少一个保持（在w中），Q（和{P1. P n}）σ holds i <$所有的P j σholds，60M. Ornaghi等人理论计算机科学电子笔记153（2006）55{|}----∈||Q（EXIτx：P（x））σ对于x在σ中的重新赋值δ成立i <$P（x）δ，并且Q（FORτx G（x）：P（x））σ对于x的所有重新赋值δ成立i <$P（x）δ，使得G（x）δ成立。对于一个规范P，P的信息类型IT（P）定义如下，其中信息值是从问题域的原始数据类型开始构建的列表它（A） = {true}，其中A是AT它（和{P1. Pn}）={（i1，...，in）|ij∈IT（Pj），1 ≤j≤n}它（或{P1. Pn}）= {（k，i）|1 ≤k≤n且i∈ IT（P k）}IT（EXI{τ x：P}） = {（c，i）|c：τ和i∈IT（P）}它（对于{τ x|G：P}）= {（（c1，i1），.，（c m，im））|m≥0且对于1≤j≤m，cj：τ且ij∈IT（P）}也就是说，信息类型根据相应规范的逻辑结构来塑造信息值。具体地，BUP的信息值是关联列表L= （（c1，i1），.，（cm，im）），其中c1，.，cm是由G（x）生成的项的元组。我们表示为dom（L）= c1，.，c m是L的定义域。我们指出它（P）不依赖于P的自由变量，即，它（P）=它（Pσ），对于每个置换σ。一个规范P赋予了属于以下的信息值的意义：它（P）。一条信息是一对i：P，其中i是（P）。 对于每一个基代换σ，i：Pσ在世界态w中的意义由关系w给出||= i：Pσ（i：Pσ在w中为真）定义如下：W|| = true：Aσ森林论坛Aσ在w中成立，其中A是ATW||=（i1，.，in）：以及{P1. Pn}σ森林论坛W||=ij：Pjσ，对于所有j=1，.，nw|| =（k，i）：或{P1... P n}σ当且仅当w|| = i：P kσW||=（c，i）：EXI{τ x：P（x）}σ森林论坛W||= i：P（c）σW||= L：对于{τ x|G（x）：P（x）}σ当且仅当（c∈dom（L）i <$G（c）σ在w中成立）且（（c，i）∈ L包含w ||= i：P（c）σ）我们可以很容易地检验w=i：Pσ意味着QPσ在w中成立。一个结构化的规格说明是根据其各部分的真实性来解释规格说明的真实性的，如下面的例子所示例2.2在例2.1的问题域中，我们可以通过下面的规范S（receipt）来指定一个质量标准S（接收）：{EXI{float total：\total是\receipt;}对于{Obj item |item.物料（入库）：EXI{浮动成本：\cost是\item;}的成本让我们假设，对于receipt=r 31，我们有一条信息（（17.05 true）（it1）（10 true））（（it2）（5.5 true）：S（r31），增值税是10%。我们可以自动提取以下人类可读信息：17.05是r31的总计，r31的项目为M. Ornaghi等人理论计算机科学电子笔记153（2006）5561||∈{{|}it1和it2，it1的成本是10，it2的成本是5.5（我们指出项目的价格分别是11和6.05为了确保人类的可读性，规范字典至关重要。还应该清楚的是，我们可以使用不同的等价字典。这是因为在一段信息i：P中，信息值i与其意义分离我们可以把它和一个具有相同信息类型P的等价属性PJ，而不改变所涉及的信息值或方法。一个封闭公理集合Ax的信息片段i：Ax是一个信息片段iA：A的集合，每个信息片段对应Ax的每个公理A。我们说w|| = i：Ax i w = i A：A，对于每个A Ax。 在下一小节中，我们用S定义的公理的信息片段来模拟OO系统S的状态。2.3COOML中的类规范在COOML中，我们通过问题域的o. C（e）类谓词引入类类C的对象的规范由以下形式的类定义提供，其中EC是一个问题公式，SC是一个名为PtyName的规范，MC是一个方法原型列表，可能带有前置和后置条件：C类ENVτ ethis.C（e）：EC（this，e）;PtyName：SC（this，e）}我们称EC为C的环境约束，因为它根据环境约束实例化类C的其逻辑意义由约束公理表示：ConstrAx（C）：Q（对于{Obj this，τ e|this.C（e）：EC（this，e）}）我们称SC（this，e）为C的信息结构，因为它描述了C实例所携带的信息值的结构和含义，根据类公理：Class Ax（C） ： 对于{Obj this，τe|this. C（e）：SC（this，e）}在后续中，自引用this被隐式地普遍量化，我们使用PtyName（this，e）来表示相应的公式SC（this，e）。一个OO系统是（由）类定义的集合S。我们将包含所有类的环境约束和S的所有类的类公理的一阶公理集Ax（S）与它联系起来。62M. Ornaghi等人理论计算机科学电子笔记153（2006）55\例2.3让我们介绍了与图2的UML图相对应的类规范。现金注册0.. 1收据0..*项目+入库总计：浮动+物料cost：floatcode：Stringprice（）：float图二. 收银机类图（A）ClassC{CashRegisterPty：或{EXI{Obj！receipt：receipt.Receipt（this）;}收据为空;}}班级回执{ENV{对象 现金|此.收据（现金） ：true;}接收Pty：和{用于{Obj item |getString（）：getString（）;}EXI{float total：\total是\this;}}}类项目{ENV{对象收据|此.项（收据） inCatalog（）;}itemPty：和{EXI{float cost：\cost是\this;}的成本EXI{String code：\code是\this的代码;}EXI{float price=price（）：\price是\this;}}/*确保结果=成本+成本 * 增值税/100*/浮动价格（）;}根据CashRegisterPty的说法，收银机只有一张收据或一张空收据。收据提供其项目列表（与ReceivtPty的第一个子属性关联的信息）和与ReceivtPty的第二个子属性关联的合计。最后，一个项目是由它的成本，它的代码和它的价格（与ItemPty相关的信息）描述的。通过floatprice=price（），我们表明price不是一个类属性，而是price（）方法返回的值相反，成本和代码是属性。对应于收银机系统的公理化是：ConstrAx（收据）Q（用于{Obj cash |this.Receipt（cash）：true;}）ConstrAx（Item） Q（用于{对象接收|this.Item（receipt）：this.inCatalog（）;}）类公理ClassAx（CashRegister）FOR{|this.CashRegister（）：CashRegisterPty（this）}{ Obj cash}的ClassAx（收据|this.收款（现金）：{对象收款}的ReceiviptPty（this，cash）}ClassAx（物料 |this.Item（receipt）：ItemPty（this，receipt）}M. Ornaghi等人理论计算机科学电子笔记153（2006）5563PP|||| PP2.4系统状态假设PC：ClassAx（C）是类公理ClassAx（C）的信息片段。事实上，C是（（ot）i）形式的信息值列表（可能是空的），其中o实例化了它，t是实例化环境变量e的项的元组。我们称PC为C类种群，作为一套。一个OO系统的种群P是它的类。我们说一个物体o属于总体Pi，并且P中有一个信息值（（ot）i）。一个群体P是有限的（一个OO系统有一个有限的对象集），P中的每个对象o在P中出现在一个唯一的信息值（（ot）i）中（一个对象属于一个OO系统的唯一副本）。Ax（S）的环境约束不包含当前状态的信息，因为它们是封闭的原子，w=true：A携带的唯一信息是A在w中成立。因此，我们让它们保持理解，我们用种群来识别系统状态，我们将系统状态的语义定义如下：定义2.4设P是OO系统S的种群，w是世界状态.则w|| = P：S i =(i) w=C：ClassAx（C）对于S的每个类C，其中C是类C的总体;(ii) 对于Ax（S）的每个环境约束A，A在w中成立我们现在展示如何为收银机系统生成一个种群，并为它生成一个世界状态wcash我们从一个CashRegister对象cr1开始：PCashRegister=（cr1（1（rcpt1 true）））指定CashRegisterPty（cr1）需要rcpt1。收款（cr1），用于在世界状态w中保存我们正在生成的现金。通过ClassAx（收据），我们必须为rcpt1构建信息值：P接收=（rcpt1（it1（1 true））（it2（1 true）（17.05 true）这意味着谓词it1.Item（rcpt1）和it2.Item（rcpt1）持有w 现 金，并且17.05是rcpt1的总计。我们必须为项目构建信息值（其中增值税为10%）：P项目=（（it1（（10 true）（“a15”true））(11true））(it2（（5.5 true）（“b121”true）（6.05 true）也就是说，10是它的成本，“a15”是它的代码，11是它的价格，所以on（注意，RCPT 1的总计实际上是IT 1和IT 2的价格之和）。生成的总体是上述总体的并集。填充对应于UML对象图，也称为系统快照[5]。例如，对应于上述64M. Ornaghi等人理论计算机科学电子笔记153（2006）55|| PPPCR1RCPT 1总计=17.05cost=5.5code=“b121”图三. UML快照人口如图3所示。在COOML中，快照可以以人类可读的格式打印出来，通过将信息值整理到相应规范的信息片段。例如，图4中示出了包含在先前群体中的信息的可能打印输出。我们注意到接收回执1：env rcpt1.Reception（cr1）;. Item（this）：it1.inCatalog（）;it2.Item（this）：it2.inCatalog（）;exi float 17.05：17.05是rcpt1第一项：env it1.Item（rcpt1）exi浮动10：10是它的成本string“a15”：“a15”是it1的代码float11：11是it1的价格第二项env it2.Item（rcpt1）exi float 5.5：5.5是它的成本string“b121”：“b121”是it2的代码float6.05：6.05是 it2的价格见图4。 打印人口打印输出包含的信息比相应的UML图更多;事实上，后者可以由信息片段导出，而反之则不成立。显示快照的能力是理解OO的有用工具模型并且存在能够生成快照的系统（例如，[7]，基于OCL [17]）。事实上，OO规范的一个问题是一致性。例如，很容易构建具有不一致多重性的UML类图在我们的方法中，一个OO系统S是一致的，如果它有一个一致的人口，并且是一致的，如果至少有一个世界状态w使得w=：S。例如，前面的人口是一致的，因为存在一个世界状态wcash，使得S的约束公理在wcash中成立，并且：w现金||=P现金注册 ：ClassAx（CashRegister）w现金||=P收据 ：ClassAx（收据）w现金||=P项目 ：ClassAx（项目）IT2cost=10code=“a15”it1M. Ornaghi等人理论计算机科学电子笔记153（2006）5565{|}0..10..*+入库+物料price（）：floatcost：floatcode：String总计：浮动项目收据现金注册{{{|}一般来说，总体的一致性是不可判定的。我们正在研究一种基于从信息片段中提取被假设为真的原子的部分解决方案如果问题域规则具有受限的语法，则可以利用标准结果，例如Horn理论的一致性2.5类层次结构在COOML中，我们可以用继承和（可能的）方法重写来形式化子类：C类扩展了C1，...，CkENVτ ethis.C（e）： E C（this，e）; x1.C1（t1）;. ; xk. Ck（tk）;产品名称：SEC（this，e）MC}其中项t1，...，tk属于环境变量e. 注意，现在C的环境约束将其环境e与其超类C1，.的环境相关联， C k.SpecificationsSE扩展了从超类继承的Specifications。C的整个信息结构SC定义如下：SC（this，e） =和{SEC（thi s，e）SC1（x1，t1）. . SCk（xk，tk）}其中，SCj（xj，tj）可以递归地从其他子类继承Example 2.5让贴现折扣：浮动price（）：float图五. 收银机类图（B）类别CashRegisterCashRegisterPty：.}班级回执{ENV对象现金此.收据（现金）：真;收据Pty：.}类项目{ENV{对象收据|此.项（收据） inCatalog（）;}66M. Ornaghi等人理论计算机科学电子笔记153（2006）55\--项目：.}类折扣扩展项{ENV{对象收据|此.折扣（收据）：this.Item（receipt）;this.inCatalog（）;}DiscountedPty：EXI{float discount：\discount是\this;}的折扣/* 确保结果=（成本-折扣）+（成本* 增值税/100）*/浮动价格（）;}类CashRegister、Recipient和Item的公理保持不变。新类的公理是：ConstrAx（折扣）Q（对于{对象接收|此.折扣（收据）：this.Item（receipt）;this.inCatalog（）;}）{对象接收}的ClassAx（折扣）|此.折扣（收据）：和{DiscountedPty（this，receipt）;ItemPty（this，receipt）;}}3面向Java程序的派生我们概述了从COOML规范中提取Java程序骨架的过程。这在精神上类似于UML类图生成Java代码的方式。为了达到这个目的，最好将一个规范转换为合取范式EXI{τ x：和{B1. Bn}}其中每个Bj可以是原子、BUP或析取或…原子。 只要引入合适的新类，这种形式总是可以得到的。每一个范式的COOML类C都被翻译成Java类JC，它表示C的环境和信息值，并且它有Info getInfo（）方法来包装信息值，还有Explanation explain（Pty p）方法来提取面向人类的解释，我们将在下面详细介绍。变量τx成为JC的属性。对于每个公式Bj，我们产生一个属性如下：如果Bj是一个问题公式，我们插入一个注释;如果它是一个BUP，则生成一个辅助类，而如果它是或{.. . }，则引入int属性。这在图6中示出。以这种方式生成的类是Java程序员可以轻松理解的常规Java类;方法可以用通常的方式也一样。 每个类C具有两个相关联的类CInfo和CPty， 自动生成。CInfo是一个抽象的预定义类Info的子类，允许我们提取对应的信息值i Java程序的当前状态。提取的i具有由CPty定义的信息类型，CPty是预定义抽象类Pty的子类，用于表示COOML属性。更准确地说，Pty和Info有几个预先定义的子类，表示COOML属性和相应信息类型。Java程序员不需要知道这些M. Ornaghi等人理论计算机科学电子笔记153（2006）5567class CashRegister{//Exi：目标收据;//或者：int case;//1：receipt.Receipt（this）;//2：收据为空;/*************************************************** 信息提取，自动生成**************************************************/public void run（）{返回new CashRegisterInfo（this）;}/* 假设：p由CashRegisterPty隐含 */ publicExplanation explain（Pty p）{return getInfo（）.explain（p）;}}类收据{//env：Obj cash;/* this.Receipt（cash）*///Exi：浮动总额//然后//对于{Obj item| item.Item（this）：item.inCatalog（）;}_item的收货信息;//true：\total是\this的总和.... ‘‘information}class Item{//env：Obj receipt; /* this.Item（receipt）; this.inCatalog（）;*///Exi：浮动成本字符串代码;//然后//price=price（）;//true：\cost是\this的成本;//true：\code是\this的代码//true：\price是\this的价格;/*@需要cost>0;确保\result= cost + cost*VAT/100; @*/floatprice（）{//return0;}.... ‘‘information}图六、示例派生Java程序68M. Ornaghi等人理论计算机科学电子笔记153（2006）55类，但扩展Info的预定义子类ForInfo的类除外，例如示例中的ReceivtInfo程序员必须使用item的属性以预期的方式包装与项关联的信息值。为此，ReceivtInfo包含适当的方法来检索和更新存储在foritem中的项目;事实上，该类本质上包含专门用于项目的Java集合方法。对于每个类C，CInfo对象i具有信息类型CPty和方法i。explain（p），它根据属性p构建信息contt的解释;后者通常是CPty类的单例对象cpty，表示C的COOML规范中定义的属性。为了支持数据的多个视图，我们可以使用cpty所构造的属性。因此，对象p的一个方法意味着p。隐含（q）返回null或一个对象m，带有从它（p）到它（q）的map方法。提取m的算法是基于一个合适的逻辑演算N-D-C，并使用一组问题域规则（PR）。我们将在下一节中对此进行在这里，我们给出了第一个例子，展示了在方法explain中方法的可能用途。让我们假设，在类Item的上下文中，我们提供以下规则：\price是\thisJML的价格{price！= cost + cost V AT/100}错误：\价格应该是JML{cost+costV AT/100}蕴涵算法假设在PR规则中，基本操作和谓词（如JML规范）可以被评估。特别地，使用上述规则，该算法可以证明在类收据中的以下对于{Obj item|item.Item（this）：或{ok（this）;错误：\priceshould beJML{cost +costV AT/100}调用receipt对象rcpt的explain（p）方法，其中p实例化为上述error属性，通过调用ReceivtPty类的implies方法来识别蕴涵。相应的映射被生成，并将输入解释转换为包含（可能的）错误项列表的解释。Map和Explanation是预定义的类。Map对象表示转换信息值的算法，而Explanation对象表示一条信息，将信息值整理到相应的属性。这也支持语义注释数据的正确例如，对象的当前状态可以被包装到一条信息i：P中，并发送到不同的（可能是远程的）接口/上下文。每个人都可以以不同的方式使用i，根据其本地问题域规则映射它。PRM. Ornaghi等人理论计算机科学电子笔记153（2006）55694微积分我们的性质可以被翻译成逻辑E[12]的谓词语言的一个片段，E是一个具有有效和完整演算的最大中间构造性命题逻辑，其完整的谓词扩展尚未被研究。在E语言中，原子由信息类型为真的Q-公式表示，而逻辑连接词则引入结构化信息类型.如果我们用Q F表示每个问题公式F，并用相应的逻辑连接词替换AND，OR，EXI，FOR，则每个属性都变成了E-for mula。对于我们的框架，Ec，我们使用自然演绎演算NDc，其规则在表1和表2中描述。 为了简短起见，我们只考虑命题连接词的二元形式，n元扩展是显而易见的。类似地，我们给出了“单例”变量列表的量化器规则ND-C算法基本上是一个有界单向量化的直觉演算，一个引入有效问题公式蕴涵的规则PRPR规则引入了有效的问题域蕴涵，而I-Q允许我们推断任意有效的公式。Q只能从微积分的Harrop片段中消除关于参数的通常附带条件适用。我们现在显示出NDC的可靠性 与第2.2小节中给出的信息片段的序列有关。设Γ是一组公式{H1， . ，Hn}。 Byπ：r∈Cwe表示在计算中作为未解除假设H1，...， H n和结论C; γ ∈ IT（Γ）表示集合{i1，.，i n}，其中i j∈IT（H j），对所有1 ≤j≤n;w|| = γ：Γ σ意味着w|| = i j：H j σ，对于所有1 ≤j≤ n。定理4.1Letπ：Γ∈C是微积分NDc中 的 一 个 p r o，设γ∈它（Γ）. 然后，存在i ∈ IT（C），使得对于所有的世界态w和基替换σ，w|| = γ：Γ σ需要w|| = i：Cσ。证据证明是通过归纳π的结构。我们注意到，证明是建设性的，事实上，我们实际上建立了一个信息值的证明公式。因此，我们隐式地定义了一个算法，给定证明π和其假设的信息值γ，输出π的结论C的信息值。我们只分析一些重要的案例。70M. Ornaghi等人理论计算机科学电子笔记153（2006）55············Γ1·π1C1Γ2·π2C2I和Γ·π（C1C2）E和 j∈{ 1， 2}（C1C2）ΓCJΓ0Γ1，[C1]Γ2， [C2]·ππ0Cj或{C1C 2}·π1D·π2D或{C1C 2}I或j∈{1，2}E或DΓ·πC（t）Γ0·π0EXI{τ x：C（x）}Γ1，[C（p）]·π1DEXI{τ x：C（x）}IEXID[G（p）]·πC（p）对于{τ x|G（x）：C（x）}我为Γ0· π0G（t）[G（p）]· π或{C（p）B}Γ1·π1对于{τ x|G（x）：C（x）}C（t）GRE的或{对于{τ x|G（x）：C（x）} B}表1微积分证明π是：Γ1·π1C1Γ2·π2C2（C1C 2）I和假设w|| = γ：Γ σ。通过对子证明π1和π2的归纳假设，存在i1∈IT（C1）和M. Ornaghi等人理论计算机科学电子笔记153（2006）5571i2∈IT（C2）使得w|| = i1：C1σ，W|| = i2：C2σ。让我们取（i1，i2）∈它（和{C1C2}）;我们有w|| =（i1，i2）：和{C1C2}σ（根据需要）。72M. Ornaghi等人理论计算机科学电子笔记153（2006）55··∈||·H1，...，HnAPR如果A是一个原子，H1是……n→A是有效的PFΓ·πQ（和{C1C2}）QCjΓ·πCIQQCEQ和j∈{1，2}Γ·πQAEQA原子一Γ·πQ（对于{τ x|G（x）：C（x）}）对于{τ x|G（x）：QC（x）}EQFOR表2微积分 （续）：PR和Q规则证明π是：Γ0Γ1，[C1]Γ2，[ C2]·π0或{C1C 2}·π1D·π2DDE或假设w|| = γ：Γ σ。通过对π 0的归纳假设，存在i∈IT（或{C1C2}）使得w||= i：或{C1C2}σ。假设i =（1，i1），其中i1∈ IT（C1）（i =（2，i2）的情况也是类似的）。然后，通过对π 1的归纳假设，将i1与C1联系起来，存在iDit（D）使得w = iD：Dσ，从而得出结论.证明π是：[G（p）]·πC（p）对于{τ x|G（x）：C（x）}我为假设w|| = γ：Γ σ。令c1，...，c m是由G（x）生成的项，让我们考虑，对于所有1 ≤j≤m，通过用c j实例化参数p从π获得的证明π j。 通过归纳假设，当我们将真与原子G（c j）联系起来时，存在i j∈ IT（C（x））使得w ||= ij：C（c j）σ。让我们考虑列表L =（（c1，i1），.，（cm，im））。我们可以很容易地检查W|| = L：对于{τ x|G（x）：C（x）}σ.QM. Ornaghi等人理论计算机科学电子笔记153（2006）5573关于完整性，我们推测这对本文利用文献[12]中的技巧，研究了具有无界单向变量的N-D算子.74M. Ornaghi等人理论计算机科学电子笔记153（2006）55···ENVASS：receipt.Receipt（cr）{本地1：对于{Obj item |item.Item（receipt）：item.inCatalog（）;}ENVASS：[2]item.Item（receipt）;{PRULE：JAVA{check（item）;}item.Item（receipt）; =关注\receipt;证明：或{JAVA{！check（item）;} interesting\receipt;}}PROVE[GR1，2]：OR{FOR{Obj item |item.物料（收货）：JAVA{！return（i）;interesting\receipt;}PRULE：FOR{Obj item |item.物料（收货）：JAVA{！return（i）;=non-interesting\receipt;证明：或{non-interesting\receipt; interesting\receipt;}}见图7。 上下文证明我们在这里考虑的情况似乎更困难，因为有限性不能在一阶逻辑中捕获。我们的目标是在模块化的方式中使用微积分，例如，在适当的类的上下文中开发证明。一个有用的上下文证明模式是：o.C（t） Class Ax（C）·π1A1......·πlocHo.C（t） Class Ax（C）·πnAn我们说o. C（t）是环境假设，公式A1，...，An是局部假设。后者是通过反复应用而获得的从环境假设和公理ClassAx（C）出发，导出了消去规则然后，为了在C的上下文中展开一个证明，人们只需要选择局部假设并证明最终结论H。我们正在研究一个模块化的演算，依赖于COOML类，这使我们能够contextualise证明，并实现证明作为程序范例在我们的Java实现，通过翻译证明到常规的Java方法。图7中的证明展示了一般的思想（语法是临时的）;特别地，它说明了在证明中使用（运行时可计算的）J