摘要
探索用基于公理语义的前后断言方法来刻划多线程程序的功能，设计了一个功能规格说明语言ＪＡＶＡＳＰＥＣ，用来形式地表达程序的功能规格说明。
A method which use pre-assertion and post-assertion based on axiomatic semantic to express the function of multi-thread programs is proposed and a funtional specification language JAVASPEC which can express formally functional specification of programs is designed.Thus,the basis supporting the automatic program generation are established.
出处
《云南大学学报（自然科学版）》
CAS
CSCD
1997年第6期544-549,共6页
Journal of Yunnan University(Natural Sciences Edition)
基金
云南省应用基础研究基金
云南大学青年基金
关键词
JAVA语言
断言
线程
规格说明
多线程
Java,axiomatic semantic,assertion,thread,formal,specification
