以文本方式查看主题

-  计算机科学论坛  (http://bbs.xml.org.cn/index.asp)
--  『 软件工程论坛 』   (http://bbs.xml.org.cn/list.asp?boardid=48)
----  谈谈最近看到三本书上讲的同一个话题  (http://bbs.xml.org.cn/dispbbs.asp?boardid=48&rootid=&id=26106)

--  作者：pennyliang
--  发布时间：1/3/2006 11:35:00 PM

--  谈谈最近看到三本书上讲的同一个话题
Meyer的OOSC，关于ADT的描述
Basse的算法分析，关于recusive的正确性描述
离散数学中相关概念

任何一个事物的正确性描述都要有specification,符合specification就是正确，反之就是错误，至于specification的正确性由precondition,postcondition,invariants保证。

引理
在一个块的precondition为真的情况下，postcondition一定能在routine退出时满足，并且同时满足invariants.

precondition是routine定义域的一个在全域上的特征函数。
每一个带有preconditon的routine都是偏函数，任何去掉precondition的方法，例如在返回值中做出变化来表达错误码都是不对的

在证明一个算法是否正确就要证明算法在preconditon被满足的情况下，总可以满足postcondition.

W 3 C h i n a ( since 2003 ) 旗 下 站 点
苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》
 46.875ms