Chinaunix首页 | 论坛 | 博客
  • 博客访问: 493302
  • 博文数量: 41
  • 博客积分: 4007
  • 博客等级: 中校
  • 技术积分: 725
  • 用 户 组: 普通用户
  • 注册时间: 2006-09-30 15:43
文章分类

全部博文(41)

文章存档

2011年(13)

2010年(14)

2009年(2)

2008年(12)

分类: LINUX

2011-02-03 12:30:22

发信人: lingcore (), 信区: CSArch
标  题: Re: 高性能CPU研发能够离开定理证明器吗
发信站: 水木社区 (Wed Feb  2 00:46:47 2011), 站内

形式验证可以分成两类。一类是全部依靠自动工具的,另一类是人机交互证明。我们讲的是第二类,并把它们称为定理证明器,以示同第一类的区别。

第一类工具不能出来大规模的验证问题,第二类不受问题规模的限制,因为它通过人机交互的方式进行证明。人可以把大问题分解成小问题,大定理的证明化解成一组小的引理的证明,可以使用归纳法。可以开发各种证明策略,甚至去扩展定理证明器的功能。

用交互式证明器做验证,同数学家证明定理相似。区别在于,在使用证明器时可以调用一些程序去证明某些小定理,但另一方面,证明过程比数学家要更为细致。对许多数学家认为“显然”的东西,在计算机中需要开发出一套专门的数学理论。

交互式证明同软件开发也有相似性。开发一个证明相当于写了一个大软件。在INTEL中,人工写的证明策略的长度超过VERILOG代码的长度。

阅读(2067) | 评论(0) | 转发(1) |
给主人留下些什么吧!~~