JML

org.jmlspecs.jmlrac
Class TransMethod.SpecCase

java.lang.Object
  extended byorg.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
Constructor Detail

TransMethod.SpecCase

protected TransMethod.SpecCase(JmlSpecBodyClause[] bc)
Method Detail

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));
 


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.