论文部分内容阅读
程序正确性的验证是计算机科学的核心问题之一,也是当前软件工程最关心的问题。这个问题至今未有满意的解决办法。 斯坦福大学计算机科学系的验证系统小组经过数年的研究,于1979年3月把他们研制的STANFORD PASCAL VERIFIER(以下简为SPV)公布于世,虽然他们自己说只是一种原型,但是却已能够进行一些并非不足道的工作,可说是迈了很成功的一步。 笔者恰好在这个系统公布之际到该系驻足了一年多。这里愿把所见所闻笔录于此,供有关同志参考。
The verification of program correctness is one of the core issues in computer science and is also the most concerned issue in current software engineering. So far there is no satisfactory solution to this problem. After years of research, Stanford’s Computer Systems Verification Systems team published the STANFORD PASCAL VERIFIER (SPV), which they developed in March 1979, although they themselves said that they are a prototype, but they have been able to To do something that is not insignificant can be a very successful step. The author stopped at the department just over a year ago when the system was released. Here is the record of what you see and hear recorded here, for the comrades for reference.