Ȣȇȫ౨௹২ᘐǛဇƍƨǤȳȐȪǢȳȈᘮᙴȆǹȈ
ǱȸǹƷᐯѣဃ঺ƴǑǔ Daikon ЈщƷોծ
Improving Daikon’s output with Automated Generation of Test Suites
based on Invariant Coverage and Model Checking Techniques‫ؗ‬ųႺՁ∗ ‫ޢ‬᣼ųීɤ† ౿ஜųჇʚ‡
Summary. Daikon dynamically detects program invariants. Considering its eﬀectiveness and outputs’ qualities, Daikon is a useful tool. It,
however, has a problem that its outputs depend on the test suites used
for the dynamic analysis. This paper proposes an automated generation
method of the test suites based on invariant coverage and model checking techniques. Applying the method to an example shows that theproposed method improves quality of the test suites as well as Daikon’s
generating invariants.

1

ǇƑƕƖ

Design by Contract(એ㒠㧘DbC ߣߔࠆ) [1] ߪ㧘઀᭽ࠍ᳿ቯߔࠆᲑ㓏ߢࡔ࠰࠶࠼߿ࠢ࡜ࠬߩ೙⚂ࠍ᳿߼ߡ߅ߊߎߣߢ㧘ࡊࡠࠣ࡜ࡓߩା㗬ᕈ߿ౣ೑↪ᕈࠍะ਄ߐߖࠆ㧚߹ߚ㧘ࡊࡠࠣ࡜ࡓߩ⴫᣿ (assertion) ߪ㧘ࡊࡠࠣ࡜ࡓ߇࠰࡯ࠬࠦ࡯࠼ਛߩ޽ࠆ․ቯߩ
႐ᚲߢḩߚߔߴ߈᧦ઙࠍ⴫ߔ㧚DbC ߦၮߠ޿ߡࡊࡠࠣ࡜ࡓߩ⴫᣿ࠍ⸥ㅀߔࠆߎߣߢ㧘࠰࡯ࠬࠦ࡯࠼ߩ઀᭽ℂ⸃ߩ⵬ഥ߿ࡊࡠࠣ࡜ࡓᬌ⸽߇ⴕ߃ࠆ㧚ㄭᐕߩ࠰࡯ࠬࠦ࡯࠼ࠨࠗ࠭ߩჇടߦߣ߽ߥ޿㧘ᣢሽࠦ࡯࠼ߦኻߒߡᚻേߦࠃࠆ⴫᣿↢ᚑߪ࿎㔍ߦߥߞߡ߈ߡ޿ࠆ㧚ߘߩߚ߼㧘⴫᣿ߩ⥄േ↢ᚑᚻᴺ߿⥄േᬌᩏᚻᴺ߇ᵈ⋡ߐࠇߡ޿ࠆ㧚⴫᣿ߩ↢ᚑߣᬌᩏߩ⥄േൻᚻᴺߦߪ㧘㕒⊛ᚻᴺߣേ⊛ᚻᴺߩ 2 ⒳㘃ߩࠕࡊࡠ࡯࠴
߇޽ࠆ [2]㧚㕒⊛ᚻᴺ [3–9] ߪ࠰࡯ࠬࠦ࡯࠼ߩ⁁ᘒࠍ⴫ߔࡕ࠺࡞ࠍ↢ᚑߒታⴕߒᓧࠆోߡߩ⁁ᘒࠍ᳞߼ࠆߚ߼㧘♖ᐲߩ㜞޿⴫᣿ߩ⥄േ↢ᚑ [3–6] ߿⥄േᬌᩏ [7–9] ߇น⢻ߢ޽ࠆ㧚ߒ߆ߒ㧘৻⥸⊛ߦߪࡕ࠺࡞ߩ⁁ᘒᢙߦኻߔࠆࠬࠤ࡯࡜ࡆ࡝࠹ࠖ߇⺖㗴ߢ޽ࠆ㧚৻ᣇ㧘േ⊛ᚻᴺߪᲧセ⊛ዋߥ޿ᤨ㑆㧘ࡔࡕ࡝ߢ⴫᣿ߩ↢ᚑ߇น⢻ߢ޽ࠆ߇㧘ᓧࠄࠇࠆታⴕ࠺࡯࠲߇ዋߥ޿႐ว㧘⥄േᬌᩏߦߪਇะ߈ߢ޽ࠆ㧚ߘߩߚ߼㧘േ⊛ᚻᴺߪ⴫᣿ߩ⥄േ↢ᚑߦ↪޿ࠄࠇࠆߎߣ߇ᄙߊ㧘ߘߩઍ⴫⊛࠷࡯࡞ߣߒߡ Daikon [10, 11]߇޽ࠆ㧚ߒ߆ߒ㧘⴫᣿ߩേ⊛↢ᚑᚻᴺߩ໧㗴ὐߣߒߡ㧘↢ᚑߐࠇࠆ⴫᣿߇ታⴕ࠺࡯࠲ࠍขᓧߔࠆ㓙ߦ↪޿ࠆ࠹ࠬ࠻ࠤ࡯ࠬߦଐሽߔࠆ࠹ࠬ࠻ࠤ࡯ࠬଐሽ໧㗴߇޽ࠆ [12]㧚
ᧄ⎇ⓥߢߪ㧘⴫᣿ࠍേ⊛ߦ⥄േ↢ᚑߔࠆᚻᴺߦ⌕⋡ߒ㧘ߘߩ࠹ࠬ࠻ࠤ࡯ࠬଐሽ໧
㗴ࠍᡷༀߔࠆߚ߼㧘ࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒ [13]㧘ࡕ࠺࡞ᬌᩏེ Java PathFinder [8, 9]㧘
⸥ภታⴕ [14, 15] ߩᛛⴚࠍᵴ߆ߒߚᣂᚻᴺࠍឭ᩺ߔࠆ㧚ࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒ [13] ߣߪ㧘േ⊛↢ᚑ࠷࡯࡞ߦ↪޿ࠆ࠹ࠬ࠻ࠤ࡯ࠬߩ᦭↪ᕈࠍ᷹ቯߔࠆߚ߼ߦឭ᩺ߐࠇߚࠞࡃ࡟࠶ࠫߢ޽ࠆ㧚ߎߩ୯߇㜞޿ߣ߈㧘േ⊛↢ᚑ࠷࡯࡞ߪା㗬ᕈߩ㜞޿⴫᣿ࠍ↢ᚑߢ߈ࠆ㧚ᢥ₂ [13] ߢߪࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒߩߚ߼ߦቯ⟵–૶↪ㅪ㎮ࠍឭ᩺ߒߡ޿ࠆ㧚ߎߩㅪ㎮ࠍㅢࠆታⴕࡄࠬߪ࠹ࠬ࠻ࠤ࡯ࠬ↢ᚑߦ᦭↪ߢ޽ࠆ߇㧘ߘߩࠃ߁ߥ࠹ࠬ࠻ࠤ࡯ࠬ↢ᚑᴺߦߟ޿ߡߪ⸒෸ߒߡ޿ߥ޿㧚Java PathFinder(એ㒠㧘JPF ߣߔࠆ) [8, 9] ߪ㧘Java ߩ࠰࡯ࠬࠦ࡯࠼߇ᜰቯߒߚ᧦ઙࠍḩߚߔ߆ߤ߁߆ࠍ್ቯߔࠆࡕ࠺࡞ᬌᩏེߢ޽ࠆ㧚JPF ߪᜰቯߒߚ᧦ઙࠍḩߚߐߥ޿႐วߦߘߩ෻଀ߣߥࠆታⴕࡄࠬࠍ᳞߼ࠆߎߣ߇ߢ߈ࠆ㧚⸥ภታⴕ [14, 15] ߪታ∗

Naoya HORI, ᄢ㒋ᄢቇᄢቇ㒮ᖱႎ⑼ቇ⎇ⓥ⑼Kozo OKANO, ᄢ㒋ᄢቇᄢቇ㒮ᖱႎ⑼ቇ⎇ⓥ⑼‡Shinji KUSUMOTO, ᄢ㒋ᄢቇᄢቇ㒮ᖱႎ⑼ቇ⎇ⓥ⑼†FOSE2008ⴕࡄࠬ߆ࠄߘߩታⴕࡄࠬࠍㅢࠆߚ߼ߦᔅⷐߥ౉ജߩ᧦ઙࠍ▚಴ߔࠆ㧚ࠃߞߡ㧘ᧄឭ᩺ᚻᴺߪ JPF ߢขᓧߒߚታⴕࡄࠬߦኻߒߡ⸥ภታⴕࠍⴕ޿㧘ߘߩ⚿ᨐ↢ᚑߐࠇߚ౉ജߩ᧦ઙࠍ↪޿ࠆߎߣߢ㧘࠹ࠬ࠻ࠤ࡯ࠬߩ⥄േ↢ᚑࠍน⢻ߣߒߡ޿ࠆ㧚
ᧄⓂߪᢥ₂ [13] ߢឭ᩺ߐࠇߡ޿ࠆࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒߦၮߠߊ࠹ࠬ࠻ࠤ࡯ࠬߩቯ⟵ࠍ߽ߣߦ㧘ߐࠄߦ⸥ภታⴕߥߤߩᣢሽߩ᭎ᔨ߿ JPF ߥߤߩ࠷࡯࡞ࠍ↪޿ߡ࠹ࠬ࠻ࠤ࡯ࠬߩ↢ᚑࠍ⥄േൻߔࠆߎߣߢ Daikon ߩ಴ജࠍᡷༀߔࠆᚻᴺࠍᣂߚߦឭ᩺ߔࠆ㧚
ᢥ₂ [6] ߪᧄ⺰ᢥߣห᭽ߦ⸥ภታⴕࠍ↪޿ߡ⴫᣿↢ᚑࠍⴕߞߡ޿ࠆ߇㧘[6] ߪ⴫᣿ࠍ㕒⊛ߦ↢ᚑߒߡ޿ࠆߩߦኻߒߡ㧘ᧄᚻᴺߪ⴫᣿ߩ↢ᚑߦേ⊛↢ᚑࠍ↪޿ߡ޿ࠆ㧚
ᧄᚻᴺߢ↢ᚑߐࠇߚ࠹ࠬ࠻ࠤ࡯ࠬߣ⴫᣿ࠍ㧘ᣢሽߩࠞࡃ࡟࠶ࠫߦၮߠ޿ߚ࠹ࠬ࠻ࠤ࡯ࠬߣ⴫᣿ߣࠍߘࠇߙࠇࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒ㧘ା㗬ᕈߣ޿߁ⷰὐߢ⹏ଔߒߚ㧚ߘߩ⚿ᨐ㧘࠹ࠬ࠻ࠤ࡯ࠬ㧘⴫᣿ߣ߽ߦᧄᚻᴺߢᡷༀߐࠇߚߎߣ߇ࠊ߆ߞߚ㧚એ㒠㧘2 ┨ߢᧄ⎇ⓥ߇ኻ⽎ߣߔࠆ໧㗴ߦߟ޿ߡㅀߴ㧘3 ┨ߢᧄ⎇ⓥߦ㑐ㅪߔࠆ࠷࡯
࡞߿᭎ᔨߦߟ޿ߡㅀߴ㧘4 ┨ߢឭ᩺ᚻᴺߣ଀㗴߳ߩㆡ↪⚿ᨐࠍ␜ߒ㧘5 ┨ߢ⠨ኤࠍⴕ޿㧘6 ┨ߢ߹ߣ߼ࠆ㧚2ȆǹȈǱȸǹ̔‫܍‬բ᫆ƱƦƷોծ૾ඥᧄ┨ߢߪ㧘ᧄ⎇ⓥ߇ኻ⽎ߣߔࠆ໧㗴ߣߘߩᡷༀᣇᴺߩ᭎⇛ߦߟ޿ߡㅀߴࠆ㧚

2.1 ȆǹȈǱȸǹ̔‫܍‬բ᫆⴫᣿ߩേ⊛↢ᚑᚻᴺߦ߅ߌࠆ⺖㗴ߣߒߡ࠹ࠬ࠻ࠤ࡯ࠬଐሽ໧㗴߇޽ࠆ [12]㧚േ⊛↢ᚑᚻᴺߪኻ⽎ߩ࠰࡯ࠬࠦ࡯࠼ࠍ࠹ࠬ࠻ࠤ࡯ࠬࠍ↪޿ߡታⴕߒ㧘ߘߎߢᓧߚ࠺࡯࠲ࠍ⸃ᨆߔࠆߎߣߢ⴫᣿ࠍ↢ᚑߔࠆ㧚ߎߩታⴕࠍⴕ߁㓙ߦ↪޿ࠆ࠹ࠬ࠻ࠤ࡯ࠬ߇↢ᚑߐࠇࠆ⴫᣿ߦᄢ߈ߥᓇ㗀ࠍਈ߃ߡߒ߹߁ߩ߇࠹ࠬ࠻ࠤ࡯ࠬଐሽ໧㗴ߢ޽ࠆ㧚
2.1.1 ѣႎဃ঺ƴᢘƠƨȆǹȈǱȸǹേ⊛↢ᚑߦㆡߒߚ࠹ࠬ࠻ࠤ࡯ࠬࠍኻ⽎ߩ࠰࡯ࠬࠦ࡯࠼߇ታⴕߒᓧࠆࡄࠬࠍోߡታⴕߔࠆ࠹ࠬ࠻ࠤ࡯ࠬߣߔࠆ㧚ߎࠇߪ㧘․ቯߩࡄࠬࠍታⴕߒߥ޿ߣ㧘࠹ࠬ࠻ࠤ࡯ࠬଐሽ໧㗴߇⊒↢ߔࠆน⢻ᕈ߇޽ࠆߚ߼ߢ޽ࠆ㧚ߎߩࠃ߁ߥ⠨߃ߢឭ᩺ߐࠇߚࠞࡃ࡟࠶ࠫߦࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒ (Invariant Coverage) [13] ߇޽ࠆ㧚ࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒߪኻ⽎ߩ࠰࡯ࠬࠦ࡯࠼߇ታⴕߒᓧࠆࡄࠬࠍ᳞߼㧘ߘߩᔅⷐߥࡄࠬࠍ࠹ࠬ࠻ࠤ࡯ࠬߦࠃߞߡߤߩ⒟ᐲታⴕߐࠇࠆ߆ߢ࠹ࠬ࠻ࠤ࡯ࠬߩ᦭↪ᕈࠍ᷹ቯߔࠆ߽ߩߢ㧘ߎߩࠞࡃ࡟࠶ࠫߦၮߠ޿ߡ↢ᚑߐࠇߚ࠹ࠬ࠻ࠤ࡯ࠬߪ᦭↪ߥ߽ߩߢ޽ࠆߎߣ߇␜ߐࠇߡ޿ࠆ [13]㧚
2.1.2 ોծ૾ඥƷಒဦ
ᧄឭ᩺ᚻᴺߢߪ㧘ࡕ࠺࡞ᬌᩏᛛⴚࠍ↪޿ߡኻ⽎ߩࠦ࡯࠼߇ታⴕߒᓧࠆࡄࠬߣߘߩࡄࠬࠍㅢࠆ౉ജߩ᧦ઙࠍ᳞߼㧘ߘߩ᧦ઙ߆ࠄ࠹ࠬ࠻ࠤ࡯ࠬࠍ⥄േߢ↢ᚑߔࠆߎߣߢ㧘࠹ࠬ࠻ࠤ࡯ࠬଐሽ໧㗴ࠍᡷༀߔࠆ㧚⴫᣿ߩേ⊛↢ᚑ࠷࡯࡞ߣߒߡ Daikon, ࡕ࠺࡞ᬌᩏེߣߒߡ Java PathFinder [8, 9] ࠍ↪޿ߚ㧚߹ߚ㧘ࡄࠬ߆ࠄ౉ജߩ᧦ઙࠍ᳞߼ࠆᣇ
ᴺߣߒߡ⸥ภታⴕ [14, 15]㧘౉ജ᧦ઙߩ◲⇛ൻࠍⴕ߁࠷࡯࡞ߣߒߡ Simplify [19] ࠍ↪޿ߡ޿ࠆ㧚3แͳᧄ┨ߢߪ㧘ᧄ⎇ⓥߦ↪޿ࠆ㧘޽ࠆ޿ߪ㧘ኻ⽎ߦߔࠆ࠷࡯࡞ߩ᭎ⷐ߿ࠗࡦࡃ࡝ࠕࡦ
࠻ⵍⷒߥߤߩ᦭↪ߥ᭎ᔨߦߟ޿ߡ◲නߦㅀߴࠆ㧚

3.1
DaikonDaikon [10, 11] ߪ౉ജߢ޽ࠆ࠰࡯ࠬࠦ࡯࠼ߣ࠹ࠬ࠻ࠤ࡯ࠬ߆ࠄ㧘ታⴕᤨߦࡔ࠰࠶
࠼ߩ౉ญ㧘಴ญ (એ㒠㧘ࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻ߣߔࠆ) ߦߡෳᾖน⢻ߥᄌᢙߩ୯ࠍ᷹ⷰ
ߔࠆḰ஻ࠍⴕ޿㧘࠹ࠬ࠻ࠤ࡯ࠬࠍ↪޿ߡ࠰࡯ࠬࠦ࡯࠼ࠍታⴕߔࠆ㧚ߘߒߡ㧘ߘߩታⴕ߆ࠄᓧࠄࠇߚᄌᢙߩ୯ߣ Daikon ߇ᜬߟ⴫᣿ࡄ࠲࡯ࡦߣࠍᾖวߒߡฦࡊࡠࠣ࡜ࡓ

Improving Daikon’s output with Automated Generation of Test Suitesࡐࠗࡦ࠻ߦ߅ߌࠆ⴫᣿ࠍ⥄േ↢ᚑߒ㧘಴ജߔࠆ㧚

3.2 ǤȳȐȪǢȳȈᘮᙴ࠹ࠬ࠻ࠤ࡯ࠬଐሽ໧㗴ࠍᡷༀߔࠆߚ߼ߦߪ㧘⴫᣿ߩേ⊛↢ᚑߦ↪޿ࠆ࠹ࠬ࠻ࠤ࡯
ࠬߪోߡߩታⴕࡄࠬࠍㅢࠆ߽ߩߢ޽ࠆᔅⷐ߇޽ࠆ㧚ࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒ [13] ߪ৻⥸⊛ߥ⴫᣿ߩ↢ᚑߦᔅⷐߥታⴕࡄࠬߦኻߔࠆ࠹ࠬ࠻ࠤ࡯ࠬ߇ㅢࠆታⴕࡄࠬߩഀวࠍ␜ߔ㧚ᢥ₂ [13] ߢߪ㧘ߎߩࠃ߁ߥታⴕࡄࠬࠍࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻ߦߡෳᾖน⢻ߥᄌᢙߩቯ⟵–૶↪ㅪ㎮ࠍ฽߻ታⴕࡄࠬߦㄭૃߒߡ޿ࠆ㧚‫ܭ‬፯ 1 ቯ⟵–૶↪ㅪ㎮ (Deﬁnition-Use Chain㧘એ㒠 DUC)ࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻ S ߦߡෳᾖน⢻ߥᄌᢙ v ߩ DUC ߪ㧘ᰴߩࠃ߁ߦቯ⟵ߢ߈ࠆ㧚Deﬁniton-Use ࡍࠕ (એ㒠㧘DU ࡍࠕߣߔࠆ) ࠍᄌᢙ v 㧘ቯ⟵ㇱ d㧘૶↪ㇱ u ߩ 3 㗄⚵ߢቯ⟵ߒ㧘v(d, u) ߢ⴫⸥ߔࠆ㧚ߎߎߢ㧘d㧘u ߪࡊࡠࠣ࡜ࡓ⸥ㅀਛߩ૏⟎ࠍ⴫ߔ㧚
DUC ߪ DU ࡍࠕߩ (᦭㒢) ♽೉ߣߒߡቯ⟵ߢ߈㧘એਅߩࠃ߁ߦ⴫⸥ߔࠆ㧚v(x1 , x0 ) ⇐ v(x2 , x1 ) . . . ⇐ v(xn , xn−1 ) (n ≥ 1)
⋥೨ߩ d ߇ᰴߩ DU ࡍࠕߩ u ߢ޽ࠆ㧚ߎߩ♽೉ߦ߅޿ߡ㧘૏⟎ d㧘u ߩⶄᢙ࿁ߩ಴⃻ߪ⸵ߔ߇㧘ห৻ DU ࡍࠕߩⶄᢙ࿁ߩ಴⃻ߪ⸵ߐߥ޿㧚♽೉ߩᦨᓟߦ߅޿ߡ d㧘u ߇ห৻ߩ૏⟎ߩߣ߈㧘ߎߩ DU ࡍࠕߩ➅ࠅ㄰ߒࠍ⸵ߒ㧘ߘߩ႐ว㧘એਅߩࠃ߁ߦ⴫⸥ߔࠆ㧚ߥ߅㧘‫⋥ߪޠ||ޟ‬೨ߩ DU ࡍࠕߩ➅ࠅ㄰ߒࠍᗧ๧ߔࠆ㧚v(x1 , x0 ) ⇐ v(x2 , x1 ) . . . ⇐ v(xn , xn−1 ) ⇐ v(xn , xn ) || (n ≥ 1)‫ܭ‬፯ 2 ࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒ
ోࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻ߦߡෳᾖน⢻ߥోᄌᢙߩ DUC ߩ✚ᢙࠍ DU Call 㧘࠹ࠬ࠻ࠤ࡯ࠬߦࠃߞߡታⴕߐࠇߚ DUC ߩᢙࠍ DU Cexecuted ߣߔࠆ㧚ߎߩߣ߈㧘޽ࠆ࠹ࠬ࠻ࠤ࡯ࠬߦ߅ߌࠆࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒ CInv ߩ୯ߪᑼ (1) ߢቯ⟵ߐࠇࠆ㧚CInv = DU Cexecuted /DU Call(1)એ㒠㧘ࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒߦၮߠ޿ߡ૞ᚑߒߚ࠹ࠬ࠻ࠤ࡯ࠬࠍࠗࡦࡃ࡝ࠕࡦ࠻ⵍ
ⷒ࠹ࠬ࠻ࠤ࡯ࠬߣ๭߱㧚
3.3 Java PathFinder
JPF [8, 9] ߪ Java ߩ࠰࡯ࠬࠦ࡯࠼ࠍኻ⽎ߣߒߚࡕ࠺࡞ᬌᩏེߢ޽ࠆ㧚JPF ߪ࠰࡯ࠬࠦ࡯࠼ߣߘߩ࠰࡯ࠬࠦ࡯࠼߇ḩߚߔߴ߈᧦ઙࠍ⸥ㅀߒߚࡊࡠࡄ࠹ࠖࡈࠔࠗ࡞ࠍ౉
ജߣߒ㧘࠰࡯ࠬࠦ࡯࠼߇ࡊࡠࡄ࠹ࠖࡈࠔࠗ࡞ߦ⸥ㅀߐࠇߚ᧦ઙࠍḩߚߔ߆ߤ߁߆ࠍ
್ቯߒ㧘ḩߚߐߥ޿႐วߦ෻଀ߣߒߡߘߩታⴕࡄࠬࠍ಴ജߔࠆ㧚ߎߎߢࡔ࠰࠶࠼ߩታⴕࡄࠬߣߪ㧘ࡔ࠰࠶࠼ߩᒁᢙߩขᓧ߆ࠄ᧦ઙߦ㆑෻ߔࠆ߹ߢߦታⴕߔࠆ࠰࡯ࠬࠦ࡯
࠼ਛߩ๮઎ᢥߩ♽೉ߢ޽ࠆ㧚
3.4 ᚡӭܱᘍƱƦƷЈщƷቇဦ҄⸥ภታⴕ [14, 15] ߪ㧘࠰࡯ࠬࠦ࡯࠼ਛߩฦታⴕࡄࠬߦ߅ߌࠆታⴕน⢻ߥ౉ജ᧦ઙࠍ⸥ภᠲ૞⊛ߦ⺰ℂᑼߣߒߡ᳞߼ࠆᚻᴺߢ޽ࠆ㧚⸥ภታⴕߢߪታⴕࡄࠬߩ౉ജ᧦ઙࠍ᳞߼ࠆ㓙ߦ㧘ࡔ࠰࠶࠼ߩᒁᢙߣߒߡ X ߿ Y ߥߤߣ޿ߞߚ⸥ภࠍઍ౉ߔࠆߎߣߢ㧘ฦታⴕࡄࠬࠍㅢࠆ৻⥸⊛ߥ᧦ઙࠍ᳞߼ࠆߎߣ߇ߢ߈ࠆ㧚߹ߚ㧘▚಴ߐࠇߚ᧦ઙᑼ߇౬㐳ߦߥࠆߎߣ߇޽ࠆ㧚ߘߩߚ߼㧘ቯℂ⸽᣿ེ Simplify [19] ࠍ↪޿ߡ᧦ઙᑼߩ◲⇛ൻࠍⴕ߁㧚Simplify ߪ౉ജߐࠇߚᑼ߇ᕡ⌀߆ุ߆ࠍ್ቯߔࠆቯℂ⸽᣿ེߢ޽ࠆ㧚߹ߚ㧘Simplify ߪ౉ജᑼ߇ᕡ⌀ߢߥ޿ߣ್ቯߒߚߣ߈㧘ߘߩᑼ߇ల⿷น⢻ߥ႐วߪߘߩ෻଀ࠍ಴ജߔࠆ㧚ߎߩ෻଀ࠍ↪޿ࠆߎߣߢ㧘ᑼߩ◲⇛ൻࠍⴕ߃ࠆߎߣ߇޽ࠆ㧚࿑ 1 ߪ◲නߥ⸥ภታⴕߩ଀ߢ޽ࠆ㧚ߎߩ଀ߢߪ㧘ᄌᢙ x㧘y ߦኻߒߡߘࠇߙࠇ⸥ภ
୯ X ߣ Y ࠍઍ౉ߒ㧘ฦታⴕࡄࠬࠍㅢࠆߚ߼ߩ᧦ઙ (࿑ਛߩ PC) ࠍ᳞߼ߡ޿ࠆ㧚଀߃߫㧘࠰࡯ࠬࠦ࡯࠼ߩ 2 ⴕ⋡ࠍታⴕߔࠆ᧦ઙ߇ (X > Y )㧘4 ⴕ⋡ࠍታⴕߔࠆ᧦ઙ߇
ன (X > Y &X > X + 1) ߢ޽ࠆߎߣ߇ࠊ߆ࠆ㧚FOSE2008
ᘙ1౉ജ಴ജ੩క৖ඥƷ‫ݣ‬ᝋƱƢǔբ᫆ƷλщƱЈщ

λщ: ኻ⽎ Java ࠰࡯ࠬࠦ࡯࠼
Јщ 1: ኻ⽎ Java ࠰࡯ࠬࠦ࡯࠼ߩ⴫᣿
Јщ 2: ࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒ࠹ࠬ࠻ࠤ࡯ࠬ

߹ߚ㧘3 ⴕ⋡ߩ else ࠍḩߚߔ᧦ઙ (X > Y &X <= X + 1) ߦኻߒߡ Simplify ࠍㆡ↪ߔࠆߣ㧘ਈ᧦ઙߪᕡ⌀ߢߪߥ޿ߣ್ቯߐࠇ㧘ߘߩ෻଀ߣߒߡ (X <= Y ) ߇಴ജߐࠇ㧘ߎߩุቯࠍߣࠆߎߣߢ㧘ਈ᧦ઙߩ◲⇛ᒻ (X > Y ) ߇ᓧࠄࠇࠆ㧚‫׋‬1ᚡӭܱᘍƷ̊⸥ภታⴕߪߘߩ․ᕈ߆ࠄ࠹ࠬ࠻ࠤ࡯ࠬ↢ᚑ߿࠺ࡃ࠶ࠣ࠷࡯࡞ߥߤߩ࠰࡯ࠬࠦ࡯࠼ߩ㕒⊛⸃ᨆᚻᴺߩ৻ㇱߣߒߡ↪޿ࠄࠇߡ޿ࠆ [17, 18]㧚4੩క৖ඥƱ̊᫆ǁƷᢘဇᧄ┨ߢߪ㧘ឭ᩺ᚻᴺߦߟ޿ߡㅀߴ㧘଀㗴߳ߩㆡ↪ߦߟ޿ߡㅀߴࠆ㧚

4.1 ੩క৖ඥƷ‫ݣ‬ᝋƱƢǔբ᫆Ʊ৖ඥƷؕஜǢǤȇǣǢߎߩ▵ߢߪ㧘ឭ᩺ᚻᴺߩ౉ജ߿಴ജ㧘߹ߚ಴ജߩ⹏ଔၮḰߦߟ޿ߡㅀߴ㧘ߘߩᓟ㧘ឭ᩺ᚻᴺߩၮᧄࠕࠗ࠺ࠖࠕࠍㅀߴࠆ㧚
ᧄᚻᴺߩኻ⽎ߣߔࠆ໧㗴ߩ౉ജ㧘಴ജࠍ⴫ 1 ߦ߹ߣ߼ࠆ㧚߹ߚ㧘಴ജߩ⹏ଔၮḰߪએਅߩߣ߅ࠅߢ޽ࠆ㧚
1. Јщ 2 ߇ᣢሽߩࠞࡃ࡟࠶ࠫߦၮߠ޿ߚ࠹ࠬ࠻ࠤ࡯ࠬࠃࠅࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒߩⷰὐ߆ࠄᡷༀߐࠇߡ޿ࠆߎߣ㧚
2. Јщ 1 ߇ᣢሽߩࠞࡃ࡟࠶ࠫߦၮߠ޿ߚ࠹ࠬ࠻ࠤ࡯ࠬࠍ↪޿ߚ Daikon ߩታⴕߢ↢ᚑߐࠇߚ⴫᣿ߦᲧߴ㧘ㆡว₸㧘ౣ⃻₸ߩⷰὐ߆ࠄᡷༀߐࠇߡ޿ࠆߎߣ㧚ߎߩ▵ߢߪ㧘ឭ᩺ᚻᴺߩਛᔃ᭎ᔨߣߥࠆ࠹ࠬ࠻ࠤ࡯ࠬߩ⾰ߩᡷༀ㧘ࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒ࠹ࠬ࠻ࠤ࡯ࠬߩ⥄േ↢ᚑߩ 2 ߟࠍవߦ◲නߦㅀߴࠆ㧚
4.1.1 ȆǹȈǱȸǹƷឋƷોծ࠰࡯ࠬࠦ࡯࠼ࠍ㕒⊛ߦ⸃ᨆߒ㧘DUC ࠍ᳞߼ࠆ㧚ߎࠇߦࠃࠅ㧘ࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻ߦߡෳᾖน⢻ߥᄌᢙߩ୯߇ᄌࠊࠆታⴕࡄࠬ߇ࠊ߆ࠆߚ߼㧘ߘࠇߦၮߠ޿ߡ↢ᚑߒߚ࠹ࠬ࠻ࠤ࡯ࠬߩࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒ߇㜞޿୯ߦߥࠅ㧘ߘߩ⚿ᨐߣߒߡ㧘ࠃࠅା㗬ᕈߩ㜞޿⴫᣿߇↢ᚑߐࠇࠆ [13]㧚
4.1.2 ǤȳȐȪǢȳȈᘮᙴȆǹȈǱȸǹƷᐯѣဃ঺․ቯߩታⴕࠍⴕ߁ࠃ߁ߥ࠹ࠬ࠻ࠤ࡯ࠬࠍ↢ᚑߔࠆߚ߼ߦߪ㧘ߘߩ․ቯߩታⴕࠍⴕ
߁ታⴕࡄࠬࠍㅢࠆߚ߼ߦࡔ࠰࠶࠼ߩᒁᢙ߿ࡠ࡯ࠞ࡞ᄌᢙ߇ḩߚߔߴ߈᧦ઙ߇ᔅⷐߢ޽ࠆ (એ㒠㧘࠹ࠬ࠻ࠤ࡯ࠬ೙⚂ߣߔࠆ)㧚ߘߩߚ߼㧘ోࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻ߣಽጘὐ
ߦߡෳᾖน⢻ߥోᄌᢙߩో DUC ࠍㅢࠆߚ߼ߩ࠹ࠬ࠻ࠤ࡯ࠬ೙⚂߇ᔅⷐߢ޽ࠆ㧚ᧄ
ᚻᴺߢߪ JPF ࠍ↪޿ߡ DUC ࠍㅢࠆታⴕࡄࠬࠍขᓧߒ㧘ߘߩታⴕࡄࠬࠍ⸥ภታⴕߔ
ࠆߎߣߢ࠹ࠬ࠻ࠤ࡯ࠬ೙⚂ࠍขᓧߒ㧘ߘߩ࠹ࠬ࠻ࠤ࡯ࠬ೙⚂ࠍ◲⇛ൻߒߚ߁߃ߢ㧘Improving Daikon’s output with Automated Generation of Test Suitesߘߩ೙⚂ࠍḩߚߔ࠹ࠬ࠻ࠤ࡯ࠬࠍ↢ᚑߔࠆ㧚‫ޓ‬੩క৖ඥ
4.2ߎߩ▵ߢߪ㧘ឭ᩺ᚻᴺߩౕ૕⊛ߥᚻ㗅ߦߟ޿ߡㅀߴࠆ㧚ឭ᩺ᚻᴺߢߪ࿑ 2 ߦ␜ߔᚻ㗅ߢࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒ࠹ࠬ࠻ࠤ࡯ࠬࠍ⥄േ↢ᚑߔࠆ㧚‫׋‬2੩క৖ඥƷಒᙲ(Step 1) ࠰࡯ࠬࠦ࡯࠼߆ࠄ᭴ᢥᧁࠍ↢ᚑߒ㧘ࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻㧘ࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻ߦߡෳᾖน⢻ߥᄌᢙࠍขᓧߔࠆ㧚(Syntax Tree Generator)㧧
(Step 2) ขᓧߒߚోᄌᢙߦߟ޿ߡ DUC㧔ቯ⟵ㇱ㧘૶↪ㇱߩ૏⟎ߪ᭴ᢥᧁߩࡁ࡯࠼㧕ࠍ↢ᚑߔࠆ㧚(DUC Generator)㧧
(Step 3) JPF ࠍ↪޿ߡ (Step 2) ߢขᓧߒߚో DUC ߩታⴕࡄࠬࠍขᓧߔࠆ㧚(JavaPathFinder)㧧
(Step 4) ขᓧߒߚోታⴕࡄࠬࠍ⸥ภታⴕߒ㧘࠹ࠬ࠻ࠤ࡯ࠬ೙⚂ࠍ▚಴ߔࠆ㧚(Symbolic Executor)㧧
(Step 5) ࠹ࠬ࠻ࠤ࡯ࠬ೙⚂ࠍḩߚߔ࠹ࠬ࠻ࠤ࡯ࠬࠍ↢ᚑߔࠆ㧚(Test suites Generator)㧧
(Step 6) ↢ᚑߒߚ࠹ࠬ࠻ࠤ࡯ࠬࠍ↪޿ߡ Daikon ࠍታⴕߔࠆ㧚ᰴ▵߆ࠄฦࠬ࠹࠶ࡊߩ⹦⚦ߦߟ޿ߡㅀߴࠆ㧚ૉߒ㧘(Step 6) ߪ߶߷⥄᣿ߥߚ߼⇛ߔࠆ㧚
4.2.1 (Step 1) ನ૨ஙƷဃ঺౉ജߣߒߡਈ߃ࠄࠇߚ࠰࡯ࠬࠦ࡯࠼߆ࠄ᭴ᢥᧁࠍ↢ᚑߔࠆ㧚߹ߚ㧘᭴ᢥᧁ↢ᚑߩ
ㆊ⒟ߢࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻㧘ฦࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻ߦߡෳᾖน⢻ߥᄌᢙࠍขᓧߔࠆ㧚
4.2.2 (Step 2)DUC Ʒဃ঺(Step 1) ߢขᓧߒߚోߡߩᄌᢙߦߟ޿ߡ DUC ߩቯ⟵ㇱ㧘૶↪ㇱࠍᰴߩࠃ߁ߦቯ߼ࠆ㧚૶↪ㇱߪ಴ญ஥ߩࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻㧘ቯ⟵ㇱߪኻ⽎ᄌᢙ߳ߩઍ౉ᢥߩ૏⟎ߢ޽ࠆ㧚᭴ᢥᧁ߆ࠄߎߩቯ⟵ߣ DUC ߩቯ⟵ߦᓥ޿ⶄᢙߩ DUC ࠍᓧࠆ㧚
4.2.3 (Step 3) ܱᘍȑǹƷ౨Ј
JPF ߇್ቯߔࠆ᧦ઙߣߒߡ⴫᣿଀ᄖࠍ⸳ቯߔࠆߎߣߢ㧘DUC ࠍㅢࠆታⴕࡄࠬࠍ᳞߼ࠆ㧚ᚻ㗅ߪᰴߩߣ߅ࠅߢ޽ࠆ㧚
1. ኻ⽎ߩ࠰࡯ࠬࠦ࡯࠼ౝߩฦቯ⟵ㇱ a ߦኻߒߡ a def ߣ޿߁ታⴕࡄࠬᬌ಴↪ߩࡉ࡯࡝ࠕࡦᄌᢙࠍ↪ᗧߒ㧘ቯ⟵ㇱ߇޽ࠆࡔ࠰࠶࠼ߩ╙ 1 ⴕߦ “boolean a def =true;” ߣߥࠆᢥࠍᝌ౉ߔࠆ㧚ߎߩಣℂࠍฦቯ⟵ㇱߦኻߒߡⴕ߁㧚
2. ฦቯ⟵ㇱߩ⋥ᓟߦ “a def = false;” ߣߥࠆᢥࠍᝌ౉ߔࠆ㧚
3. (Step 1) ߢขᓧߒߚขᓧߒߚᄌᢙ߆ࠄ৻ߟࠍㆬ߱㧚ㆬᛯߒߚᄌᢙߦߟ޿ߡ DUCࠍ৻ߟㆬ߱㧚ߎߩ DUC ߩᦨᓟߩ૶↪ㇱߦࠕࠨ࡯࠻ᢥࠍᝌ౉ߔࠆ㧚ࠕࠨ࡯࠻ᢥߩFOSE2008᧦ઙᑼߪ DUC ߇ㅢࠆቯ⟵ㇱߩࡉ࡯࡝ࠕࡦᄌᢙߩุቯߣㅢࠄߥ޿ቯ⟵ㇱߩࡉ࡯࡝ࠕࡦᄌᢙߩ⺰ℂ๺ߢ޽ࠆ㧚ߎߩࠃ߁ߦߔࠆߎߣߢᔅⷐߥቯ⟵ㇱ㧘૶↪ㇱࠍㅢࠆࡄࠬ߇ታⴕߐࠇߚ㓙ߦߘߩታⴕࡄࠬࠍ⴫᣿଀ᄖ߇⊒↢ߒ㧘JPF ߢታⴕࡄࠬࠍᓧࠆߎߣ߇ߢ߈ࠆ㧚
4. JPF ࠍታⴕߒ㧘⴫᣿଀ᄖ߇⊒↢ߒߚታⴕࡄࠬࠍᓧࠆ㧚
5. 3.4. ࠍ DUC ߩᢙߛߌ➅ࠅ㄰ߔ㧚߹ߚ㧘࠰࡯ࠬࠦ࡯࠼ౝߦⶄᢙߩᄌᢙࠍ⚵ߺวࠊߖߚ࡝࠲࡯ࡦᢥ߇޽ࠆ႐ว㧘ߘߩᄌᢙߩ DUC ߩ⚵ߺวࠊߖߦߟ޿ߡ߽ห᭽ߩಣℂࠍⴕ߁㧚JPF ߩታⴕ⚿ᨐߪ Java ߩ๮઎ᢥ㧘ኻᔕߔࠆࡃࠗ࠻ࠦ࡯࠼ߩ๮઎ᢥߩ♽೉߇ᓧࠄࠇࠆ㧚
4.2.4 (Step 4) ȆǹȈǱȸǹСኖƷምЈ࠹ࠬ࠻ࠤ࡯ࠬ೙⚂ߪ㧘ታⴕࡄࠬߦኻߒߡ⸥ภታⴕߔࠆߎߣߢ▚಴ߢ߈ࠆ㧚⸥ภታⴕࠍߔࠆ㓙ߦߪ Java ߩ๮઎ᢥࠍ↪޿ࠆ߇㧘ᧄᚻᴺߢߪ᧦ઙಽጘߥߤߩ⸃ᨆࠍⴕ߁ߚ߼ࡃࠗ࠻ࠦ࡯࠼ߩ๮઎ᢥ߽↪޿ࠆ㧚ߎࠇߪ JPF ߩ಴ജ⚿ᨐਛߩ Java ߩ๮઎ᢥߦߪ㧘ㅢߞߚ᧦ઙಽጘߦ㑐ߔࠆ᣿␜⊛ߥ⸥ㅀ߇ߥ޿ߚ߼㧘ࡃࠗ࠻ࠦ࡯࠼ࠍ⸃ᨆߔࠆߎߣߢಽጘᖱႎࠍขᓧߔࠆᔅⷐ߇޽ࠆߚ߼ߢ޽ࠆ㧚
4.2.5 (Step 5) ȆǹȈǱȸǹƷဃ঺࠹ࠬ࠻ࠤ࡯ࠬߪੂᢙࠍ↪޿ߡ㧘ߘߩਛߢ೙⚂ࠍḩߚߔ߽ߩࠍㆬ߱ߎߣߢታ⃻ߔࠆ㧚ߘߩᚻ㗅ߪએਅߩߣ߅ࠅߢ޽ࠆ㧚
1. ࠹ࠬ࠻ࠤ࡯ࠬ೙⚂ࠍ Java ߦᄌ឵ߔࠆ㧚
2. ߘߩࠦ࡯࠼ࠍ↪޿ߡ࠹ࠬ࠻ࠤ࡯ࠬࠍ↢ᚑߔࠆࠦ࡯࠼ࠍ૞ᚑߔࠆ㧚ߎߩࠦ࡯࠼ߢ
ߪ Java ߩ random 㑐ᢙࠍ↪޿ߡੂᢙࠍ↢ᚑߒ㧘↢ᚑߐࠇߚੂᢙߩ߁ߜోߡߩ೙
⚂ࠍḩߚߔ߽ߩࠍ౉ജߣߒߡ㧘ኻ⽎ߩࡊࡠࠣ࡜ࡓࠍታⴕߔࠆ㧚

4.3 ੩క৖ඥƷ̊᫆ǁƷᢘဇߎߩ▵ߢߪ㧘ឭ᩺ᚻᴺࠍౕ૕⊛ߥ଀㗴ߦㆡ↪ߔࠆ㧚ߥ߅㧘ឭ᩺ᚻᴺߪᧂታⵝߢ޽ࠆߚ߼㧘ߎߎߢㅀߴߡ޿ࠆ⚿ᨐߪ৻ㇱᚻേߦࠃࠆ߽ߩߢ޽ࠆ㧚ᣢሽߩࠞࡃ࡟࠶ࠫߣߒ
ߡߪ๮઎✂⟜₸㧘ߘࠇߦၮߠߊ࠹ࠬ࠻ࠤ࡯ࠬߣߒߡ๮઎✂⟜₸߇ 100% ߢ޽ࠆ࠹ࠬ࠻ࠤ࡯ࠬࠍ↪޿ߚ㧚๮઎✂⟜₸ߣߪ㧘࠰࡯ࠬࠦ࡯࠼ਛߩో๮઎ᢥߩ߁ߜ࠹ࠬ࠻ࠤ࡯
ࠬ߇ታⴕߔࠆ๮઎ᢥߩഀวߢ޽ࠆ㧚Boyer-Moore ᢥሼ೉ᬌ⚝ࠕ࡞ࠧ࡝࠭ࡓࠍ଀㗴ߣߒߡ↪޿ࠆ (࿑ 3㧘એ㒠 BMmatch.java ߣߔࠆ)㧚

‫׋‬3BMmatch.java

Boyer-Moore ᢥሼ೉ᬌ⚝ࠕ࡞ࠧ࡝࠭ࡓߪ 2 ߟߩᢥሼ೉ߦኻߒߡㆡ↪ߔࠆࠕ࡞ࠧ࡝࠭ࡓߢ㧘 ᣇߩᢥሼ೉߇߽߁ ᣇߩᢥሼ೉ࠍ฽߻႐วߪవ㗡ᢥሼ೉ߩࠗࡦ࠺࠶ࠢࠬࠍ㧘฽߹ߥ޿႐วߪ-1 ࠍ㄰ߔ㧚ⶄᢙߩ while ࡞࡯ࡊ㧘ⶄᢙߩ return ߇޽ࠆߎߣ߆ࠄᄙߊߩታⴕࡄࠬ߇޽ࠆߚ߼㧘ࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒߦၮߠ޿ߚ࠹ࠬ࠻ࠤ࡯ࠬߩലᨐ߇

Improving Daikon’s output with Automated Generation of Test Suitesࠃࠅ㗼⪺ߢ޽ࠆߣ⠨߃㧘ߎߩ࠰࡯ࠬࠦ࡯࠼ࠍ଀㗴ߣߒߡㆬࠎߛ㧚
4.3.1 (Step 1) ನ૨ஙƷဃ঺
࿑ 4 ߪ BMmatch.java ߆ࠄ↢ᚑߒߚ᭴ᢥᧁߢ޽ࠅ㧘⴫ 2 ߪࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻ߦߡෳᾖน⢻ߥᄌᢙߢ޽ࠆ㧚‫׋‬4ᘙ2(Step 1) ưࢽǒǕƨ BMmatch.java Ʒನ૨ங

(Step 1) ưࢽǒǕƨ BMmatch.java ƷӲȗȭǰȩȠȝǤȳȈƴƯӋༀӧᏡƳ‫٭‬ૠࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻
Entry
Exit1
Exit2
Exit3

ᄌᢙ
text, patternlast, n, m, i, text, pattern, return
last, n, m, i, j, text, pattern, return
last, n, m, i, j, text, pattern, return4.3.2 (Step 2)DUC Ʒဃ঺⴫ 2 ߩࡊࡠࠣ࡜ࡓࡐࠗࡦ࠻ߦߡෳᾖน⢻ߥᄌᢙߣ࿑ 4 ߦ޽ࠆ᭴ᢥᧁ߆ࠄ㧘࿑ 5 ߦ␜ߒߚࠃ߁ߥ DUC ࠍ↢ᚑߔࠆߎߣ߇ߢ߈ߚ㧚ߥ߅㧘ߎߎߢߪ DUC ߦ߅ߌࠆ૏⟎ߪ᭴ᢥᧁߩࡁ࡯࠼⇟ภߢ⴫ࠊߒߡ޿ࠆ㧚‫׋‬5(Step 2) ưࢽǒǕƨ‫٭‬ૠ i, text, pattern Ʒμ DUC

4.3.3 (Step 3) ܱᘍȑǹƷ౨Ј
࿑ 5 ߢ␜ߒߚ DUC ࠍㅢࠆታⴕࡄࠬࠍ JPF ࠍ↪޿ߡᓧߚ㧚߹ߕ㧘BMmatch.java ౝߩቯ⟵ㇱߪ “2:*Def*”,“9:*Def*”,“11:*Def*” ߩ 3 ߟߢ޽ࠆ㧚ቯ⟵ㇱߦኻᔕߒߚࡉ࡯࡝ࠕࡦቯᢙࠍએਅߩࠃ߁ߦ૞ᚑߔࠆ㧚• boolean a def = true; // 2:*Def*ߦኻᔕ• boolean b def = true; // 9:*Def*ߦኻᔕ• boolean c def = true; // 11:*Def*ߦኻᔕߘࠇߙࠇߩ DUC ߦኻᔕߒߚࠕࠨ࡯࠻ᢥࠍ DUC ߩ૶↪ㇱߦᝌ౉ߔࠆ㧚ߘߩ଀ߣߒߡߪએਅߩࠃ߁ߥ߽ߩ߇޽ࠆ㧚• assert a def || !b def || !c def ; // DUC i(11,10)⇐i(9,11)⇐i(2,9) ߦኻᔕ• assert a def || !b def || c def ; // DUC i(9,10)⇐i(2,9) ߦኻᔕFOSE2008• assert a def || b def || c def ; // DUC i(2,10) ߦኻᔕߎߩࠃ߁ߥࠕࠨ࡯࠻ᢥࠍᝌ౉ߒߚኻ⽎࠰࡯ࠬࠦ࡯࠼ߦኻߒߡ JPF ࠍታⴕߒߚ㧚࿑
6 ߪ㧘ߘߩታⴕ⚿ᨐߪߩ৻ㇱߣߢ޽ࠆ㧚‫׋‬6(Step 3) ưࢽǒǕƨ JPF ƷЈщኽௐ (ɟᢿ)

4.3.4 (Step 4) ȆǹȈǱȸǹСኖƷምЈ
࿑ 7 ߪ㧘DUC‫ޟ‬i(11, 10) ⇐ i(11, 11) ⇐ i(9, 11) ⇐ i(2, 9)‫ࠍޠ‬ታⴕߔࠆߚ߼ߩ࠹ࠬ࠻ࠤ࡯ࠬ೙⚂ߢ޽ࠆ㧚‫׋‬7(Step 4) ưࢽǒǕƨᚡӭܱᘍƷኽௐ

4.3.5 (Step 6)Daikon Ʒܱᘍ(Step 5) ߢᚻേߦࠃࠅ↢ᚑߒߚ࠹ࠬ࠻ࠤ࡯ࠬߩ Daikon ߦኻߔࠆ⚿ᨐࠍ࿑ 8 ߩฝߦ␜ߔ㧚5ᎋ‫ݑ‬ᧄ┨ߢߪ㧘4.3 ߢ␜ߒߚ଀㗴߳ߩㆡ↪⚿ᨐ߆ࠄ㧘ឭ᩺ᚻᴺߩ᦭↪ᕈߦߟ޿ߡ⠨ኤߔࠆ㧚Ყセࠍⴕ߁㓙ߩ್ቯၮḰߪᰴߩߣ߅ࠅߢ޽ࠆ㧚• (Step 5) ߢ↢ᚑߐࠇߚ࠹ࠬ࠻ࠤ࡯ࠬ߇ᣢሽߩࠞࡃ࡟࠶ࠫߦၮߠ޿ߚ࠹ࠬ࠻ࠤ࡯
ࠬࠃࠅࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒߩⷰὐ߆ࠄఝࠇߡ޿ࠆ߆ ?
• ᣢሽߩࠞࡃ࡟࠶ࠫߦၮߠ޿ߚ࠹ࠬ࠻ࠤ࡯ࠬࠍ↪޿ߡ↢ᚑߒߚ⴫᣿ࠃࠅ (Step 6)ߢ↢ᚑߒߚ⴫᣿߇ㆡว₸㧘ౣ⃻₸ߩ୯ߩⷰὐ߆ࠄఝࠇߡ޿ࠆ߆ ?
ߥ߅㧘ㆡว₸ߪ↢ᚑߐࠇߚ⴫᣿ਛߩ᦭↪ߥ⴫᣿ߩഀวࠍ␜ߔ୯ߢ㧘ౣ⃻₸ߪ᦭↪
ߢ޽ࠆ⴫᣿ਛߩ↢ᚑߐࠇߚ᦭↪ߥ⴫᣿ߩഀวࠍ␜ߒ㧘ߘࠇࠄߩ୯߇㜞޿ߣ߈ା㗬ᕈߩ㜞޿⴫᣿ࠍ↢ᚑߢ߈ࠆ࠷࡯࡞ߛߣ⠨߃ࠄࠇࠆ㧚ߎߎߢ㧘᦭↪ߥ⴫᣿ߣߪ㧘એਅߩ 2 ߟߩ᧦ઙߩߤߜࠄ߆ࠍḩߚߔ߽ߩߢ޽ࠆ㧚• ․ቯߩࡄࠬߦଐሽߒߥ޿㧚• ․ቯߩࡄࠬߦଐሽߔࠆ᧦ઙ a ߪߘߩࡄࠬࠍㅢࠆ᧦ઙ b ߦࠃߞߡ฽ᗧ (b → a) ߐࠇߡ޿ࠆ㧚Improving Daikon’s output with Automated Generation of Test Suites߹ߚ㧘ㆡว₸㧘ౣ⃻₸ߩቯ⟵ߪᰴߩߣ߅ࠅߢ޽ࠆ㧚‫ܭ‬፯ 3 ㆡว₸ߣౣ⃻₸↢ᚑߐࠇߚ⴫᣿ߩ㓸วࠍ Ag 㧘ኻ⽎ߩ࠰࡯ࠬࠦ࡯࠼߆ࠄੱ߇ᔅⷐߛߣ್ᢿߒߚ⴫᣿
ߩ㓸วࠍ An ߣߔࠆ㧚ߎߩߣ߈㧘ㆡว₸ P 㧘ౣ⃻₸ R ߪએਅߩࠃ߁ߦቯ⟵ߐࠇࠆ㧚

P =| Ag ∩ An | / | Ag |, R =| Ag ∩ An | / | An |5.1 ȆǹȈǱȸǹƷൔ᠋ᣢሽߩࠞࡃ࡟࠶ࠫߦၮߠ޿ߚ࠹ࠬ࠻ࠤ࡯ࠬߩࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒߩ୯ߪ 3/17 ߢ޽ࠅ㧘(Step 5) ߢ↢ᚑߐࠇߚ࠹ࠬ࠻ࠤ࡯ࠬߩࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒߩ୯ߪ 17/17 ߢ޽ࠆ㧚ࠃߞߡ㧘ឭ᩺ᚻᴺࠍ↪޿ߡ↢ᚑߐࠇߚ࠹ࠬ࠻ࠤ࡯ࠬߪࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒߩⷰ
ὐ߆ࠄఝࠇߡ޿ࠆ㧚
5.2ဃ঺ƞǕƨᘙଢƷൔ᠋‫׋‬8Daikon ƷᘙଢЈщƷൔ᠋Ტ߼Ჴଏ‫܍‬ȆǹȈǱȸǹᲦӫᲴ੩క৖ඥƕဃ঺ƠƨȆǹȈǱȸǹᲣ

࿑ 8 ߪ㧘๮઎✂⟜₸߇ 100% ߢ޽ࠆ࠹ࠬ࠻ࠤ࡯ࠬࠍ↪޿ߚ Daikon ߩታⴕ⚿ᨐߣ㧘(Step 6) ߢᓧߚ⴫᣿಴ജߩᲧセࠍ␜ߒߡ޿ࠆ㧚ߎߩ㧞ߟߩ⴫᣿಴ജࠍᲧセߔࠆߣ㧘৻⥸ߢߥ޿⴫᣿ߩ㒰෰ߣ᦭↪ߥ⴫᣿ߩㅊടߩ 2 ߟߩᏅ߇޽ࠆߎߣ߇ࠊ߆ࠆ㧚5.2.1 ɟᑍႎưƳƍᘙଢƷᨊӊ৻⥸⊛ߢߪߥ޿⴫᣿ߣߪ㧘‫ޟ‬pattern.toString one of “abcdefg”, “abdced”, “c” ‫ޠ‬ߩࠃ߁ߥ࠹ࠬ࠻ࠤ࡯ࠬߦଐሽߒߚ⴫᣿ࠍᗧ๧ߔࠆ㧚࿑ 8 ࠃࠅ㧘ឭ᩺ᚻᴺࠍㆡ↪ߔࠆߣ৻⥸⊛ߢߥ޿⴫᣿߇㒰෰ߐࠇߡ޿ࠆߩߢ㧘Daikon ߇↢ᚑߔࠆ⴫᣿ߩㆡว₸ࠍะ਄ߐߖߚߎߣ߇ࠊ߆ࠆ㧚ߎߩℂ↱ߣߒߡߪ㧘ឭ᩺ᚻᴺߦࠃࠅోߡߩࡄࠬࠍ✂⟜ߔࠆ࠹ࠬ࠻ࠤ࡯ࠬࠍ↢ᚑߒߚߚ߼ߦ㧘․ቯߩࡄࠬߦଐሽߔࠆ৻⥸⊛ߢߥ޿⴫᣿߇ᚑࠅ┙ߚߥ޿ታⴕ࠺࡯࠲ࠍᓧࠆߎߣ߇ߢ߈ߚߚ߼ߢ޽ࠆ㧚
5.2.2 ஊဇƳᘙଢƷᡙь᦭↪ߥ⴫᣿ࠍㅊടߔࠆߎߣߢ㧘Daikon ߩ↢ᚑߔࠆ⴫᣿ߩౣ⃻₸ࠍ਄ߍࠆߎߣ߇ߢ߈ࠆ㧚࿑ 8 ࠃࠅ㧘ឭ᩺ᚻᴺࠍㆡ↪ߔࠆߎߣߢ↢ᚑߐࠇߚ⴫᣿ߩਛߦ‫ޟ‬text.toString>= pattern.toString‫⴫߁޿ߣޠ‬᣿߇฽߹ࠇߡ޿ߚ㧚ߎߩ⴫᣿ߪ․ቯߩࡄࠬߦଐሽߒ
ߚ⴫᣿ߢߪߥ޿ߩߢ᦭↪ߥ⴫᣿ߢ޽ࠆ㧚ࠃߞߡ㧘ࠃࠅᄙߊߩ᦭↪ߥ⴫᣿ࠍ↢ᚑߔࠆߎߣ߇ߢ߈ࠆߩߢ㧘Daikon ߇↢ᚑߔࠆ⴫᣿ߩౣ⃻₸ࠍะ਄ߐߖߚߎߣ߇ࠊ߆ࠆ㧚ߎߩℂ↱ߣߒߡߪ㧘ᣢሽᚻᴺߢߪታⴕߒߥ߆ߞߚࡄࠬࠍឭ᩺ᚻᴺߢᓧࠄࠇߚ࠹ࠬ࠻ࠤ࡯FOSE2008ࠬߢታⴕߢ߈ߚߚ߼ߢ޽ࠆߣ⠨߃ࠄࠇࠆ㧚એ਄ࠃࠅ㧘5.1㧘5.2 ߢ␜ߒߚࠃ߁ߦឭ᩺ᚻᴺߪᢥ₂ [13] ߩታ㛎⚿ᨐߣห᭽ߦ࠹ࠬ࠻ࠤ࡯ࠬ㧘⴫᣿಴ജࠍᡷༀߒߡ޿ࠆߩߢ㧘ᧄ⥄േ↢ᚑᚻᴺߪ᦭↪ߢ޽ࠆߣ⠨߃ߡ޿ࠆ㧚6ƋƱƕƖᧄ⎇ⓥߢߪ㧘ࠗࡦࡃ࡝ࠕࡦ࠻ⵍⷒߦၮߠߊ࠹ࠬ࠻ࠤ࡯ࠬߩ⥄േ↢ᚑᚻᴺࠍឭ᩺ߒߚ㧚ߎߩᚻᴺߪ Daikon ࠍࡌ࡯ࠬߦߒߥ߇ࠄ㧘ߎߩᰳὐߢ޽ࠆ࠹ࠬ࠻ࠤ࡯ࠬଐሽ໧
㗴ࠍ DUC ߿⸥ภታⴕࠍ↪޿ࠆߎߣߦࠃࠅᡷༀߒߡ޿ࠆ㧚BMmatch.java ࠍ଀㗴ߣߒ㧘ᧄᚻᴺߣᣢሽᚻᴺࠍ⹏ଔߒߚ⚿ᨐ㧘࠹ࠬ࠻ࠤ࡯ࠬߣ⴫᣿߇ߣ߽ߦᡷༀߐࠇࠆߎ
ߣ߇ࠊ߆ߞߚ㧚੹ᓟߪᚻᴺߩታⵝࠍⴕ޿㧘ታ↪଀㗴߳ߩㆡ↪ߦࠃࠆ⹏ଔ߿ታⴕല₸߅ࠃ߮⸘▚㊂ߩ⹏ଔ㧘㕒⊛↢ᚑ࠷࡯࡞ߣߩᲧセߥߤࠍⴕ޿ߚ޿㧚Ӌᎋ૨ྂ
[ 1 ] B. Meyer: “Applying Design by Contract,” Computer (IEEE), vol.25, no.10, pp.40-51,
1992.
[ 2 ] J. W. Nimmer and M. D. Ernst: “Invariant Inference for Static Checking: An EmpiricalEvaulation,” in Proc. of SIGSOFT Symp. on Foundations of Software Engineering 2002, FSE
2002, pp.11-20, 2002.
[ 3 ] P. Cousot and R. Cousot: “Modular Static Program Analysis, ” Compiler Construction,LNCS, vol.2304, pp.159-178, 2002.
[ 4 ] C. Flanagan and K. R. Leino: “Houdini, an Annotation Assistant for ESC/Java,” inProc. of Int. Symp. of Formal Methods Europe on Formal Methods for Increasing Software
Productivity, FME 2001, pp.500-517, 2001.
[ 5 ] N. Tillmann, F. Chen and W. Schulte: “Discovering likely method speciﬁcations,” Int.
Conf. on Formal Engineering Methods, ICFEM 2006, LNCS 4260, 2006.
[ 6 ] P. H. Schmitt and B. Weiss: “Invariants by Symbolic Execution,” in Proc. of the 4thInternational Veriﬁcation Workshop, VERIFY 2007, pp.195-210, 2007.
[ 7 ] D. L. Detlefs, K. Rustan M. Leino, G. Nelson and J. B. Saxe: “Extended static Checking,”
SRC Research Report 159, Compaq SRC, 1998.
[ 8 ] W. Visser, K. Havelund,k G. Brat, S. Park and F. Lerda: “Model Checking Programs,”
Automated Software Engineering Journal 2003, vol.10, pp.203-232, 2003.
[ 9 ] F. Lerda and W. Visser: “Addressing Dynamic Issues of Program Model Checking,” inProc. of Int. Workshop on SPIN Model Checking 2001, pp.88-102, 2001.
[10] M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz and C.
Xiao: “The Daikon System for Dynamic Detection of Likely Invariants,” Science of Computer
Programming, vol.69, no.1-3, pp.35-45, 2007.
[11] J. W. Nimmer and M. D. Ernst: “Automatic Generation of Program Speciﬁcation,” inProc. of SIGSOFT Int. Symp. on Software Testing and Analysis 2002, pp.232-242, 2002.
[12] J. W. Nimmer and M. D. Ernst:“Static Veriﬁcation of Dynamically Detected Program
Invariants: Integrating Daikon and ESC/Java,” in Proc. of First Workshop on Runtime Veriﬁcation, RV 2001, pp.152-171, 2001.
[13] N. Gupta and Z. V. Heidepriem: “A New Structural Coverage Criterion for Dynamic
Detection of Program Invariants,” in Proc. of Int. Conf. on Automated Software Engineering,ASE 2003, pp.49-58, 2003.
[14] S.Khurshid, C. S. Pasareanu and W. Visser: “Generalized Symbolic Execution for Model
Checking and Testing,” in Proc. of Int. Conf. on Tools and Algorithms for the Constructionand Analysis of Systems, TACAS 2003, pp.553-568, 2003.
[15] J. C. King: “Symbolic Execution and Program Testing,” Communications of the ACM
1976, vol.19, no.7, pp.385-394, 1976.
[16] N. Gupta: “Generating Test Data for Dynamically Discovering Likely Program Invariants,” in Proc. of ICSE 2003 Workshop on Dynamic Analysis, WODA 2003, pp.21-24, 2003.
[17] C. Boyapati, S. Khurshid and D. Marinov: “Korat: Automated Testing based on Java
Predicates,” in Proc. of Int. Symp. on Software Testing and Analysis 2002, ISSTA 2002,
pp.123-133, 2002.
[18] W. R. Bus, J. D. Pincus and D. J. Sielaﬀ: “A Static Analyzer for Finding DynamicProgramming Errors,” Software: Practice and Experience, 30(7), pp.775-802, 2000.
[19] D. Detlefs, G. Nelson, J. B. Saxe: “Simplify: A Theorem Prover for Program Checking,”
Journal of the ACM, vol.52, no.3, pp.365-473, 2005.