Introducing H, an Institution-Based Formal Specification and Verification Language

被引：0
作者：
Răzvan Diaconescu
机构：
[1] Simion Stoilow Institute of Mathematics of the Romanian Academy,
来源：
Logica Universalis | 2020年 / 14卷
关键词：
Institution theory; modal logic; formal specification; Primary 03C95; Secondary 03C98; 68N30;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
This is a short survey on the development of the formal specification and verification language H with emphasis on the scientific part. H is a modern highly expressive language solidly based upon advanced mathematical theories such as the internalisation of Kripke semantics within institution theory.
引用
收藏
页码：259 / 277
页数：18
相关论文
共 35 条
[1]  
Areces C(2001)Bringing them all together J. Log. Comput. 11 657-669
[2]  
Blackburn P(2002)CASL: the common algebraic specification language Theor. Comput. Sci. 286 153-196
[3]  
Delany SR(2000)Representation, reasoning, and relational structures: a hybrid logic manifesto Log. J. IGPL 8 339-365
[4]  
Astesiano E(1995)Hybrid languages J. Log. Lang. Inf. 4 251-272
[5]  
Bidoit M(2010)Quasi-boolean encodings and conditionals in algebraic specification J. Log. Algebr. Program. 79 174-188
[6]  
Kirchner H(2016)Quasi-varieties and initial semantics in hybridized institutions J. Log. Comput. 26 855-891
[7]  
Krieg-Brückner B(2017)Implicit Kripke semantics and ultraproducts in stratified institutions J. Log. Comput. 27 1577-1606
[8]  
Mosses P(2011)On the algebra of structured specifications Theor. Comput. Sci. 412 3145-3174
[9]  
Sannella D(2016)Encoding hybridized institutions into first order logic Math. Struct. Comput. Sci. 26 745-788
[10]  
Tarlecki A(2007)Ultraproducts and possible worlds semantics in institutions Theor. Comput. Sci. 379 210-230
1234