基于前后断言的多线程形式功能规格说明语言  

A Multi-Thread Formal Functional Specification Language Based on PreAssertion and PostAssertion

作　　者：李彤[1] 沈勤祖[1] 王庆革 

机构地区：[1]云南大学计算机科学系

出　　处：《云南大学学报（自然科学版）》1997年第6期544-549,共6页Journal of Yunnan University(Natural Sciences Edition)

基　　金：云南省应用基础研究基金;云南大学青年基金

摘　　要：探索用基于公理语义的前后断言方法来刻划多线程程序的功能，设计了一个功能规格说明语言ＪＡＶＡＳＰＥＣ，用来形式地表达程序的功能规格说明。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.

关 键 词：JAVA语言 断言 线程 规格说明 多线程 

分 类 号：TP319[自动化与计算机技术—计算机软件与理论]