JML

org.jmlspecs.jmlrac
Class TransMethod.GeneralSpecCase

java.lang.Object
  extended byorg.jmlspecs.jmlrac.TransMethod.SpecCase
      extended byorg.jmlspecs.jmlrac.TransMethod.GeneralSpecCase
Enclosing class:
TransMethod

protected static class TransMethod.GeneralSpecCase
extends TransMethod.SpecCase

A concrete wrapper class to JmlGeneralSpecCase for conjoining multiple specification clauses in a specification case.

Version:
$Revision: 1.66 $
Author:
Yoonsik Cheon
See Also:
JmlGeneralSpecCase

Field Summary
private  JmlGeneralSpecCase spec
          The spec case whose specification clauses to be conjoined.
 
Fields inherited from class org.jmlspecs.jmlrac.TransMethod.SpecCase
bodyClauses
 
Constructor Summary
TransMethod.GeneralSpecCase(JmlGeneralSpecCase spec)
          Constructs a new instance.
 
Method Summary
 boolean hasPrecondition()
          Returns true if this spec case has the precondition specified.
 boolean hasSpecVarDecls()
          Returns true if this spec case has any specification variable declarations.
 JExpression precondition()
          Returns the precondition of this spec case.
 JmlSpecVarDecl[] specVarDecls()
          Returns the specification variable declarations of this spec case.
 
Methods inherited from class org.jmlspecs.jmlrac.TransMethod.SpecCase
conjoin, exceptionalPostcondition, hasExceptionalPostcondition, hasPostcondition, isCheckable, postcondition
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

spec

private JmlGeneralSpecCase spec
The spec case whose specification clauses to be conjoined.

Constructor Detail

TransMethod.GeneralSpecCase

public TransMethod.GeneralSpecCase(JmlGeneralSpecCase spec)
Constructs a new instance.

 requires spec != null && (* spec is desugared *);
 

Method Detail

hasSpecVarDecls

public boolean hasSpecVarDecls()
Returns true if this spec case has any specification variable declarations.


hasPrecondition

public boolean hasPrecondition()
Returns true if this spec case has the precondition specified.


specVarDecls

public JmlSpecVarDecl[] specVarDecls()
Returns the specification variable declarations of this spec case.


precondition

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


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.