org.jmlspecs.jml4.rac
Class DesugarSpec

java.lang.Object
  org.eclipse.jdt.internal.compiler.ASTVisitor
      org.jmlspecs.jml4.rac.DefaultRacAstVisitor
          org.jmlspecs.jml4.rac.DesugarSpec

All Implemented Interfaces:

JavaAstVisitor, JmlAstVisitor, RacAstVisitor

public class DesugarSpec
extends DefaultRacAstVisitor

A JML visitor class for desugaring method specifications. In the desugared form, a generic specification, a normal behavior specification and a exceptional specification are all translated into a (general form of) behavior specification. A case-analysis specification, known as specification cases, and a nested specification are also desugared. The desugaring does not produce a completely desugared method specification, but a partial form sufficient for the further processing by the runtime assertion checker.

In the desugared specification, each specification case is translated into a general behavior specification case. If necessary, a default specification body clause such as ensures clause and signals clause is added. A specification cases specification is desugared by copying specificification variable declarations and specification headers into each specification case. A nested specification is desugared by unfolding the nesting. For example, the following specification:

  also requires p1; {| ensures p2; also ensures p3; |}
  also behavior ensures p4;
  also normal_behavior ensures p5;
  also exceptional_behavior signals (E e) p6;
 

is desugared into:

  also behavior requires p1; ensures p2;
  also behavior requires p1; ensures p3;
  also behavior ensures p4;
  also behavior ensures p5; signals (Exception e) false;
  also behavior signals (E e) p6; ensures false;
 

Author:

Amritam Sarcar and Yoonsik Cheon

Constructor Summary

DesugarSpec()

Method Summary

JmlSpecCaseHeader	addRequiresClause(JmlSpecCaseBody bs, JmlRequiresClause req) Add the given requires clause to this specification case.
JmlMethodSpecification	perform(JmlMethodSpecification mspec, TypeReference[] exceptions) Returns a desugared specification of the given method specification.
void	traverse(JmlMethodSpecification self, BlockScope scope)
boolean	visit(JmlMethodSpecification self, BlockScope scope) Desugars the given JML specification.
boolean	visit(JmlSpecCaseBlock self, BlockScope scope)
boolean	visit(JmlSpecCase jmlSpecCase, BlockScope scope)
boolean	visit(JmlSpecCaseBody jmlSpecCaseBody, BlockScope scope)
boolean	visit(JmlSpecCaseRestAsClauseSeq self, BlockScope scope)
boolean	visit(JmlSpecCaseRest self, BlockScope scope)
void	visitJmlBehaviorSpec(JmlSpecCase self) Desugars a behavior specification.
void	visitJmlExceptionalBehaviorSpec(JmlSpecCase self) Desugars an exceptional behavior specification.
void	visitJmlExceptionalSpecBody(JmlSpecCaseRest self) Desugars an exceptional specification body.
void	visitJmlExceptionalSpecCase(JmlSpecCaseBody self) Desugars an exceptional specification case.
void	visitJmlExtendingSpecification(JmlMethodSpecification self, BlockScope scope) Desugar an extending specification.
void	visitJmlGenericSpecBody(JmlSpecCaseRest self) Desugars a generic specification body.
void	visitJmlGenericSpecCase(JmlSpecCaseBody self) Desugars a generic specification case.
void	visitJmlNormalBehaviorSpec(JmlSpecCase self) Desugars a normal behavior specification.
void	visitJmlNormalSpecBody(JmlSpecCaseRest self) Desugars a normal specification body.
void	visitJmlNormalSpecCase(JmlSpecCaseBody self) Desugars a normal specification case.

Methods inherited from class org.jmlspecs.jml4.rac.DefaultRacAstVisitor

endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class org.eclipse.jdt.internal.compiler.ASTVisitor

acceptProblem, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.jmlspecs.jml4.rac.JmlAstVisitor

endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Constructor Detail

DesugarSpec

public DesugarSpec()

Method Detail

perform

public JmlMethodSpecification perform(JmlMethodSpecification mspec,
                                      TypeReference[] exceptions)

Returns a desugared specification of the given method specification.

Parameters:

mspec - the method specification to be desugared

exceptions - exceptions that the target method may throw.

Returns:

the desugared method specification

See Also:

#visitJmlSpecification(JmlSpecification)

visit

public boolean visit(JmlMethodSpecification self,
                     BlockScope scope)

Desugars the given JML specification. In the desugared specification, each specification case is translated into a general behavior specification case. A default specification body clause such as ensures clause and signals clause is added if necessary. A specification cases specification is desugared by copying specification variable declarations and specification headers into each specification case. A nested specification is desugared by unfolding the nesting. For example, the following specification:

  also requires p1; {| ensures p2; also ensures p3; |}
  also behavior ensures p4;
  also normal_behavior ensures p5;
  also exceptional_behavior signals (E e) p6;
 

is desugared into:

  also behavior requires p1; ensures p2;
  also behavior requires p1; ensures p3;
  also behavior ensures p4;
  also behavior ensures p5; signals (Exception e) false;
  also behavior signals (E e) p6; ensures false;
 

Both the subclassing contract and redundant specifications are not desugared.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:

visit in interface JmlAstVisitor

Overrides:

visit in class ASTVisitor

addRequiresClause

public JmlSpecCaseHeader addRequiresClause(JmlSpecCaseBody bs,
                                           JmlRequiresClause req)

Add the given requires clause to this specification case.

traverse

public void traverse(JmlMethodSpecification self,
                     BlockScope scope)

visitJmlExtendingSpecification

public void visitJmlExtendingSpecification(JmlMethodSpecification self,
                                           BlockScope scope)

Desugar an extending specification. In the desugared specification, each conjoinable specification is translated into a corresponding behavior conjoinable specification, if necssary, with a default specification body clause added. For example, the method specification of:

  and ensures p1; 
  and behavior ensures p2;
  and normal_behavior ensures p3;
  and exceptional_behavior signals (E e) p4;
 

is desugared into:

  and behavior ensures p1;
  and behavior ensures p2;
  and behavior ensures p3; signals (Exception e) false;
  and behavior signals (E e) p4; ensures false;
 

Redundant specifications are not desugared.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

visitJmlBehaviorSpec

public void visitJmlBehaviorSpec(JmlSpecCase self)

Desugars a behavior specification.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

visitJmlNormalBehaviorSpec

public void visitJmlNormalBehaviorSpec(JmlSpecCase self)

Desugars a normal behavior specification.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

visitJmlExceptionalBehaviorSpec

public void visitJmlExceptionalBehaviorSpec(JmlSpecCase self)

Desugars an exceptional behavior specification.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

visitJmlGenericSpecCase

public void visitJmlGenericSpecCase(JmlSpecCaseBody self)

Desugars a generic specification case.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

visitJmlGenericSpecBody

public void visitJmlGenericSpecBody(JmlSpecCaseRest self)

Desugars a generic specification body.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

visit

public boolean visit(JmlSpecCaseRest self,
                     BlockScope scope)

visit

public boolean visit(JmlSpecCaseRestAsClauseSeq self,
                     BlockScope scope)

Specified by:

visit in interface JmlAstVisitor

Overrides:

visit in class ASTVisitor

visit

public boolean visit(JmlSpecCaseBlock self,
                     BlockScope scope)

Specified by:

visit in interface JmlAstVisitor

Overrides:

visit in class ASTVisitor

visit

public boolean visit(JmlSpecCase jmlSpecCase,
                     BlockScope scope)

Specified by:

visit in interface JmlAstVisitor

Overrides:

visit in class ASTVisitor

visit

public boolean visit(JmlSpecCaseBody jmlSpecCaseBody,
                     BlockScope scope)

Specified by:

visit in interface JmlAstVisitor

Overrides:

visit in class ASTVisitor

visitJmlNormalSpecCase

public void visitJmlNormalSpecCase(JmlSpecCaseBody self)

Desugars a normal specification case.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

visitJmlNormalSpecBody

public void visitJmlNormalSpecBody(JmlSpecCaseRest self)

Desugars a normal specification body.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

visitJmlExceptionalSpecCase

public void visitJmlExceptionalSpecCase(JmlSpecCaseBody self)

Desugars an exceptional specification case.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

visitJmlExceptionalSpecBody

public void visitJmlExceptionalSpecBody(JmlSpecCaseRest self)

Desugars an exceptional specification body.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);