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 条
  • [41] Non-uniform dependence on periodic initial data for the two-component Fornberg-Whitham system in Besov spaces
    Dutta, Prerona
    Keyfitz, Barbara Lee
    AIMS MATHEMATICS, 2024, 9 (09): : 25284 - 25296
  • [42] A simple two-component reaction-diffusion system showing rich dynamic behavior: spatially homogeneous aspects and selected bifurcation scenarios
    Hayase, Y
    Descalzi, O
    Brand, HR
    PHYSICA A-STATISTICAL MECHANICS AND ITS APPLICATIONS, 2005, 356 (01) : 19 - 24
  • [43] Development and Validation of a High-Throughput Cell-Based Screen To Identify Activators of a Bacterial Two-Component Signal Transduction System
    van Rensburg, Julia J.
    Fortney, Kate R.
    Chen, Lan
    Krieger, Andrew J.
    Lima, Bruno P.
    Wolfe, Alan J.
    Katz, Barry P.
    Zhang, Zhong-yin
    Spinola, Stanley M.
    ANTIMICROBIAL AGENTS AND CHEMOTHERAPY, 2015, 59 (07) : 3789 - 3799
  • [44] A Simple Transform to Linearize and Resolve Two-Component Decay Data: Illustration of Its Use and Efficacy in Assaying 33P/32P Mixtures by Liquid Scintillation Counting
    Colle, R.
    Radioactivity & Radiochemistry, 8 (02):
12345