jml2b.formula
Class UnaryForm

java.lang.Object
  extended byjml2b.util.Profiler
      extended byjml2b.formula.Formula
          extended byjml2b.formula.UnaryForm
All Implemented Interfaces:
IFormToken, java.io.Serializable
Direct Known Subclasses:
JavaUnaryForm

public class UnaryForm
extends Formula

This class implements unary Formula. The node type can be :

Author:
L. Burdy
See Also:
Serialized Form

Field Summary
 
Fields inherited from interface jml2b.formula.IFormToken
ARRAY_ACCESS, ARRAY_RANGE, B_ACCOLADE, B_APPLICATION, B_ARRAY_EQUALS, B_BOOL, B_BTRUE, B_COUPLE, B_DOM, B_FUNCTION_EQUALS, B_IN, B_INTERVAL, B_OVERRIDING, B_SET_EQUALS, B_SUBSTRACTION_DOM, B_UNION, CONSTANT_FUNCTION, CONSTANT_FUNCTION_FUNCTION, EQUALS_ON_OLD_INSTANCES, EQUALS_ON_OLD_INSTANCES_ARRAY, FINAL_IDENT, GUARDED_SET, INTERSECTION_IS_NOT_EMPTY, IS_ARRAY, IS_MEMBER_FIELD, IS_STATIC_FIELD, Ja_ADD_OP, Ja_AND_OP, Ja_CHAR_LITERAL, Ja_COMMA, Ja_DIFFERENT_OP, Ja_DIV_OP, Ja_EQUALS_OP, Ja_GE_OP, Ja_GREATER_OP, Ja_IDENT, Ja_JAVA_BUILTIN_TYPE, Ja_LE_OP, Ja_LESS_OP, Ja_LITERAL_false, Ja_LITERAL_null, Ja_LITERAL_super, Ja_LITERAL_this, Ja_LITERAL_true, Ja_LNOT, Ja_MOD, Ja_MUL_OP, Ja_NEGATIVE_OP, Ja_NUM_INT, Ja_OR_OP, Ja_QUESTION, Ja_STRING_LITERAL, Ja_UNARY_NUMERIC_OP, Jm_AND_THEN, Jm_EXISTS, Jm_FORALL, Jm_IMPLICATION_OP, Jm_IS_SUBTYPE, Jm_OR_ELSE, Jm_T_OLD, Jm_T_RESULT, Jm_T_TYPE, LOCAL_ELEMENTS_DECL, LOCAL_VAR_DECL, MODIFIED_FIELD, NEW_OBJECT, T_CALLED_OLD, T_TYPE, T_VARIANT_OLD, toString
 
Constructor Summary
UnaryForm(byte nodeType, Formula exp)
          Constructs a unary formula from a formula and a token.
UnaryForm(UnaryForm f)
           
 
Method Summary
 java.lang.Object clone()
          Clones the formula.
 int contains(java.util.Vector selectedFields)
           
 boolean equals(java.lang.Object f)
          Returns whether the formula equals the parameter.
 void garbageIdent()
          Annotates all the fields that appear in the formula to declare them in the Atelier B files.
 BasicType getBasicType()
          Returns the type of a formula
 Formula getExp()
          Returns the leaf formula.
 void getFields(java.util.Set fields)
          Collects the fields that occur in the formula.
 Formula instancie(Formula b)
          Replaces this with the parameter in the expression.
 boolean is(Formula f)
          Returns whether the formula corresponds to a read formula.
 boolean isObvious(boolean atTheEnd)
          Returns whether a formula is obvious.
 void processIdent()
          Collects all the indentifier of a formula to give them an index in the identifer array.
 void save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf)
          Saves the formula in a .jpo file
 Formula sub(Formula a, Formula b, boolean subInCalledOld)
          Applies a substitution on a formula.
 Formula subIdent(java.lang.String a, Formula b)
          Applies a substitution on a formula.
 Formula suppressSpecialOld(int token)
          Suppress the called old pragmas.
 
Methods inherited from class jml2b.formula.Formula
and, create, declarField, domainRestrict, getFalse, getNodeType, getNull, implies, indent, isBFalse, matchAEqualsNull, not, oldParam, or, renameParam, sub, toJava, toLang, toVector
 
Methods inherited from class jml2b.util.Profiler
runGC
 
Methods inherited from class java.lang.Object
getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

UnaryForm

public UnaryForm(UnaryForm f)

UnaryForm

public UnaryForm(byte nodeType,
                 Formula exp)
Constructs a unary formula from a formula and a token.

Parameters:
nodeType - token of the new formula
exp - part of the new formula
Method Detail

clone

public java.lang.Object clone()
Description copied from class: Formula
Clones the formula.

Specified by:
clone in class Formula
Returns:
the cloned formula

sub

public Formula sub(Formula a,
                   Formula b,
                   boolean subInCalledOld)
Description copied from class: Formula
Applies a substitution on a formula.

Specified by:
sub in class Formula
Parameters:
a - the substituted formula
b - the new formula
subInCalledOld - specify whether the substitution should also be applied in the called old construction
Returns:
the formula when the substitution has been applied.

suppressSpecialOld

public Formula suppressSpecialOld(int token)
Description copied from class: Formula
Suppress the called old pragmas. old pragma are substitued with called old into the specification of a called method in manner to be differentiated from the old pragma of the current method. After the treatment, the called old pragmas are suppressed.

Specified by:
suppressSpecialOld in class Formula
Returns:
the formula with suppressed called old pragmas

processIdent

public void processIdent()
Description copied from class: Formula
Collects all the indentifier of a formula to give them an index in the identifer array. This array is then analyzed to give short name when it is possible to identifiers.

Specified by:
processIdent in class Formula
See Also:
jml2b.pog.IdentifierResolver#bIdents

instancie

public Formula instancie(Formula b)
Description copied from class: Formula
Replaces this with the parameter in the expression.

Specified by:
instancie in class Formula
Parameters:
b - expression on which the method where the expression occurs is called.
Returns:
the modified expression

garbageIdent

public void garbageIdent()
Description copied from class: Formula
Annotates all the fields that appear in the formula to declare them in the Atelier B files.

Specified by:
garbageIdent in class Formula

getFields

public void getFields(java.util.Set fields)
Description copied from class: Formula
Collects the fields that occur in the formula.

Specified by:
getFields in class Formula
Parameters:
fields - The set a collected fields.

subIdent

public Formula subIdent(java.lang.String a,
                        Formula b)
Description copied from class: Formula
Applies a substitution on a formula.

Specified by:
subIdent in class Formula
Parameters:
a - the substituted string correspondingto an identifier
b - the new formula
Returns:
the formula when the substitution has been applied.

equals

public boolean equals(java.lang.Object f)
Description copied from class: Formula
Returns whether the formula equals the parameter.

Specified by:
equals in class Formula
Parameters:
f - the checked parameter
Returns:
true if the formula syntaxically equals the parameter, false otherwise

is

public boolean is(Formula f)
Description copied from class: Formula
Returns whether the formula corresponds to a read formula.

Specified by:
is in class Formula
Parameters:
f - a read formula coming from a jpo file
Returns:
true if the formula equals to the read formula, false otherwise.

contains

public int contains(java.util.Vector selectedFields)
Specified by:
contains in class Formula

isObvious

public boolean isObvious(boolean atTheEnd)
Description copied from class: Formula
Returns whether a formula is obvious.

Specified by:
isObvious in class Formula
Returns:
true if the formula is considered as obvious, false otherwise

save

public void save(IJml2bConfiguration config,
                 IOutputStream s,
                 IJmlFile jf)
          throws java.io.IOException
Description copied from class: Formula
Saves the formula in a .jpo file

Specified by:
save in class Formula
Parameters:
config -
s - the ouputstream corresponding to a jpo file
jf -
Throws:
java.io.IOException - when the formula cannot be saved.

getExp

public Formula getExp()
Returns the leaf formula.

Returns:
exp

getBasicType

public BasicType getBasicType()
Description copied from class: Formula
Returns the type of a formula

Specified by:
getBasicType in class Formula
Returns:
The basic type of ta formula.