COMPOSITIONAL CHARACTERIZATION OF OBSERVABLE PROGRAM PROPERTIES

被引:1
|
作者
STEFFEN, B
JAY, CB
MENDLER, M
机构
[1] UNIV EDINBURGH,LFCS,EDINBURGH EH8 9YL,MIDLOTHIAN,SCOTLAND
[2] UNIV ERLANGEN NURNBERG,INST COMP AIDED CIRCUIT DESIGN,W-8520 ERLANGEN,GERMANY
关键词
D O I
10.1051/ita/1992260504031
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
In this paper we model both program behaviours and abstractions between them as lax functors, which generalize abstract interpretations by exploiting the natural ordering of program properties. This generalization provides a framework in which correctness (safety) and completeness of abstract interpretations naturally arise from this order. Furthermore, it supports modular and stepwise refinement: given a program behaviour, its characterization, which is a "best" correct and complete denotational semantics for it, can be determined in a compositional way.
引用
收藏
页码:403 / 424
页数:22
相关论文
共 50 条
  • [1] Compositional Control Synthesis for Partially Observable Systems
    Kuijper, Wouter
    van de Pol, Jaco
    CONCUR 2009 - CONCURRENCY THEORY, PROCEEDINGS, 2009, 5710 : 431 - 447
  • [3] Compositional heterogeneity in multiphase steels: Characterization and influence on local properties
    Chang, Yuling
    Haase, Christian
    Szeliga, Danuta
    Madej, Lukasz
    Hangen, Ude
    Pietrzyk, Maciej
    Bleck, Wolfgang
    MATERIALS SCIENCE AND ENGINEERING A-STRUCTURAL MATERIALS PROPERTIES MICROSTRUCTURE AND PROCESSING, 2021, 827
  • [4] Program Models for Compositional Verification
    Huisman, Marieke
    Aktug, Irem
    Gurov, Dilian
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2008, 5256 : 147 - +
  • [5] Game characterization of logic program properties
    Int J Pressure Vessels Piping, 2 (99):
  • [6] OBSERVABLE PROPERTIES OF OBLATE SPHEROIDS
    FILLMORE, JA
    ASTRONOMICAL JOURNAL, 1986, 91 (05): : 1096 - 1107
  • [7] Growth and properties characterization of compositional graded barium strontium titanate films
    Zhao, Xu
    Hu, Zuoqi
    Li, Yuanyuan
    Xie, Zijian
    Wang, Yuhui
    Zhenkong Kexue yu Jishu Xuebao/Journal of Vacuum Science and Technology, 2012, 32 (11): : 955 - 960
  • [8] An observable for vacancy characterization and diffusion in crystals
    Geslin, Pierre-Antoine
    Ciccotti, Giovanni
    Meloni, Simone
    JOURNAL OF CHEMICAL PHYSICS, 2013, 138 (14):
  • [9] A Compositional Method for Deciding Program Termination
    Dimovski, Aleksandar
    ICT INNOVATIONS 2010, 2011, 83 : 71 - 80
  • [10] Recursive Games for Compositional Program Synthesis
    Beyene, Tewodros A.
    Chaudhuri, Swarat
    Popeea, Corneliu
    Rybalchenko, Andrey
    VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, 2016, 9593 : 19 - 39