Я работаю над проектом, в котором мне нужно написать контракт для метода, использующего COFOJA, и я должен сгенерировать код для метода из контрактов, используя эвристику.
1) Как я смогу сканировать аннотации, используемые в COFOJA, такие как @ require, @ensures и т. Д.?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