|
|||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES All Classes | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectjml2b.util.Profiler
jml2b.formula.Formula
This class describes a formula. A formula is the content of a lemma : an hypothesis or a goal.
Field Summary |
Method Summary | |
static BinaryForm |
and(Formula s1,
Formula s2)
Returns the conjunctive formula between the two parameters. |
abstract java.lang.Object |
clone()
Clones the formula. |
abstract int |
contains(java.util.Vector selectedFields)
|
static Formula |
create(IJml2bConfiguration config,
JpoInputStream s,
IJmlFile fi)
Create a formula from a token read into a stream. |
static Formula |
declarField(Field f)
Returns the formula corresponding to a field declaration. |
Formula |
domainRestrict(java.util.Vector df)
Applies successive domain restriction to the formula |
abstract boolean |
equals(java.lang.Object f)
Returns whether the formula equals the parameter. |
abstract void |
garbageIdent()
Annotates all the fields that appear in the formula to declare them in the Atelier B files. |
abstract BasicType |
getBasicType()
Returns the type of a formula |
static Formula |
getFalse()
Returns the formula false . |
abstract void |
getFields(java.util.Set fields)
Collects the fields that occur in the formula. |
byte |
getNodeType()
Returns the nodeType. |
static Formula |
getNull()
Returns the formula null . |
static BinaryForm |
implies(Formula s1,
Formula s2)
Returns the implicative formula between the two parameters. |
static java.lang.String |
indent(int i)
Returns the string containing white spaces corresponding to an indentation |
abstract Formula |
instancie(Formula b)
Replaces this with the parameter in the expression. |
abstract boolean |
is(Formula f)
Returns whether the formula corresponds to a read formula. |
boolean |
isBFalse()
Returns whether a formula corresponds to bfalse |
abstract boolean |
isObvious(boolean atTheEnd)
Returns whether a formula is obvious. |
boolean |
matchAEqualsNull()
Returns whether a formula matches with an equality with null |
static UnaryForm |
not(Formula s1)
Returns the negation of the parameter. |
Formula |
oldParam(java.util.Vector signature)
Encapsulates given parameters into an old pragma. |
static BinaryForm |
or(Formula s1,
Formula s2)
Returns the disjunctive formula between the two parameters. |
abstract void |
processIdent()
Collects all the indentifier of a formula to give them an index in the identifer array. |
Formula |
renameParam(IAParameters signature,
java.util.Vector newSignature)
Renames the fields belonging to the parameter list with new names. |
abstract void |
save(IJml2bConfiguration config,
IOutputStream s,
IJmlFile jf)
Saves the formula in a .jpo file |
Formula |
sub(Field a,
Field b,
boolean subInCalledOld)
Applies a substitution on a formula. |
abstract Formula |
sub(Formula a,
Formula b,
boolean subInCalledOld)
Applies a substitution on a formula. |
abstract Formula |
subIdent(java.lang.String a,
Formula b)
Applies a substitution on a formula. |
abstract Formula |
suppressSpecialOld(int token)
Suppress the called old pragmas. |
java.lang.String |
toJava(int indent)
Translates the formula into the Java language |
ITranslationResult |
toLang(java.lang.String language,
int indent)
Translates the formula into a given language. |
java.util.Vector |
toVector()
Converts comma separated formulas into a set of formulas. |
Methods inherited from class jml2b.util.Profiler |
runGC |
Methods inherited from class java.lang.Object |
getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Method Detail |
public static Formula getNull()
null
.
null
public static Formula getFalse()
false
.
false
public static BinaryForm or(Formula s1, Formula s2)
s1
- left disjonctive formulas2
- right disjonctive formula
s1 || s2
public static Formula declarField(Field f)
f
- Field to declare.
public static BinaryForm and(Formula s1, Formula s2)
s1
- left conjonctive formulas2
- right conjonctive formula
s1 && s2
public static UnaryForm not(Formula s1)
s1
- negated formula
! s1
public static BinaryForm implies(Formula s1, Formula s2)
s1
- left implicative formulas2
- right implicative formula
s1 ==> s2
public static Formula create(IJml2bConfiguration config, JpoInputStream s, IJmlFile fi) throws java.io.IOException, LoadException
config
- The current configurations
- The input streamfi
- The JML file corresponding to the input stream.
java.io.IOException
- if the end of the stream is reached before the
formula has been read
LoadException
- if the read token is unknown.public static java.lang.String indent(int i)
i
- The indentation number
i
white spaces.public abstract BasicType getBasicType()
public abstract java.lang.Object clone()
public abstract void processIdent()
jml2b.pog.IdentifierResolver#bIdents
public abstract Formula instancie(Formula b)
this
with the parameter in the expression.
b
- expression on which the method where the expression occurs is
called.
public abstract void getFields(java.util.Set fields)
fields
- The set a collected fields.public abstract Formula sub(Formula a, Formula b, boolean subInCalledOld)
a
- the substituted formulab
- the new formulasubInCalledOld
- specify whether the substitution should also be
applied in the called old construction
public abstract Formula suppressSpecialOld(int token)
public abstract Formula subIdent(java.lang.String a, Formula b)
a
- the substituted string correspondingto an identifierb
- the new formula
public abstract boolean equals(java.lang.Object f)
f
- the checked parameter
true
if the formula syntaxically equals the
parameter, false
otherwisepublic abstract boolean is(Formula f)
f
- a read formula coming from a jpo file
true
if the formula equals to the read formula,
false
otherwise.
MergeException
public abstract boolean isObvious(boolean atTheEnd)
true
if the formula is considered as obvious,
false
otherwisepublic abstract void save(IJml2bConfiguration config, IOutputStream s, IJmlFile jf) throws java.io.IOException
config
- s
- the ouputstream corresponding to a jpo filejf
-
java.io.IOException
- when the formula cannot be saved.public abstract void garbageIdent()
public abstract int contains(java.util.Vector selectedFields)
public Formula oldParam(java.util.Vector signature)
old
pragma.
signature
- the signature of a called method
public java.lang.String toJava(int indent)
indent
- The current indentation
public ITranslationResult toLang(java.lang.String language, int indent) throws LanguageException
language
- The language in which the formula should be translated.indent
- The current indentation
LanguageException
- when the language is unknown.public Formula sub(Field a, Field b, boolean subInCalledOld)
a
- the substituted fieldb
- the new fieldsubInCalledOld
- specify whether the substitution should also be
applied in the called old construction
public Formula renameParam(IAParameters signature, java.util.Vector newSignature) throws PogException
signature
- the signature of the called methodnewSignature
- the list of new names
PogException
jml2b.pog.Proofs#renameParam(Parameters, Vector)
public boolean isBFalse()
true
when the formula is false == true
or true == false
, false
otherwise.public boolean matchAEqualsNull()
null
true
if the formula matches with
a == null
, false
otherwise.public java.util.Vector toVector()
BinaryForm.toVector()
public Formula domainRestrict(java.util.Vector df)
df
- set of formula from which the formula should be restricted.
public byte getNodeType()
|
|||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES All Classes | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |