时间并发约束程序设计框架及其扩展——tccp建模及功能特性的案例研究

理论计算机科学电子笔记188（2007）143-155www.elsevier.com/locate/entcs带外部函数的时间并发约束程序设计框架1M. 在第一条，第二 条。Gramlichb，3A. Villanuevaa，4aDSIC，西班牙维也纳科技奥地利维也纳摘要介绍了用于反应式系统建模的时间并发约束编程语言（tccp）。 这种语言允许一个模型在一个非常直观的方式，这些系统的典型成分，如超时，抢占等，但是，没有自然的方式来建模其他理想的功能，如功能计算，例如计算算术结果。事实上，尽管实现这种操作是可能的，但是在tccp中，计算的每一步都需要时间，并且避免干扰（反应）系统的预期整体行为是非常复杂的。在本文中，我们提出了一个扩展的tccp建模瞬时计算，提高了语言的表达能力，在这个意义上说，操作是繁琐的实现纯tccp，执行一个高效的，外部功能引擎，而tccp程序员可以专注于在系统的纯的，通常是更复杂的反应部分。我们还描述了一个激励工作的案例研究，并从验证的角度讨论了这里提出的新功能如何也可以用作开发人员的新工具。关键词：时间并发约束语言，功能特性，案例研究1引言时间并发约束程序设计（Timed Concurrent Constraint Programming，简称tccp）是由F. de Boer等人在[3]中对反应系统进行建模，即，持续与用户交互（并且通常不终止）的并发系统tccp被定义为ccp模型的扩展，1这项工作得到了欧盟（FEDER）和西班牙教育和文化部（赠款TIN 2004 - 7943-C 04和HA 2006 -0007）、“欧盟-印度跨文化传播信息和通信技术项目（赠款ALA/95/23/2003/077- 054）”以及巴伦西亚政府（赠款GV06/285）的部分支助2电子邮件地址：alpuente@dsic.upv.es3电子邮件地址：gramlich@logic.at4电子邮件地址：villanue@dsic.upv.es1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.043144M. Alpuente等人/理论计算机科学电子笔记188（2007）143Saraswat在[12]中，它被理想地认为是一个简单但强大的并发模型。tccp语言对原始ccp模型进行了两个主要修改。一方面，在tccp的语义中包含了一个隐含的（离散）时间概念。另一方面，引入了一个新的条件代理，它能够处理负面信息，可用于模型超时和抢占。在本文中，我们提出了一个扩展的tccp模型的瞬时功能，使我们能够简化和加快算术计算。虽然在tccp中实现算术函数是可能的，但是这样的函数的最终实现是非常不直观的。此外，这些计算消耗了大量的时间，从而使进程的同步例如，一个给定的进程可能需要另一个进程提交计算的一些数据，并且该计算可能需要一些时间，这取决于数据大小。因此，计算可能会减慢并最终扰乱系统的整体执行。我们在第3节中通过一个例子来说明这个问题。从验证的角度来看，这里介绍的新功能可以作为开发人员的新工具众所周知，验证并发系统是非常复杂的。在tccp的上下文中，进程之间的同步是手动编程的，执行不好的计算可能会导致同步错误，甚至掩盖其他通信异常，然后变得更加难以捉摸的捕捉。在这种情况下，对系统的反应和功能组件进行独立验证的可能性可能是非常有用的工具。用函数式语言编写的外部函数可以被看作是tccp函数实现的一种规范，程序员可以通过使用外部函数的版本来检查整个tccp使用外部函数的断言也可以引入tccp程序中，从而在程序执行期间自动验证它们是否满足。在第2节中，我们首先介绍tccp语言，然后在第3节中，我们通过一个例子来激励语言的拟议扩展我们还提供了新构造的语义。在第4节中，我们通过一个代表性的例子（一台计算机的模型）来说明所提出的扩展。我们将在第5节讨论如何使用这些新特性来检查tccp程序。最后，一些进一步的工作和我们的结论在第6节。2TCCP语言并发约束编程框架（concurrent constraint programming framework，ccp）被定义为一个简单但功能强大的并发系统模型。在过去的几十年里，该模型已经以不同的方式得到了扩展，tccp就是其中之一tccp是具有时间概念和捕获负面信息的机制的并发约束语言类似于ccp家族的其他语言，tccp是参数化的w.r.t.一个潜在的约束系统。这意味着，在每一个时刻，有前-M. Alpuente等人/理论计算机科学电子笔记188（2007）143145它是一个全局存储器，包含了到该特定时刻为止积累的信息。底层的约束系统决定了语言的原子命题和约束。下面我们回顾一下tccp的基本方面。 一个tccp程序P：：=D. A由一组声明D和一个代理A组成。一个声明D被定义为一组声明D.D或一个形式为D：：=p（x）：−A的子句，其中x是一个变量列表（可能为空），A是一个主体。最后，代理人被定义为：A：：= tell（c）|Σ0IntCopyright © 2018 - 2019 www.cnxt.com版权所有x1*2 + x2*1 + x3*0.5 + x4*0.2 + x5*0.1 + x6*0.05 + x7*0.02 + x8*0.01当总金额大于产品价格时，我们开始供应产品并（如有必要）返回找零的过程，这取决于机器中每种硬币的数量请注意，change也是一个外部函数，它表示机器必须返回给用户的硬币数量下面的代码摘录显示了change函数的实现，其中Price表示所选产品的成本，C硬币的数量在机器的情况下，并输入硬币，有由用户介绍。辅助函数coinsFor计算机器将返还给用户的每种硬币change：：Int-> Coins-> Coins-> Coinschange Price Input Case = coinsFor（Price-（paid Input））CasecoinsFor：：Int -> Coins ->Coins coinsFor x（C c1 c2 c3 c4 c5c6）| x>= 2 &c1> 0 =加（C 1 0 0 0 0 0 0）coins对于（x-2）（C（c1-1）c2 c3 c4 c5 c6 c7 c8）| x>= 1 &c2> 0 =加（C 0 1 0 0 0 0 0）对于（x-1）（C c1（c2-1）c3 c4 c5 c6 c7 c8）[...]| x >= 0.01 &c8 > 0 =加（C 0 0 0 0 0 0 1）152M. Alpuente等人/理论计算机科学电子笔记188（2007）143coinsFor（x-0.01）（C c1 c2 c3 c4 c5 c6 c7（c8-1））| 否则=（C-1 - 1 - 1 - 1 - 1 - 1 - 1）plus：： 硬币->硬币->硬币加上（C x1 x2 x3 x4 x5 x6 x7 x8）（C y1 y2 y3 y4 y5 y6 y7 y8）=C（x1+y1）（x2+y2）（x3+y3）（x4+y4）（x5+y5）（x6+y6）（x7+y7）（x8+y8）过程giveChange将硬币返回给用户，同时也更新了机箱。只要有可能，这些硬币最终会被并行返回注意，该过程使用通过上述函数变化计算的结果。如果没有足够的硬币来返回所需的零钱，则零钱函数返回值（C-1- 1 - 1 - 1 - 1 - 1 - 1）。通过这种方式，这种情况可以通过简单地在coffeeMachine进程中引入关于返回值Chng的检查来检测然而，为了简单起见，我们没有在当前版本的代码中实现这种检查。giveChange（Order，Change，Case，D1，D2，D3，D4，D5，D6，D7，D8，X1，X2，X3，X4，X5，X6，X7，X8，C1，C2，C3，C4，C5，C6，C7，C8（tell（Change = c（D1，D2，D3，D4，D5，D6，D7，D8））||tell（Case=[c（X1，X2，X3，X4，X5，X6，X7，X8）|案件']）||问（真）→（告诉（C1是X1-D1））||tell（C2是X2-D2）||【......】tell（C8是X8-D8）||tell（Order=[no|]中）||tell（空闲=[空闲|]））。最后，系统过程验证机器和用户声明。最初，硬币机有两个硬币的每一类。system（Case，Output）：-Free，Order，Cash，Cash'，Case'（tell（Free=[idle|]中）||tell（Order=[no|]中）||tell（Cash = [c（0，0，0，0，0，0，0）|Cash ']）||用户（免费，订单，现金，现金'）||Case=[c（2，2，2，2，2，2，2，2）|案件']）||coffeeMachine（Free，Ord er，C ash，Cas e，Ca se '，Out put））.5分析和运行时验证在本节中，我们将说明如何在tccp中使用瞬时函数来验证系统的某些（静态和动态）属性让我们列举一些用户可能感兴趣的属性，以检查在模型的计算机：(i) 如果发起订单并且已经引入足够的资金，则最终正确地完成订单（即，提供产品、正确退回找零、始终更新Case并重置机器状态）;否则，机器M. Alpuente等人/理论计算机科学电子笔记188（2007）143153退回钱。154M. Alpuente等人/理论计算机科学电子笔记188（2007）143(ii) 如果用户没有为所选产品引入足够的钱，则不执行任何动作，除非按下取消按钮。在这种情况下，插入的硬币将返回给用户。让我们（部分地）指定上面的前一个属性。也就是说，在订单完成后正确更新案例。我们必须检查机箱的新价值是否与机箱+现金-找零的金额一致。为了验证此属性，我们引入了一个新的外部函数检查，执行所需的计算。检查：：Coins -> Coins-> Coins-> Bool检查（C x1 x2 x3 x4 x5 x6 x7 x8）（C y1 y2 y3 y4 y5 y6 y7 y8）（C z1 z2z3 z4 z5 z6 z7 z8）（C w1 w2 w3 w4 w5 w6 w7 w8）=y1+w1-x1 == z1 y2+w2-x2 == z2 y3+w3-x3 == z3 y4+w4-x4 == z4y5+w5-x5 == z5 y6+w6-x6 == z6 y7+w7-x7 == z7 y8+w8-x8 == z8假设函数调用检查（Change，C，coffeeMachine（.）：-[...]询问（订单=[取消|]）→giveChange（Order，Input，Case，Case'））||check2（Change '，Case'，Case '，Cash'）||coffeeMachine（Free'，Free''，Order'，Order''，Cash'，Case'，Case’’,Change’,[...]支票2（找零、箱子、B（B ←check（Change，Case，Case '，Cash）||ask（true）→now（B=0）then stop elseskip.程序中的这些函数调用可以被看作是在代码中引入in-variant或断言的一种手段。这种不变量在系统执行期间被检查，并且在断言之一未被满足的情况下执行被中断。显然，不变量不应该破坏原始系统的行为，程序员必须负责同步。也可以在程序目标级别对此类检查进行编程，方法是使用共享变量来同步主进程与专用监视器。coffeeMachine（Free，Free '，Order，Order'，Cash，Case，Case '，Change，Output）||check2（零钱，箱子，箱子'，现金）关于动态特性，我们可以将我们的方法与[4，1]中定义的约束时态逻辑结合起来，我们如下所示。再次考虑上面的性质（i）一方面，我们必须检查，当咖啡订单给机器时，后者最终产生咖啡输出或moreMoney输出。在约束时态逻辑中，M. Alpuente等人/理论计算机科学电子笔记188（2007）143155可以写成：Q（订单=咖啡→Q（产出=咖啡产出=更多钱））更具体地说，当订单咖啡给机器，并提供了足够的钱已经引入，然后机器必须生产咖啡和返回的变化。这可以具体说明如下：Q（订单=咖啡→收到的钱→（Q（产出=咖啡changereturned）其中接收的货币和返回的找零是对应于布尔属性的原子谓词，该布尔属性必须由程序在适当的时刻更新直观地说，每次系统检测到引入的金额足以为所选产品提供服务时，都应该更新收到的资金我们还可以检查机器的状态是否在工作，只要收到的钱是真的第二个考虑的属性检查用户没有引入足够的钱的情况在这种情况下，如果给出取消订单，则机器应该退还用户直到该时刻引入的全部金额这个额外的新动态属性可以定义如下：Q（订单=收到的咖啡钱）→（1）（1）（2）（3）（（订单=取消订单（退回更改））收到的款项）其中返回的改变是对应于适当的布尔属性的另一个原子谓词。U运算符表示时态逻辑的经典直到运算符，也为[4]的逻辑定义。我们目前正在通过将其与Curry中更强大的外部约束求解器连接来改进我们的实现。作为进一步的工作，我们还计划开发一种方法，通过调整[6]中开发的模型检查器来验证具有外部函数的tccp6结论在定时并发系统中，数据在进程之间共享，并且一个进程可能等待另一个进程结束，需要有效的同步策略作为一个支持进程时间相关并行性的系统，tccp属于这一类，函数计算（特别是算术计算）实际上是进程同步的瓶颈。由于tccp不支持顺序计算，因此执行简单的算术计算可能会浪费大量时间，并且会暂停所有需要此计算结果的其他进程的进程为了克服这些缺点，我们开发了一个功能引擎，可以插入到tccp系统。这大大优化了系统的性能，156M. Alpuente等人/理论计算机科学电子笔记188（2007）143对tccp的可用性更高。本文中的案例研究表明了在tccp中结合这些方面的有用性，特别是在实际领域中，可以方便地将算术计算与解决问题策略的其他部分区分开来。引用[1] M. Alpuente，M.M. Gallardo，E. Pimentel和A.维拉纽瓦 TCCP验证的实时逻辑。J. of Universal Computer Science，to appear，2006.[2] M.阿尔蓬特湾Gramlich，和A.维拉纽瓦带外部函数的时间并发约束编程。技术报告DSIC-II/13/06，DSIC，技术巴伦西亚大学，2006年12月。http://www.dsic.upv.es/www.example.com[3] F. S. de Boer，M. Gabbrielli和M. C. Meo.一种时间并发约束语言。 信息与计算，161：45[4] F. S. de Boer，M. Gabbrielli和M. C. Meo.时间并发约束程序推理的时态逻辑。In G. Smolka，编辑，Proceedings of 8 th International Symposium on Temporal Representation and Reasoning，第227IEEEComputer Society Press，2001.[5] S. Bonnier和J. Maluszynski。逻辑程序与外部过程的干净融合。在Proceedings of the 5th Conferenceon Logic Programming第五届逻辑编程研讨会论文集，第311-326页麻省理工学院出版社，1988年。[6] M. Falaschi和A.维拉纽瓦 时间并发约束程序的自动验证。理论与实践的逻辑。出现，2006年。[7] M. Hanus （ ed. ） .Curry ： An Integrated Functional Logic Language （ Curry ： AnIntegratedFunctional0.8.2），2006年3月可在http://www.informatik.uni-kiel.de/上查阅。[8] M.赫梅尼吉尔多CIAO设计中的若干方法论问题--一个通用、并行、并发约束系统.在Proceedings of theInternational Conference on Principles and Practice of Constraint Programming，LNCS第874卷，第123-133页。Springer-Verlag，1994.[9] A.赫兰兹和J·J·莫雷诺·纳瓦罗SLAM-SL教程。技术报告，Babel Group，计算机科学学院，马德里技术大学，2001年。基于A.赫兰兹论文[10] 下午 希尔和J。W. LL OYD。 TheeGüodelProg rramminggLang ua ge. MITPre ss，1994年。 ISBN0-262-08229-2。[11]F. 洛佩兹-弗洛拉瓜和J。 他是我的儿子。 TOY：AMultiparadigmDeclarativ e System.在中国。的Int'l Conference on Rewriting Techniques and Applications，LNCS的第1631卷，第244-247页。Springer-Verlag，1999.[12] V. A.萨拉斯瓦特并发约束编程语言。麻省理工学院出版社，马萨诸塞州剑桥，1993年。[13] Z. Somogyi，F. Henderson和T.康威Mercury是一种高效的纯声明逻辑程序设计语言。Journal of LogicProgramming，29：17[14] F.瓦伦西亚无限状态定时CCP 过程和一阶LTL 的可判定性。Theoretical Computer Science，330（3）：577[15] 范罗伊，布兰德，D. Duchier，S. Haridi，M. Henz和C. 舒尔特 多范式编程中的逻辑编程：奥兹经验。逻辑程序设计的理论与实践，3（6）：715