程序验证方法，函数与反函数 两则

[zhang3]

http://www.douban.com/note/109898706/
http://www.douban.com/note/109960005/

程序验证方法，是通过给定：

1 输入谓词
2 输出谓词

然后通过程序验证工具来判断，这个程序是否满足以上两个条件。

这个模型存在一个有趣的，自相矛盾的悖论：

a 如果1和2不能完全的表达对程序的要求，那么程序验证是不完善的。

b 如果1和2已经完全的表达了对程序的要求，那么程序验证是不需要的。

a很好理解。

而对于b，如果已经通过1和2完全的表达了对程序的要求，那么这个程序验证的断言，就是程序本身，又何必需要对什么程序进行验证呢？

这个模型之所以能够存在的前提是这样，举例来说

我写了一个算平方根的程序，输入x输出y为x的平方根，很复杂，我很晕。
我心里知道这个程序输入正整数的时候输出也应该是正整数，但是算法太复杂了我不知道会不会输出一个负数出来。
所以我要验证一下这个输入输出断言对于这个程序是否成立。

所以，程序验证永远不可能是完全的验证，一旦要成为完全的验证，那么必然会写出一个本身就相当于程序功能的输入-输出断言出来。

函数与反函数：

这里要说的不是数学上的函数与反函数，而是这样一个编程上的问题：

给定一个函数，f(x)

function f(x)
... ...;
return result;
end

请问，如何得到这个函数的反函数？

这个问题就很有意思了。

初步猜测如下：

1 对于某些函数，反函数是可以通过特定的步骤和方法而得到的。
2 对于某些函数，反函数是可以通过猜测和逼近的方法而得到近似解。
3 对于某些函数，反函数不存在。

[朱晋玄]

或者存在连续性和有序性的话倒是可以考虑解方程的方法

在 2010年12月3日 下午6:41，Ding, Cong <dingc...@gmail.com> 写道：
> 这样的函数跟数学上的函数没有区别啊，就是一个映射而已
>
> 如果不知道函数体，想要根据输出得到输入，除了穷举没有别的办法
>

[open audio]

这里考虑的是，如何从分析函数代码的过程本身得到反函数的代码，这和数学的解法还是有区别的。