论文部分内容阅读
针对一个基于共享变量的带有进程创建的命令式语言，用变迁系统描述了它的结构操作语义，并用扩展的状态变迁迹模型定义了它的指称语义，在该模型下，状态变迁被区分为两种不同形式，分别表示发生在原进程和被创建进程中的状态变迁，这样便可以定义适当的语义复合运算，在对命令的指称进行复合时根据变迁类型的不同对变迁迹进行串行或交错连接，恰当地反映了进程的并发运行受创建命令在程序中的相对位置的限制，最后证明了这两个语义