如何扫描使用 COFOJA 编写的合同中使用的注释？

发布于 2024-11-25 12:27:07 字数 688 浏览 3 评论 0原文

我正在开发一个项目，我必须使用 COFOJA 为方法编写合同，并且必须使用启发式方法从合同生成方法代码。

1) 我如何能够扫描 COFOJA 中使用的注释，如 @requires、@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

原文

I am working on a project, where I have to write a contract for a method using COFOJA , and I have to generate code for method from the contracts using heuristics.

1) How will I be able to scan Annotations used in COFOJA like @ requires, @ensures etc?
2) IF I generate Abstract syntax tree, whether the AST will contain annotations / contract language also?

for ex: consider following input to my project

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

分享到QQ

分享到微博