jml2b.pog.util
Class IdentifierResolver

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.util.IdentifierResolver

public class IdentifierResolver

extends Profiler

This class provides utilities for the treatment of identifiers. Each identifier gets two names, an absolute one and a short one. For example, the absolute name for the field absoluteName of this class would be f_jml2b_util_absoluteName and the short name would be f_absoluteName. Those names are calculated when the processIdent() methods are called. After the PO generation, names are resolved in manner to choose which one will be used in the lemmas. If they are no conflicts the short one will be used.

Author:

L. Burdy

See Also:

jml2b.pog.IdentifierResolver#bIdents, jml2b.pog.IdentifierResolver#resolveIdents(), Formula.processIdent()

Method Summary

boolean	absoluteNameEquals(java.lang.String s) Test whether the absolute name equals the parameter.
static int	addIdent(AClass c) Adds a class identifier in the set of identifier.
static int	addIdent(AField f) Adds a field identifier in the set of identifier.
static int	addIdent(Package p) Adds a package identifier in the set of identifier.
static java.lang.String	bName(int index) Returns the name in the B syntax of an identifier
static void	clearName() Clear the name index of all the named node of the identifier set.
void	clearNName() Clear the name index.
java.lang.String	getBName() Returns the name to be used into the B lemmas.
static void	init(IJml2bConfiguration config) Initialize the set of indentifier to the set containing an element corresponding to the length pseudo field
static void	resolveIdents() Resolve identifiers conflict.
void	setShortName() Indicates that the short name can be used.
boolean	shortNameEquals(IdentifierResolver ts) Test whether the short name equals the parameter.
static void	unResolveIdents() Disallow all identifier of the set of identifier to use their short name
void	unsetShortName() Indicates that the absolute name can be used.

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

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

Method Detail

init

public static void init(IJml2bConfiguration config)
                 throws Jml2bException

Initialize the set of indentifier to the set containing an element corresponding to the length pseudo field

Throws:

Jml2bException

bName

public static java.lang.String bName(int index)

Returns the name in the B syntax of an identifier

Parameters:

index - The index of the searched identifier

addIdent

public static int addIdent(AField f)

Adds a field identifier in the set of identifier.

Parameters:

f - The field to add

Returns:

The index in the identifier set of the added identifier.

addIdent

public static int addIdent(AClass c)

Adds a class identifier in the set of identifier.

Parameters:

c - The class to add

Returns:

The index in the identifier set of the added identifier.

addIdent

public static int addIdent(Package p)

Adds a package identifier in the set of identifier.

Parameters:

p - The package to add

Returns:

The index in the identifier set of the added identifier.

clearName

public static void clearName()

Clear the name index of all the named node of the identifier set.

See Also:

NamedNode.clearName()

resolveIdents

public static void resolveIdents()

Resolve identifiers conflict. Allows to set short names to identifier that are not conflictual

unResolveIdents

public static void unResolveIdents()

Disallow all identifier of the set of identifier to use their short name

getBName

public java.lang.String getBName()

Returns the name to be used into the B lemmas.

Returns:

the absolute or the short name depending on getAbsoluteName

absoluteNameEquals

public boolean absoluteNameEquals(java.lang.String s)

Test whether the absolute name equals the parameter.

Parameters:

s - tested string

Returns:

true if the string is equal to the absolute name, false otherwise.

shortNameEquals

public boolean shortNameEquals(IdentifierResolver ts)

Test whether the short name equals the parameter.

Returns:

true if the string is equal to the short name, false otherwise.

setShortName

public void setShortName()

Indicates that the short name can be used.

unsetShortName

public void unsetShortName()

Indicates that the absolute name can be used.

clearNName

public void clearNName()

Clear the name index.

See Also:

NamedNode.clearName()