An observationally complete program logic for imperative higher-order functions

被引：0
|
作者：
Honda, Kohei [1 ]
Yoshida, Nobuko [2 ]
Berger, Martin [3 ]
机构：
[1] Univ London, Dept Comp Sci, London WC1E 7HU, England
[2] Univ London Imperial Coll Sci Technol & Med, Dept Comp, London SW7 2AZ, England
[3] Univ Sussex, Dept Informat, Brighton BN1 9RH, E Sussex, England
来源：
THEORETICAL COMPUTER SCIENCE | 2014年 / 517卷
基金：
英国工程与自然科学研究理事会;
关键词：
Completeness Characteristic formulae; Program logic; Higher-order function; Imperative programming; Observational equivalence; FULL ABSTRACTION; HOARE-LOGIC; SEMANTICAL ANALYSIS; ALGOL; 60; VERIFICATION; SOUNDNESS; LANGUAGE; SYSTEM; PCF;
D O I：
10.1016/j.tcs.2013.11.003
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We establish a strong completeness property called observational completeness of the program logic for imperative, higher-order functions introduced in [1]. Observational completeness states that valid assertions characterise program behaviour up to observational congruence, giving a precise correspondence between operational and axiomatic semantics. The proof layout for the observational completeness which uses a restricted syntactic structure called finite canonical forms originally introduced in game-based semantics, and characteristic formulae originally introduced in the process calculi, is generally applicable for a precise axiomatic characterisation of more complex program behaviour, such as aliasing and local state. (C) 2013 Elsevier B.V. All rights reserved.
引用
收藏
页码：75 / 101
页数：27
相关论文
共 50 条
  • [1] An observationally complete program logic for imperative higher-order functions
    Honda, K
    Yoshida, N
    Berger, M
    [J]. LICS 2005: 20th Annual IEEE Symposium on Logic in Computer Science - Proceedings, 2005, : 270 - 279
  • [2] A logical analysis of aliasing in imperative higher-order functions
    Berger, Martin
    Honda, Kohei
    Yoshida, Nobuko
    [J]. JOURNAL OF FUNCTIONAL PROGRAMMING, 2007, 17 : 473 - 546
  • [3] A logical analysis of aliasing in imperative higher-order functions
    Berger, M
    Honda, K
    Yoshida, N
    [J]. ACM SIGPLAN NOTICES, 2005, 40 (09) : 280 - 293
  • [4] Logic program synthesis in a higher-order setting
    Lacey, D
    Richardson, J
    Smaill, A
    [J]. COMPUTATIONAL LOGIC - CL 2000, 2000, 1861 : 87 - 100
  • [5] Partial recursive functions in Higher-Order Logic
    Krauss, Alexander
    [J]. AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 589 - 603
  • [6] Program abstraction in a higher-order logic framework
    Benini, M
    Kalvala, S
    Nowotka, D
    [J]. THEOREM PROVING IN HIGHER ORDER LOGICS, 1998, 1479 : 33 - 48
  • [7] USE OF HIGHER-ORDER LOGIC IN PROGRAM VERIFICATION
    ERNST, GW
    HOOKWAY, RJ
    [J]. IEEE TRANSACTIONS ON COMPUTERS, 1976, 25 (08) : 844 - 851
  • [8] Implementing a program logic of objects in a higher-order logic theorem prover
    Hofmann, M
    Tang, F
    [J]. THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 268 - 282
  • [9] ON HIGHER-ORDER LOGIC
    KOGALOVS.SR
    [J]. DOKLADY AKADEMII NAUK SSSR, 1966, 171 (06): : 1272 - &
  • [10] Sound and Complete Concolic Testing for Higher-order Functions
    You, Shu-Hung
    Findler, Robert Bruce
    Dimoulas, Christos
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2021, 2021, 12648 : 635 - 663
12345