org.jmlspecs.jmlrac
Class TransMethod.SpecCase

java.lang.Object
  org.jmlspecs.jmlrac.TransMethod.SpecCase

Direct Known Subclasses:

TransMethod.GeneralSpecCase

Enclosing class:

TransMethod

protected static abstract class TransMethod.SpecCase

extends Object

An abstract superclass for conjoining multiple specification clauses, such as requires and ensures clauses, in a specification case.

Version:

$Revision: 1.66 $

Author:

Yoonsik Cheon

Field Summary
protected  JmlSpecBodyClause[]	bodyClauses

 

Constructor Summary
protected	TransMethod.SpecCase(JmlSpecBodyClause[] bc)

 

Method Summary
protected static JExpression	conjoin(List clauses)           Returns a new conjoined expression made out of predicates of the given specification clauses.
private  JmlSignalsClause	desugar(JmlSignalsOnlyClause sig)           Desugars a signals_only clause into a signals clause.
JmlSignalsClause[]	exceptionalPostcondition()           Returns the exceptional postcondition of this spec case.
boolean	hasExceptionalPostcondition()           Returns true if this spec case has the postcondition.
boolean	hasPostcondition()           Returns true if this spec case has the normal postcondition specified.
abstract  boolean	hasPrecondition()           Returns true if this spec case has the precondition specified.
abstract  boolean	hasSpecVarDecls()           Returns true if this spec case has any specification variable declarations.
protected  boolean	isCheckable(JmlSpecBodyClause clause)           Returns true if the given spec body clause is checkable.
JExpression	postcondition()           Returns the normal postcondition of this spec case.
abstract  JExpression	precondition()           Returns the precondition of this spec case.
abstract  JmlSpecVarDecl[]	specVarDecls()           Returns the specification variable declarations of this spec case.

 

Methods inherited from class java.lang.Object

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

 

Field Detail

bodyClauses

protected JmlSpecBodyClause[] bodyClauses

TransMethod.SpecCase

protected TransMethod.SpecCase(JmlSpecBodyClause[] bc)

hasSpecVarDecls

public abstract boolean hasSpecVarDecls()

Returns true if this spec case has any specification variable declarations.

hasPrecondition

public abstract boolean hasPrecondition()

Returns true if this spec case has the precondition specified.

hasPostcondition

public boolean hasPostcondition()

Returns true if this spec case has the normal postcondition specified.

hasExceptionalPostcondition

public boolean hasExceptionalPostcondition()

Returns true if this spec case has the postcondition.

specVarDecls

public abstract JmlSpecVarDecl[] specVarDecls()

Returns the specification variable declarations of this spec case.

precondition

public abstract JExpression precondition()

Returns the precondition of this spec case. If this spec case has multiple requires clauses, the clauses are conjoined.

See Also:

conjoin(List)

postcondition

public JExpression postcondition()

Returns the normal postcondition of this spec case. If this spec case has multiple ensures clauses, the clauses are conjoined.

See Also:

conjoin(List)

isCheckable

protected boolean isCheckable(JmlSpecBodyClause clause)

Returns true if the given spec body clause is checkable. The clause is checkable if it is not a redundant specification or the command line option "noredundancy" is not turned on.

exceptionalPostcondition

public JmlSignalsClause[] exceptionalPostcondition()

Returns the exceptional postcondition of this spec case. If this spec case has multiple signals clauses, the clauses are conjoined. If this spec case has a signals_only clause, it is first desugared into a signals clause.

 ensures \result != null ==> \result.length > 0;
 

See Also:

conjoin(List)

desugar

private JmlSignalsClause desugar(JmlSignalsOnlyClause sig)

Desugars a signals_only clause into a signals clause. A signals_only clause of the form:

  signals_only \nothing;
 

is desugared into the following signals clause:

  signals (java.lang.Exception e) false;
 

Furthermore, a signals_only clause of the form

  signals_only E1, E2, ..., En;
 

is desugared into the following signals clause:

  signals (java.lang.Exception e) 
       e instanceof E1
    || e instanceof E2
       ...
    || e instanceof En;
 

conjoin

protected static JExpression conjoin(List clauses)

Returns a new conjoined expression made out of predicates of the given specification clauses. A null is returned if there is nothing to be conjoined in the given list of specification clauses. A specification clause corresponding to \not_specified is desugared into true.

 requires clauses != null && 
   (\forall Object o; clauses.contains(o); 
     (o instanceof JmlRequiresClause) ||
     (o instanceof JmlEnsuresClause));