An axiomatic approach to structuring specifications

被引:9
作者
Diaconescu, Razvan [1 ]
机构
[1] Romanian Acad, Simion Stoilow Inst Math, Bucharest, Romania
关键词
Algebraic specification; Structured specification; Institutions; INTERPOLATION; PROOF;
D O I
10.1016/j.tcs.2012.03.001
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
In this paper we develop an axiomatic approach to structured specifications in which both the underlying logical system and corresponding institution of the structured specifications are treated as abstract institutions, which means two levels of institution independence. This abstract axiomatic approach provides a uniform framework for the study of structured specifications independently from any actual choice of specification building operators, and moreover it unifies the theory and the model oriented approaches. Within this framework we develop concepts and results about 'abstract structured specifications' such as co-limits, model amalgamation, compactness, interpolation, sound and complete proof theory, and pushout-style parameterization with sharing, all of them in a top down manner dictated by the upper level of institution independence. (C) 2012 Elsevier B.V. All rights reserved.
引用
收藏
页码:20 / 42
页数:23
相关论文
共 50 条
  • [31] Automating invariant verification of behavioral specifications
    Nakano, Masahiro
    Ogata, Kazuhiro
    Nakamura, Masaki
    Futatsugi, Kokichi
    QSIC 2006: SIXTH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE, PROCEEDINGS, 2006, : 49 - +
  • [32] Formal specifications and test: Correctness and oracle
    LeGall, P
    Arnould, A
    RECENT TRENDS IN DATA TYPE SPECIFICATION, 1996, 1130 : 342 - 358
  • [33] Heterogeneous Logical Environments for Distributed Specifications
    Mossakowski, Till
    Tarlecki, Andrzej
    RECENT TRENDS IN ALGEBRAIC DEVELOPMENT TECHNIQUES, 2009, 5486 : 266 - +
  • [34] Exhaustive test sets for algebraic specifications
    Aiguier, Marc
    Arnould, Agnes
    Le Gall, Pascale
    Longuet, Delphine
    SOFTWARE TESTING VERIFICATION & RELIABILITY, 2016, 26 (04) : 294 - 317
  • [35] A TRANSLATION METHOD FROM NATURAL-LANGUAGE SPECIFICATIONS OF COMMUNICATION PROTOCOLS INTO ALGEBRAIC SPECIFICATIONS USING CONTEXTUAL DEPENDENCIES
    ISHIHARA, Y
    SEKI, H
    KASAMI, T
    SHIMABUKURO, J
    OKAWA, K
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 1993, E76D (12) : 1479 - 1489
  • [36] Structuring water rights in China: a hierarchical framework
    Wang, Yahua
    Wan, Tingting
    Biswas, Asit K.
    INTERNATIONAL JOURNAL OF WATER RESOURCES DEVELOPMENT, 2018, 34 (03) : 418 - 433
  • [37] Property-oriented semantics of structured specifications
    Sannella, Donald
    Tarlecki, Andrzej
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2014, 24 (02)
  • [38] Generating Model Checkers from Algebraic Specifications
    Teodor Rus
    Eric Van Wyk
    Tom Halverson
    Formal Methods in System Design, 2002, 20 : 249 - 284
  • [39] Feasibility of H∞ design specifications:: an interpolation method
    Ferreres, G
    Puyou, G
    ACC: PROCEEDINGS OF THE 2005 AMERICAN CONTROL CONFERENCE, VOLS 1-7, 2005, : 4309 - 4314
  • [40] Creme: An automatic invariant prover of behavioral specifications
    Nakano, Masahiro
    Ogata, Kazuhiro
    Nakamura, Masaki
    Futatsugi, Kokichi
    INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 2007, 17 (06) : 783 - 804