Japanese subtitles

← 02-45 Automated Inferring

Get Embed Code
4 Languages

Showing Revision 1 created 06/09/2014 by K2480.

  1. 具体例を挙げて説明しましょう
  2. 平方根を求める関数において
    xを取得し平方根を返します
  3. 2、4、16という値で関数を呼び出します
  4. 平方根を2の値で呼び出すと
  5. xは2でepsは10e-7の値であると推測できます
  6. これらのパターンもインスタンス化します
  7. xは2以上もしくはxは2以下である
  8. これらのパターンは値には有効だからです
  9. 次の反復で平方根を4で呼び出します
  10. するとxは常に2という不変条件が削除されます
  11. しかしxは4以下であるという条件が有効になります
  12. 新たな値と以前の不変条件がマージするのです
  13. xは2以上という条件は新しい値にも有効です
  14. 16の平方根を呼び出して
    得られる不変条件は16以下かつ2以上で
  15. これが最終的な条件です
  16. xは2と16の間でepsは常に10e-7
  17. 事後条件に関しては戻り値の類似値域が分かります
  18. 戻り値は2と4の平方根の間です
  19. これは16の平方根です
  20. しかし2乗した戻り値は
    xと等しいということが分かります
  21. Daikonが適切なパターンを有しているからです
  22. つまり2つの変数の乗算は
    3つ目の変数と等しいというパターンです
  23. そして戻り値でインスタンス化され
    再び戻り値とxでインスタンス化されます
  24. このパターンは少なくとも
    整数によるすべての実行で有効です
  25. 浮動小数点を入力すると
    丸め誤差のためepsが始動します
  26. そしてこのパターンはもう見つかりません
  27. Daikonはパターンライブラリにあるものしか
    作り出せませんが
  28. パターンを追加すれば
    さらにプロパティが見つかるでしょう
  29. もう少しDaikonを使いましょう
  30. 完ぺきなパターンがあっても
  31. このような手法は入力される実数によって決まります
  32. Daikonが作るものはすべての実行に適していますが
  33. 平方根の事前条件にはxが0以上である場合を除き
    xを制限する値域がないことは分かっています
  34. また平方根の戻り値は必ずしも
    2の平方根と16の平方根の間にあるとは限りません
  35. 実際にこれは0より大きいです
  36. つまり始点で素晴らしいテストが行われるのならば
  37. 不変条件の動的推論のツールはとても有効です
  38. xと戻り値の正確な範囲を得る正しい方法は?
  39. 0の値で平方根を呼び出す
  40. 1の値で平方根を呼び出す
  41. maxintの値が最大の整数である場合に
    maxintの値で平方根を呼び出す
  42. 負値で平方根を呼び出す
  43. 複数の呼び出しが必要です
    正確な値域を得るのに必要なものを選んでください