二级形式语义与语义导引编译

本文给出了一种形式语义方法,它能使形式语义与编译一致。这种方法的基础是一时序逻辑语言,一方面它是一种逻辑系统,故其语义简明,便于形式化和有效地实现;另一方面它又是一种中间程序语言,其它高级语言的语义可以用严格形式转换的方法投射到它之上,这样形成的一种二级形式语义本身即构成一种编译转换。