TransMethod.GeneralSpecCase (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.jmlrac
Class TransMethod.GeneralSpecCase

java.lang.Object
  org.jmlspecs.jmlrac.TransMethod.SpecCase
      org.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.