规约本身可能错

验证只保证"程序符合规约"。规约写错了，验证通过的程序照样是错的。