Formalizing the Institution for Event-B in the Coq Proof Assistant

被引：3

作者：

Reynolds, Conor ^{[1
]}

机构：

[1] Maynooth Univ, Maynooth, Kildare, Ireland

来源：

RIGOROUS STATE-BASED METHODS, ABZ 2021 | 2021年 / 12709卷

关键词：

Coq; Event-B; Institution theory; UNIVERSAL ALGEBRA;

D O I：

10.1007/978-3-030-77543-8_17

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We formalize a fragment of the theory of institutions sufficient to establish basic facts about the institution EVT for Event-B, and its relationship with the institution FOPEQ for first-order predicate logic. We prove the satisfaction condition for EVT and encode the institution comorphism FOPEQ -> EVT embedding FOPEQ in EVT.

引用

页码：162 / 166

页数：5

共 8 条

[1] Abrial J.-R., 2010, Modeling in Event-B: System and Software Engineering
[2] Capretta V, 1999, LECT NOTES COMPUT SC, V1690, P131
[3] Farrell Marie, 2017, Recent Trends in Algebraic Development Techniques. 23rd IFIP WG 1.3 International Workshop, WADT 2016. Revised Selected Papers. LNCS 10644, P104, DOI 10.1007/978-3-319-72044-9_8
[4] INSTITUTIONS - ABSTRACT MODEL-THEORY FOR SPECIFICATION AND PROGRAMMING
GOGUEN, JA
BURSTALL, RM
[J]. JOURNAL OF THE ACM, 1992, 39 (01) : 95 - 146
[5] Formalization of Universal Algebra in Agda
Gunther, Emmanuel
Gadea, Alejandro
Pagano, Miguel
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2018, 338 : 147 - 166
[6] Mossakowski T., 2007, Logica Universalis, P111
[7] Mossakowski T, 2007, LECT NOTES COMPUT SC, V4424, P519
[8] Sannella D., 2012, Foundations of Algebraic Specification and Formal Software Development, DOI [10.1007/978-3-642-17336-3, DOI 10.1007/978-3-642-17336-3]

← 1 →