• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Asia-Pacific Software Engineering Conference >Writing Concurrent Java Programs Based on CafeOBJ Specifications
【24h】

Writing Concurrent Java Programs Based on CafeOBJ Specifications

机译：根据CafeOBJ规范编写并发Java程序

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

CafeOBJ is an advanced algebraic specification language that can be used for writing formal specifications of various software systems and verifying properties of them. It implements equational logic by rewriting and can be used as a powerful interactive theorem proving system. Specifiers can write proof scores also in CafeOBJ and conduct proofs by executing the proof scores. Despite its usefulness, up to present, the application of CafeOBJ specifications to software development is very limited. Therefore, we would like to propose methods or techniques to make an observation transition system (OTS) in CafeOBJ more usable in both software development and testing. We focus on concurrent systems and how to write concurrent programs in Java based on OTSs. Java has been chosen as the implementation language because concurrency is strongly supported in this language and there are also many powerful testing frameworks in Java that can help us further verify properties of the programs.
机译：CafeOBJ是一种高级的代数规范语言，可用于编写各种软件系统的正式规范并验证其性能。它通过重写实现方程逻辑，并且可以用作功能强大的交互式定理证明系统。指定者还可以在CafeOBJ中编写证明分数，并通过执行证明分数来进行证明。尽管有用，但到目前为止，CafeOBJ规范在软件开发中的应用非常有限。因此，我们希望提出一些方法或技术，以使CafeOBJ中的观察转换系统（OTS）在软件开发和测试中更有用。我们专注于并发系统以及如何基于OTS用Java编写并发程序。之所以选择Java作为实现语言，是因为该语言强烈支持并发，并且Java中还有许多强大的测试框架可以帮助我们进一步验证程序的属性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号