COFOJA を使用してメソッドのコントラクトを作成する必要があるプロジェクトに取り組んでおり、ヒューリスティックを使用してコントラクトからメソッドのコードを生成する必要があります。
1) @requires、@ensures などの COFOJA で使用される注釈をスキャンするにはどうすればよいですか? 2) 抽象構文ツリーを生成する場合、AST に注釈/契約言語も含まれるかどうか?
例：私のプロジェクトへの次の入力を検討してください
class Test{
@requires( { a> 0})
@ensures( {a==0 implies fact(a)=1 , and a>0 implies fact(a) = fact(a-1)*a } )
public int fact (int a)
{
}
}
// Output of first version of code: (Its a rough estimate of code,)
class Test1{
public int fact (int a)
{
if (a==0)
return 1;
if(a >0)
return a*fact(a-1);
if(a<0) throw new AssertionException("Precondition failed/violated a<0 ");
}
} // end of class