作者
Stephen A Cook
发表日期
1978/2
期刊
SIAM Journal on Computing
卷号
7
期号
1
页码范围
70-90
出版商
Society for Industrial and Applied Mathematics
简介
A simple ALGOL-like language is defined which includes conditional, while, and procedure call statements as well as blocks. A formal interpretive semantics and a Hoare style axiom system are given for the language. The axiom system is proved to be sound, and in a certain sense complete, relative to the interpretive semantics. The main new results are the completeness theorem, and a careful treatment of the procedure call rules for procedures with global variables in their declarations.
引用总数
学术搜索中的文章
SA Cook - SIAM Journal on Computing, 1978