WEAKEST PRECONDITION SEMANTICS FOR TIME AND CONCURRENCY

被引：3
作者：
SCHOLEFIELD, D
ZEDAN, HSM
机构：
[1] Formal Systems Research Group, Department of Computer Science, University of York, Heslington, York
来源：
INFORMATION PROCESSING LETTERS | 1992年 / 43卷 / 06期
关键词：
FORMAL SEMANTICS; WEAKEST PRECONDITIONS; REAL-TIME SYSTEMS; CONCURRENCY;
D O I：
10.1016/0020-0190(92)90116-D
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
A weakest precondition semantics for a real-time concurrent language is defined. An example in verification is presented, and the use of predicate transformers as the basis of a refinement calculus is also discussed.
引用
收藏
页码：301 / 308
页数：8
相关论文
共 10 条
[1]  
BACK RJR, 1989, REX WORKSHOP REFINEM
[2]  
Dijkstra EW, 1976, DISCIPLINE PROGRAMMI
[3]   AN AXIOMATIC BASIS FOR COMPUTER PROGRAMMING [J].
HOARE, CAR .
COMMUNICATIONS OF THE ACM, 1969, 12 (10) :576-&
[4]  
MARZULLO K, 1991, F REAL TIME COMPUTIN
[5]  
MORGAN C, 1988, RPG70
[6]  
Morgan C., 1990, PROGRAMMING SPECIFIC
[7]   A THEORETICAL BASIS FOR STEPWISE REFINEMENT AND THE PROGRAMMING CALCULUS [J].
MORRIS, JM .
SCIENCE OF COMPUTER PROGRAMMING, 1987, 9 (03) :287-306
[8]  
SCHOLEFIELD D, 1992, LECTURE NOTES COMPUT, V571
[9]  
SCHOLEFIELD D, IN PRESS REFINEMENT
[10]  
SCHOLEFIELD D, 1992, TAM EUROMICRO 92
1