开发者

How to scan Annotations used in contracts written using COFOJA?

开发者 https://www.devze.com 2023-03-21 06:29 出处:网络
I am working on a project, where I have to write a contract for a method usi开发者_JAVA百科ng COFOJA , and I have to generate code for method from the contracts using heuristics.

I am working on a project, where I have to write a contract for a method usi开发者_JAVA百科ng 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


to set eclipse: http://webcourse.cs.technion.ac.il/236700/Spring2013/ho/WCFiles/Contracts%20for%20Java.pdf

and for cofoja: https://fsteeg.wordpress.com/2011/02/07/setting-up-contracts-for-java-in-eclipse/

0

精彩评论

暂无评论...
验证码 换一张
取 消