A HOL MECHANIZATION OF THE AXIOMATIC SEMANTICS OF A SIMPLE DISTRIBUTED-PROGRAMMING LANGUAGE

被引：0
|
作者：
HARRISON, WL
ARCHER, MM
LEVITT, KN
机构：
[1] UNIV ILLINOIS,DEPT COMP SCI,URBANA,IL 61801
[2] UNIV CALIF DAVIS,DEPT COMP SCI,DAVIS,CA 95616
来源：
IFIP TRANSACTIONS A-COMPUTER SCIENCE AND TECHNOLOGY | 1993年 / 20卷
关键词：
PROGRAM VERIFICATION; SPECIFYING; VERIFYING; AND REASONING ABOUT PROGRAMS;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
This paper presents the axiomatic semantics for a simple distributed language, and its mechanization in HOL. The constructs of this language include those basic to a very simple sequential programming language in addition to asynchronous send and synchronous receive statements. The language has the appearance of a system programming language that supports sequential execution extended with message passing, and would be a suitable basis for coding distributed operating systems and applications. Included in the mechanization are functions which generate the goals associated with the verification of sequences of simple statements in the language. In contrast to Gordon's work on the HOL mechanization of programming logics, the starting point for our work is an axiomatic (rather than denotational definition) of the language, in the style of Schlichting's definition of message passing.
引用
收藏
页码：347 / 356
页数：10
相关论文
共 50 条
  • [31] TOOLS FOR DISTRIBUTED-PROGRAMMING IN THE INCAS PROJECT
    BUHLER, P
    WYBRANIETZ, D
    [J]. MICROPROCESSING AND MICROPROGRAMMING, 1989, 27 (1-5): : 199 - 206
  • [32] DISTRIBUTED-PROGRAMMING WITH LOGIC TUPLE SPACES
    CIANCARINI, P
    [J]. NEW GENERATION COMPUTING, 1994, 12 (03) : 251 - 284
  • [33] A truly concurrent semantics for a simple parallel programming language
    Gastin, P
    Mislove, M
    [J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 1999, 1683 : 515 - 529
  • [34] PARALLEL AND DISTRIBUTED-PROGRAMMING WITH PARMOD-C
    WEININGER, A
    SCHNEKENBURGER, T
    FRIEDRICH, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 591 : 115 - 126
  • [35] AN INTEGRATED FRAMEWORK FOR THE DESIGN OF DISTRIBUTED-PROGRAMMING ENVIRONMENTS
    FERNANDEZ, MAR
    SERRANO, GL
    DIAZ, MVE
    [J]. MICROPROCESSING AND MICROPROGRAMMING, 1991, 32 (1-5): : 401 - 409
  • [36] An axiomatic semantics for the synchronous language Gentzen
    Tini, S
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2003, 66 (02) : 316 - 348
  • [37] A semantics comparison workbench for a concurrent, asynchronous, distributed programming language
    Corrodi, Claudio
    Heussner, Alexander
    Poskitt, Christopher M.
    [J]. FORMAL ASPECTS OF COMPUTING, 2018, 30 (01) : 163 - 192
  • [38] DEFINITION AND IMPLEMENTATION OF A FLEXIBLE COMMUNICATION PRIMITIVE FOR DISTRIBUTED-PROGRAMMING
    MOSTEFAOUI, A
    RAYNAL, M
    [J]. APPLICATIONS IN PARALLEL AND DISTRIBUTED COMPUTING, 1994, 44 : 115 - 124
  • [39] Programming language semantics
    Schmidt, DA
    [J]. ACM COMPUTING SURVEYS, 1996, 28 (01) : 265 - 267
  • [40] DISTRIBUTED ACTIVE OBJECTS - A METHODOLOGICAL PROPOSAL AND TOOL FOR DISTRIBUTED-PROGRAMMING WITH TRANSPUTER SYSTEMS
    CAPEL, M
    TROYA, JM
    PALMA, A
    [J]. MICROPROCESSING AND MICROPROGRAMMING, 1993, 38 (1-5): : 197 - 204
12345