Chinese, Simplified subtitles

← 02-45 自动推导

Get Embed Code
4 Languages

Showing Revision 1 created 04/05/2013 by 秀隆 杨.

  1. 让我给你看个例子。
  2. 一个求平方根的函数。
  3. 参数x,返回平方根。
  4. 分别用2 , 4, 16来调用。
  5. 用2来调用求平方根函数时,
  6. 我们可以知道,x的值是2,
  7. 然而,这些也是实例:
  8. x <= 2, x >= 2,
  9. 因为这些模式对所有的值都成立。
  10. 下次迭代中,用4来调用,
  11. x总为2的不变量已经被删掉。
  12. 我们现在只知道,x <= 4还成立。
  13. 我们可以拿前面的不变量和新的这个进行合并。
  14. x >= 2也就仍成立了。
  15. 当我们用16来调用时,不变量就是
  16. x <= 16 and x >= 2
  17. 最后的结果就是:
  18. x 在2-16之间,eps总是10^-7。
  19. 对后置条件来说,也能得到类似的返回值范围。
  20. 介于2的平方根和4之间。
  21. 4就是16的平方根。
  22. 然而,还有就是,返回值的平方要等于x。
  23. 能发现这一点,是因为Daikon有一个针对这个情况的模式,
  24. 即任意两个变量的相乘 == 另一变量的模式,
  25. 它的实例化是通过两个返回值 和x,
  26. 这个模式不管如何运行程序都是成立的--
  27. 至少对于整数是这样。
  28. 如果是浮点数嘛,精度会起作用,
  29. 因为舍入错误,则这个模式就不能成立了。
  30. 所以Daikon可以得到的其实局限于它拥有的模式库,
  31. 但如果你加入更多的模式,就能发现更多的性质,
  32. 只是会让Daikon更费时一点,才能发现这些模式。
  33. 还有,即使有一个完美的模式集了,
  34. 这样的方法也要基于实际的数值,
  35. 调用的参数的值。
  36. Daikon会把运行中发现的关联都找出来,
  37. 不过我们也知道,平方根的实际先决条件
  38. 并不由x来进行特定的限制,
  39. 除了限制下x必须>= 0。
  40. 同样,返回值也不用是2平方根到
  41. 16的平方根之间。
  42. 它可以是>= 0的任意值。
  43. 所以,不变量动态引用的工具可以很好的发挥作用,
  44. 只要在一开始就有很好的测试集。
  45. 我们应该如何得到x 和返回值正确的范围呢?
  46. 通过用0来调用 这个函数?
  47. 用1来调用?
  48. 用最大的整数来调用,
  49. 还是用负数来调用?
  50. 提示:你需要多个调用。
  51. 选择所有你认为需要的选项。交给你了。