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 条
12345