Formal validation of data-parallel programs: a two-component assertional proof system for a simple language

被引：4
|
作者：
Bouge, L
Cachera, D
LeGuyadec, Y
Utard, G
Virot, B
机构：
[1] UNIV ORLEANS,LIFO,F-45067 ORLEANS 2,FRANCE
[2] VALORIA,VANNES,FRANCE
来源：
THEORETICAL COMPUTER SCIENCE | 1997年 / 189卷 / 1-2期
关键词：
D O I：
10.1016/S0304-3975(97)00041-8
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a proof system for a simple data-parallel kernel language called L. This proof system is based on a two-component assertion language. We define a weakest preconditions calculus and analyze its definability properties. This calculus is used to prove the completeness of the proof system. We also present a two-phase proof methodology, yielding proofs similar to those for scalar languages. We finally discuss other approaches.
引用
收藏
页码：71 / 107
页数：37
相关论文
共 44 条
  • [31] Integrating inventory planning, pricing and maintenance for perishable products in a two-component parallel manufacturing system with common cause failures
    Ali Salmasnia
    Ali Talesh-Kazemi
    Operational Research, 2022, 22 : 1235 - 1265
  • [32] Application of PARAFAC to a two-component system exhibiting Fluorescence Resonance Energy Transfer: from theoretical prediction to experimental validation
    Chen, Hao
    Kenny, Jonathan E.
    ANALYST, 2012, 137 (01) : 153 - 162
  • [33] Simple practical processing of a large single crystal from a large amount of a complete stoichiometric mixture in two-component system
    Ito, K
    Sato, H
    Kanazawa, H
    Tamada, O
    Kitazawa, T
    Koike, M
    Takei, H
    JOURNAL OF CRYSTAL GROWTH, 2004, 271 (3-4) : 398 - 402
  • [34] Continuity properties of the data-to-solution map for the two-component higher order Camassa-Holm system
    Wang, Feng
    Li, Fengquan
    NONLINEAR ANALYSIS-REAL WORLD APPLICATIONS, 2019, 45 : 866 - 876
  • [35] Non-uniform dependence of the data-to-solution map for the two-component Fornberg-Whitham system
    Yu, Yanghai
    Li, Jinlu
    ANNALI DI MATEMATICA PURA ED APPLICATA, 2023, 202 (01) : 59 - 76
  • [36] Non-uniform dependence on initial data of a modified periodic two-component Camassa-Holm system
    Lv, Guangying
    Wang, Xiaohuan
    ZAMM-Zeitschrift fur Angewandte Mathematik und Mechanik, 2015, 95 (05): : 444 - 456
  • [37] Non-uniform continuity on initial data for the two-component b-family system in Besov space
    Wu, Xing
    Li, Cui
    Cao, Jie
    MONATSHEFTE FUR MATHEMATIK, 2023, 201 (02): : 547 - 563
  • [38] Non-uniform continuity on initial data for the two-component b-family system in Besov space
    Xing Wu
    Cui Li
    Jie Cao
    Monatshefte für Mathematik, 2023, 201 : 547 - 563
  • [39] On Initial Data Problem for a Periodic Two-Component b-Family System (vol 29, pg 171, 2022)
    Wang, Xiaohuan
    JOURNAL OF NONLINEAR MATHEMATICAL PHYSICS, 2022, 29 (03) : 658 - 658
  • [40] A robust bathtub-shaped failure time model for a two-component system with applications to complete and censored reliability data
    Abba, Badamasi
    Wang, Hong
    Muhammad, Mustapha
    Bakouch, Hassan S.
    QUALITY TECHNOLOGY AND QUANTITATIVE MANAGEMENT, 2024, 21 (03): : 309 - 339
12345