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 条
  • [41] 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
  • [42] On Describing Terminating Algebraic Specifications Based on Their Models
    Nakamura, Masaki
    Ogata, Kazuhiro
    Futatsugi, Kokichi
    INTERNATIONAL MULTICONFERENCE OF ENGINEERS AND COMPUTER SCIENTISTS, IMECS 2012, VOL I, 2012, : 269 - 274
  • [43] BUILDING SPECIFICATIONS IN THE EVENT-B INSTITUTION
    Farrell, Marie
    Monahan, Rosemary
    Power, James F.
    LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 18 (04) : 4:1 - 4:55
  • [44] On pushout consistency, modularity and interpolation for logical specifications
    Veloso, PAS
    INFORMATION PROCESSING LETTERS, 1996, 60 (02) : 59 - 66
  • [45] A Relatively Complete Calculus for Structured Heterogeneous Specifications
    Mossakowski, Till
    Tarlecki, Andrzej
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 2014, 8412 : 441 - 456
  • [46] An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
    Hammond, Angus
    Liu, Zongyuan
    Perami, Thibaut
    Sewell, Peter
    Birkedal, Lars
    Pichon-Pharabod, Jean
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (POPL): : 604 - 637
  • [47] Development of communication protocols using algebraic and temporal specifications
    Jmaiel, M
    Pepper, P
    COMPUTER NETWORKS, 2003, 42 (06) : 737 - 764
  • [48] First-order specifications of programmable data types
    Mirkowska, Z
    Salwicki, A
    Srebrny, M
    Tarlecki, A
    SIAM JOURNAL ON COMPUTING, 2001, 30 (06) : 2084 - 2096
  • [49] Synthesizing Nested Relational Queries from Implicit Specifications
    Benedikt, Michael
    Pradic, Cecilia
    Wernhard, Christoph
    PROCEEDINGS OF THE 42ND ACM SIGMOD-SIGACT-SIGAI SYMPOSIUM ON PRINCIPLES OF DATABASE SYSTEMS, PODS 2023, 2023, : 33 - 45
  • [50] On oracles for interpreting test results against algebraic specifications
    Machado, PDL
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, 1999, 1548 : 502 - 518