jml2b.structure.jml
Class Exsures

java.lang.Object
  jml2b.util.Profiler
      jml2b.structure.jml.Exsures

All Implemented Interfaces:

Linkable, java.io.Serializable, TypeCheckable

public class Exsures

extends Profiler

implements Linkable, TypeCheckable, java.io.Serializable

This class implements an exsures clause, that is an exception type, a field corresponding to the exception and a property.

Author:

L. Burdy, A. Requet

See Also:

Serialized Form

Field Summary

Fields inherited from interface jml2b.link.Linkable

STATE_LINKED, STATE_LINKED_STATEMENTS, STATE_LINKED_TYPE_CHECKED, STATE_UNLINKED

Constructor Summary

Exsures(Type t, java.lang.String name, Expression s)
Constructs an exsure clause.

Method Summary

java.lang.Object	clone()
Type	getExceptionType() Returns the type of the exception.
Expression	getExpression() Returns the property ensured by this exsures clause.
static void	getExsures(java.lang.String str, java.util.Vector v) Stores the exsures clauses corresponding to str into v.
Field	getField() Returns the field declared into the exsures clause.
Exsures	instancie() Instancie the clause.
void	link(IJml2bConfiguration config, LinkContext c)
int	linkStatements(IJml2bConfiguration config, LinkContext c)
void	processIdent() Collects all the indentifier of the clause to give them an index in the identifer array.
Exsures	renameParam(Parameters signature, Parameters newSignature)
void	setParsedItem(ParsedItem pi)
java.lang.String	toJava(int indent)
Type	typeCheck(IJml2bConfiguration config, LinkContext c)

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

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

Constructor Detail

Exsures

public Exsures(Type t,
               java.lang.String name,
               Expression s)

Constructs an exsure clause.

Parameters:

t - The type of the exception

name - The name of the thrown exception in the property. It can be null, meaning that the exception is not named

s - The ensured property

Method Detail

getExsures

public static void getExsures(java.lang.String str,
                              java.util.Vector v)
                       throws Jml2bException

Stores the exsures clauses corresponding to str into v.

Parameters:

str - the string that should be parsed.

v - the vector where the resulting exsures are stored.

Throws:

Jml2bException

clone

public java.lang.Object clone()

link

public void link(IJml2bConfiguration config,
                 LinkContext c)
          throws Jml2bException

Specified by:

link in interface Linkable

Throws:

Jml2bException

linkStatements

public int linkStatements(IJml2bConfiguration config,
                          LinkContext c)
                   throws Jml2bException

Specified by:

linkStatements in interface Linkable

Throws:

Jml2bException

typeCheck

public Type typeCheck(IJml2bConfiguration config,
                      LinkContext c)
               throws Jml2bException

Specified by:

typeCheck in interface TypeCheckable

Throws:

Jml2bException

processIdent

public void processIdent()

Collects all the indentifier of the clause to give them an index in the identifer array. This array is then analyzed to give short name when it is possible to identifiers.

See Also:

jml2b.pog.IdentifierResolver#bIdents

instancie

public Exsures instancie()

Instancie the clause. More informations on instancie.

Returns:

the instanciated exsures clause

renameParam

public Exsures renameParam(Parameters signature,
                           Parameters newSignature)

setParsedItem

public void setParsedItem(ParsedItem pi)

getField

public Field getField()

Returns the field declared into the exsures clause.

Returns:

exceptionField

getExceptionType

public Type getExceptionType()

Returns the type of the exception.

Returns:

exceptionType

getExpression

public Expression getExpression()

Returns the property ensured by this exsures clause.

Returns:

expression

toJava

public java.lang.String toJava(int indent)