首页    期刊浏览 2024年11月30日 星期六
登录注册

文章基本信息

  • 标题:Combining Algebraic and Set-Theoretic Specifications (Extended Version)
  • 本地全文:下载
  • 作者:Claus Hintermeier ; Hélene Kirchner ; Peter D. Mosses
  • 期刊名称:BRICS Report Series
  • 印刷版ISSN:0909-0878
  • 出版年度:1996
  • 卷号:3
  • 期号:52
  • 出版社:Aarhus University
  • 摘要:Specification frameworks such as B and Z provide power sets and cartesian products as built-in type constructors, and employ a rich notation for defining (among other things) abstract data types using formulae of predicate logic and lambda-notation. In contrast, the so-called algebraic specification frameworks often limit the type structure to sort constants and first-order functionalities, and restrict formulae to (conditional) equations. Here, we propose an intermediate framework where algebraic specifications are enriched with a set-theoretic type structure, but formulae remain in the logic of equational Horn clauses. This combines an expressive yet modest specification notation with simple semantics and tractable proof theory.
国家哲学社会科学文献中心版权所有