• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE International Symposium on Theoretical Aspects of Software Engineering >On the Theoretical Foundation of Meta-Modelling in Graphically Extended BNF and First Order Logic
【24h】

On the Theoretical Foundation of Meta-Modelling in Graphically Extended BNF and First Order Logic

机译：论图形扩展BNF和一阶逻辑中元建模的理论基础

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

摘要

Meta-modeling plays an important role in model driven software development methodology. In our previous work, a graphic extension of BNF (GEBNF) was proposed to define the abstract syntax of graphic modeling languages. From a GEBNF syntax definition, a first order predicate logic language can be induced so that meta-modeling can be performed formally by specifying a predicate on the domain of syntactically valid models. In this paper, we investigate the theoretical foundation of this meta-modeling approach. We first formally define the semantics of GEBNF syntax definitions as algebras that contain no junk and satisfy constraints derived from GEBNF syntax rules. The semantics of the induced logic is then formally defined by regarding such algebras as models. We then formally prove that well-formed syntax definitions together with syntax morphisms form a category, where syntax morphisms represent the translations between modeling languages. The models (i.e. algebras) in a modeling language and the homomorphisms between them also form a category. Finally, we prove that the functors from GEBNF syntax definitions to the categories of models and to sentences in the induced first order logic form an institution. Therefore, GEBNF and its induced logics form a valid formal specification language for models.
机译：元建模在模型驱动软件开发方法中起着重要作用。在我们以前的工作中，提出了BNF（GEBNF）的图形扩展，以定义图形建模语言的抽象语法。从GEBNF语法定义，一阶谓词逻辑语言可以被诱导，使元模型可以通过对语法有效的模型域指定谓词正式执行。在本文中，我们调查了该元建模方法的理论基础。我们首先将Gebnf语法定义的语义正式定义为包含从Gebnf语法规则导出的垃圾和满足约束的代数。然后通过将这种代数视为模型来正式定义诱导逻辑的语义。然后，我们正式证明，与语法态度一起形成了良好的语法定义，形成了一个类别，其中语法造理代表建模语言之间的翻译。在建模语言中的模型（即代数）和它们之间的同态也形成了一个类别。最后，我们证明了从Gebnf语法定义的函数到模型类别以及诱导的一阶逻辑中的句子形成一个机构。因此，GEBNF及其诱导逻辑为模型形成了有效的正式规范语言。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号