摘要: 程序正确性的验证是计算机科学的核心问题之一，也是当前软件工程最关心的问题.这个问题至今未有满意的解决办法.斯坦福大学计算机科学系的验证系统小组经过数年的研究，于1979年3月把他们研制的STANFORD PASCAL VERIFIER（以下简为SPV）公布于世，虽然他们自己说只是一种原型，但是却已能够进行一些并非不足道的工作，可说是迈了很成功的一步.笔者恰好在这个系统公布之际到该系驻足了一年多.这里愿把所见所闻笔录于此，供有关同志参考.