jml2b.pog.lemma
Class Proofs

java.lang.Object
  jml2b.pog.lemma.Proofs

All Implemented Interfaces:

IFormToken, jml.JmlDeclParserTokenTypes, java.io.Serializable

Direct Known Subclasses:

ExceptionalProofs

public class Proofs

extends java.lang.Object

implements jml.JmlDeclParserTokenTypes, java.io.Serializable, IFormToken

This class describes all the proof obligations associated with a method or with the static initialisation. It is the result of the weakest precondition calculus. It contains a list of hypothesis and a list of theorem.

Author:

L. Burdy

See Also:

Serialized Form

Field Summary

Fields inherited from interface jml.JmlDeclParserTokenTypes

ABRUPT_BEHAVIOR, ACCESSIBLE, ACCESSIBLE_KEYWORD, ACCESSIBLE_REDUNDANTLY, ACCESSIBLE_SEQ, ADDITIVE_ASSIGNMENT_OP, ADDITIVE_OP, AFFIRM_KEYWORD, ALSO, AND, ARRAY_DECLARATOR, ASGNABLE_SEQ, ASSERT, ASSERT_REDUNDANTLY, ASSIGN, ASSIGNABLE, ASSIGNABLE_KEYWORD, ASSIGNABLE_REDUNDANTLY, ASSUME, ASSUME_KEYWORD, ASSUME_REDUNDANTLY, AXIOM, BACKWARD_IMPLIES, BADCHAR, BAND, BAND_ASSIGN, BEHAVIOR, BITWISE_ASSIGNMENT_OP, BITWISE_OP, BNOT, BOR, BOR_ASSIGN, BREAKS, BREAKS_KEYWORD, BREAKS_REDUNDANTLY, BREAKS_SEQ, BSR, BSR_ASSIGN, BXOR, BXOR_ASSIGN, CALLABLE, CALLABLE_KEYWORD, CALLABLE_REDUNDANTLY, CALLABLE_SEQ, CASE, CAST, CHAR_LITERAL, CHOOSE, CHOOSE_IF, COLON, COMMA, CONJOINABLE_SPEC, CONSTRAINT, CONSTRAINT_KEYWORD, CONSTRAINT_REDUNDANTLY, CONSTRUCTOR, CONT_SEQ, CONTINUES, CONTINUES_KEYWORD, CONTINUES_REDUNDANTLY, DEC, DECREASES, DECREASES_REDUNDANTLY, DECREASING, DECREASING_KEYWORD, DECREASING_REDUNDANTLY, DEPENDS, DEPENDS_KEYWORD, DEPENDS_REDUNDANTLY, DIM_EXPRS, DIMS, DINFORMALLY, DIV, DIV_ASSIGN, DIV_SEQ, DIVERGES, DIVERGES_KEYWORD, DIVERGES_REDUNDANTLY, DOC_ATSIGN, DOC_ATSIGN_KEYWORD, DOC_AUTHOR, DOC_COMMENT, DOC_COMMENT_START, DOC_DEPRECATED, DOC_EXCEPTION, DOC_JML_SPECS, DOC_NL_WS, DOC_NON_EMPTY_TEXTLINE, DOC_NON_NL_WS, DOC_PARAM, DOC_RETURN, DOC_SEE, DOC_SERIAL, DOC_SERIALDATA, DOC_SERIALFIELD, DOC_SINCE, DOC_THROWS, DOC_UNKNOWN_KEYWORD, DOC_VERSION, DOT, DOT_DOT, ELSE, ENS_SEQ, ENSURES, ENSURES_KEYWORD, ENSURES_REDUNDANTLY, EOF, EQUAL, EQUALITY_OP, EQUIV, EQUIVALENCE_OP, ESC, EXAMPLE, EXCEPTIONAL_BEHAVIOR, EXCEPTIONAL_EXAMPLE, EXPONENT, EXSURES, EXSURES_REDUNDANTLY, EXT_ALSO, EXT_AND, FLOAT_SUFFIX, FOR, FOR_EXAMPLE, FOR_INIT, FOR_TEST, FOR_UPDATER, FORALL, GE, GHOST, GT, HENCE_BY, HENCE_BY_KEYWORD, HENCE_BY_REDUNDANTLY, HEX_DIGIT, IDENT, IGNORED_AT_IN_COMMENT, IMPLICATION_OP, IMPLIES_THAT, INC, INFORMAL_DESCRIPTION, INIT, INITIALIZER, INITIALLY, INSTANCE, INSTANCE_INIT, INVARIANT, INVARIANT_KEYWORD, INVARIANT_REDUNDANTLY, IS_SUBTYPE_OF, JAVA_BUILTIN_TYPE, JAVA_MODIFIER, JML_BACKSLASH_SEQUENCE, JML_MODIFIER, L_ARROW, LABEL, LABEL_KEYWORD, LAND, LBRACK, LCURLY, LCURLY_VBAR, LE, LET, LETOLD_KEYWORD, LIMPLIES, LITERAL_abstract, LITERAL_assert, LITERAL_boolean, LITERAL_break, LITERAL_byte, LITERAL_case, LITERAL_catch, LITERAL_char, LITERAL_class, LITERAL_const, LITERAL_continue, LITERAL_default, LITERAL_do, LITERAL_double, LITERAL_else, LITERAL_extends, LITERAL_false, LITERAL_final, LITERAL_finally, LITERAL_float, LITERAL_for, LITERAL_if, LITERAL_implements, LITERAL_import, LITERAL_instanceof, LITERAL_int, LITERAL_interface, LITERAL_long, LITERAL_native, LITERAL_new, LITERAL_null, LITERAL_package, LITERAL_private, LITERAL_protected, LITERAL_public, LITERAL_return, LITERAL_short, LITERAL_static, LITERAL_strictfp, LITERAL_super, LITERAL_switch, LITERAL_synchronized, LITERAL_this, LITERAL_throw, LITERAL_throws, LITERAL_transient, LITERAL_true, LITERAL_try, LITERAL_void, LITERAL_volatile, LITERAL_while, LNOT, LOGICAL_OP, LOOP_ASGNABLE_SEQ, LOOP_ASSIGNABLE_KEYWORD, LOOP_EXSURES, LOOP_INV_SEQ, LOOP_INVARIANT, LOOP_INVARIANT_REDUNDANTLY, LOOP_MODIFIES, LOOP_SIG_SEQ, LOR, LPAREN, LT, MAINTAINING, MAINTAINING_KEYWORD, MAINTAINING_REDUNDANTLY, MEASURED_BY, MEASURED_BY_KEYWORD, MEASURED_BY_REDUNDANTLY, METH, MINUS, MINUS_ASSIGN, ML_COMMENT, MOD, MOD_ASSIGN, MODEL, MODEL_PROGRAM, MODIFIABLE, MODIFIABLE_REDUNDANTLY, MODIFIER_SET, MODIFIES, MODIFIES_REDUNDANTLY, MONITORED, MONITORED_BY, MULTIPLICATIVE_ASSIGNMENT_OP, MULTIPLICATIVE_OP, NESTED_CLASS, NL_WS, NON_NL_WS, NON_NULL, NORMAL_BEHAVIOR, NORMAL_EXAMPLE, NOT_EQUAL, NOT_EQUIV, NOWARN_LABEL, NOWARN_LABEL_LIST, NULL_TREE_LOOKAHEAD, NUM_FLOAT, NUM_INT, OLD, OR, PARAM, PLUS, PLUS_ASSIGN, POST, POST_DEC, POST_INC, POST_INCREMENT_OP, POST_REDUNDANTLY, PRE, PRE_INCREMENT_OP, PRE_REDUNDANTLY, PRIVACY_MODIFIER, PURE, QUANT_VARS, QUANTIFIED_EXPR, QUANTIFIER_TOKEN, QUESTION, R_ARROW, RBRACK, RCURLY, READABLE_IF, REFINE, RELATIONAL_OP, REPLACE, REPRESENTS, REPRESENTS_KEYWORD, REPRESENTS_REDUNDANTLY, REQUIRES, REQUIRES_KEYWORD, REQUIRES_REDUNDANTLY, RETURNS, RETURNS_KEYWORD, RETURNS_REDUNDANTLY, RETURNS_SEQ, RPAREN, SEMI, SET, SET_COMPR, SHIFT_ASSIGNMENT_OP, SHIFT_OP, SIG_SEQ, SIGNALS, SIGNALS_KEYWORD, SIGNALS_REDUNDANTLY, SL, SL_ASSIGN, SL_COMMENT, SPEC_CASE, SPEC_PROTECTED, SPEC_PUBLIC, SPEC_SL_COMMENT, SPEC_STATEMENT, SR, SR_ASSIGN, STAR, STAR_ASSIGN, STAR_ELEMS, STATIC_INITIALIZER, STRING_LITERAL, SUBCLASSING_CONTRACT, T_ELEMTYPE, T_EVERYTHING, T_EXISTS, T_FIELDS_OF, T_FORALL, T_FRESH, T_INVARIANT_FOR, T_IS_INITIALIZED, T_LBLNEG, T_LBLPOS, T_LOCKSET, T_MAX, T_MIN, T_NONNULLELEMENTS, T_NOT_MODIFIED, T_NOT_SPECIFIED, T_NOTHING, T_NUM_OF, T_OLD, T_OTHER, T_PRODUCT, T_REACH, T_RESULT, T_SUCH_THAT, T_SUM, T_TYPE, T_TYPEOF, T_TYPEOFALLTYPES, UNARY_NUMERIC_OP, UNINITIALIZED, UNREACHABLE, VAR_DECL, VBAR_RCURLY, VF_SEQ, VOCAB, WEAKLY, WHEN, WHEN_KEYWORD, WHEN_REDUNDANTLY, WS

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

Proofs()
Construct an empty proof.

Proofs(Lemma l)
Construct a proof from a lemma

Proofs(Theorem t)
Construct a proof from a theorem

Method Summary

void	addAll(Proofs l) Concats two proofs.
Proofs	addBox(ColoredInfo b) Adds a colored info to the theorems.
void	addHyp(Formula f) Adds new local hypothesis with no associated colored info.
void	addHyp(Formula f, ColoredInfo b, byte origin) Adds new hypothesis.
void	addHyp(Formula f, java.util.Vector b, byte origin) Adds new hypothesis.
void	addHyp(SimpleLemma sl, byte origin) Adds the goals of a lemme to the hypothesis.
java.lang.Object	clone() Clones a proof.
void	finalize(IJml2bConfiguration config, Formula param, Expression invStaticFinalFields, Formula hyp, Formula req, java.lang.String name, ColoredInfo b, ColoredInfo method) Finalize the proof obligations by adding the parameters typing in hypothesis adding the invariant coming from the final static field initialization in hypothesis adding the invariant in hypothesis adding the requires of the current method in hypothesis assigning a name
java.util.Vector	findUsedLocHyp()
void	garbageIdent() Annotates all the fields that appear in the theorem to declare them in the Atelier B files.
void	gc(IJml2bConfiguration config, boolean force) Tries to suppress obvious goals, lemmas, theorems.
void	getFields(java.util.Set fields) Collect the fields present in the current proof obligation.
SimpleLemma	getLemma(int i)
java.util.Vector	getLocFlow()
java.util.Enumeration	getLocHyp() Returns the hypothesis
Theorem	getTheorem(int i)
TheoremList	getThl() Returns the list of theorems.
boolean	isUsed(VirtualFormula vf) Test wheter an hypothesis is used in the theorems.
void	mergeWith(Proofs jf) Merge two proofs.
int	nbLemmas()
int	nbPo() Returns the number of goals (or proof obligations).
int	nbPoChecked()
int	nbPoProved() Returns the number of goals that are in a specified state.
int	nbPoProved(java.lang.String prover) Returns the number of goals that are in a specified state.
int	nbTheorems()
Proofs	param(IJml2bConfiguration config, java.util.Vector signature, Expression param, ExceptionalBehaviourStack exceptionalBehaviour) Renames the formal parameter of a called method by the calling parameters.
void	proveObvious(boolean prove, boolean atTheEnd) Proves the obvious goals if asked.
Proofs	quantify(Formula var, Formula type)
Proofs	quantify(Formula var, Formula type, ColoredInfo b) Quantifies the proof whith a variable.
Proofs	quantify(java.lang.String var, Formula type) Quantifies the proof whith a variable.
Proofs	quantify(java.lang.String var, Formula type, ColoredInfo b) Quantifies the proof whith a variable.
Proofs	quantify(java.lang.String var, Type type, ColoredInfo b) Quantifies the proof whith a variable.
Proofs	renameParam(IAParameters signature, java.util.Vector newSignature) Rename the fields belonging to the parameter list with new names.
void	save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) Saves the proof in the a .jpo file
void	saveThl(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf)
Proofs	selectLabel(java.util.Vector labels) Selects in the lemmas corresponding to behaviours, the cases corresponding to labels.
Proofs	sub(Substitution s) Apply a substitution to the content of the proof.
Proofs	suppressSpecialOld(int token) Suppress the Called Old expressions in the proof.

Methods inherited from class java.lang.Object

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

Constructor Detail

Proofs

public Proofs()

Construct an empty proof.

Proofs

public Proofs(Lemma l)

Construct a proof from a lemma

Proofs

public Proofs(Theorem t)

Construct a proof from a theorem

Method Detail

clone

public java.lang.Object clone()

Clones a proof.

Returns:

the cloned proof

getThl

public TheoremList getThl()

Returns the list of theorems.

getLocHyp

public java.util.Enumeration getLocHyp()

Returns the hypothesis

finalize

public void finalize(IJml2bConfiguration config,
                     Formula param,
                     Expression invStaticFinalFields,
                     Formula hyp,
                     Formula req,
                     java.lang.String name,
                     ColoredInfo b,
                     ColoredInfo method)
              throws Jml2bException,
                     PogException

Finalize the proof obligations by

• adding the parameters typing in hypothesis
• adding the invariant coming from the final static field initialization in hypothesis
• adding the invariant in hypothesis
• adding the requires of the current method in hypothesis
• assigning a name

Parameters:

param - the Formula corresponding to parameters declaration (may be null)

invStaticFinalFields - the Expression corresponding to the final static fields initialization (may be null)

hyp - the Formula corresponding to the invariant (may be null)

name - prefix for the PO of this proof (used to generate the Atelier B files)

b - the ColoredInfo associated to the requires clause.

Throws:

Jml2bException

PogException

sub

public Proofs sub(Substitution s)

Apply a substitution to the content of the proof. the substitution is applied on the hypothesis and on the theorems.

Parameters:

s - substitution to apply.

Returns:

the current proof substituted.

suppressSpecialOld

public Proofs suppressSpecialOld(int token)

Suppress the Called Old expressions in the proof.

Returns:

the current proof when the Called Old have been suppressed.

renameParam

public Proofs renameParam(IAParameters signature,
                          java.util.Vector newSignature)

Rename the fields belonging to the parameter list with new names. When calling a method, its formal parameter should be renamed in the specification of this method before to be substitued with the calling parameter (via a WP calculus on parameters) in manner to avoid conflits with current names. In the example below, the parameter a of the method m2 is renamed when the call is performed in manner to avoid to replace a with 1 in all the proof.

 //@ ensures \result == 1;
 int m1() {
    int a = 0;
    m2(1);
    return a++;
 }
 //@ requires a == 0;
 int m2(int a) {
    ...
 }
 

Parameters:

signature - the signature of the called method

newSignature - the list of new names

Returns:

the current proof renamed

param

public Proofs param(IJml2bConfiguration config,
                    java.util.Vector signature,
                    Expression param,
                    ExceptionalBehaviourStack exceptionalBehaviour)
             throws Jml2bException,
                    PogException

Renames the formal parameter of a called method by the calling parameters. Calling parameters are evaluated (through the WP calculus) and the result of this evaluation is substituted to the formal parameter.

Parameters:

signature - signature of the current method.

param - expression corresponding to the calling parameters (may be null)

exceptionalBehaviour - exceptional behaviours to prove if the parameter evaluation throws an exception

Returns:

the current proof renamed.

Throws:

Jml2bException

PogException

quantify

public Proofs quantify(java.lang.String var,
                       Type type,
                       ColoredInfo b)

Quantifies the proof whith a variable.

Parameters:

var - the quantified variable

type - the type of the quantified variable

b - ColoredInfo associated to the added hypothesis

Returns:

the current proof with a new hypothesis corresponding to the variable declation

quantify

public Proofs quantify(java.lang.String var,
                       Formula type)

Quantifies the proof whith a variable.

Parameters:

var - the quantified variable

type - the type of the quantified variable

Returns:

the current proof with a new hypothesis corresponding to the variable declation

quantify

public Proofs quantify(java.lang.String var,
                       Formula type,
                       ColoredInfo b)

Quantifies the proof whith a variable.

Parameters:

var - the quantified variable

type - the type of the quantified variable

b - ColoredInfo associated to the added hypothesis

Returns:

the current proof with a new hypothesis corresponding to the variable declation

quantify

public Proofs quantify(Formula var,
                       Formula type)

quantify

public Proofs quantify(Formula var,
                       Formula type,
                       ColoredInfo b)

Quantifies the proof whith a variable.

Parameters:

var - the quantified variable

type - the type of the quantified variable

b - ColoredInfo associated to the added hypothesis

Returns:

the current proof with a new hypothesis corresponding to the variable declation

addHyp

public void addHyp(SimpleLemma sl,
                   byte origin)

Adds the goals of a lemme to the hypothesis.

Parameters:

sl - Lemme that contains the goals that are added in hypothesis

origin - Origin of the new hypothesis

addHyp

public void addHyp(Formula f,
                   ColoredInfo b,
                   byte origin)

Adds new hypothesis.

Parameters:

f - Formula added in hypothese. When the formula is a conjonction, each conjective formula is added separetly

b - ColoredInfo associated to the added hypothesis

origin - Origin of the new hypothesis

addHyp

public void addHyp(Formula f,
                   java.util.Vector b,
                   byte origin)

Adds new hypothesis.

Parameters:

f - Formula added in hypothese. When the formula is a conjonction, each conjective formula is added separetly

b - ColoredInfo associated to the added hypothesis

origin - Origin of the new hypothesis

addHyp

public void addHyp(Formula f)

Adds new local hypothesis with no associated colored info.

Parameters:

f - Formula added in hypothese. When the formula is a conjonction, each conjective formula is added separetly

addAll

public void addAll(Proofs l)

Concats two proofs. This means that

• the hypothesis of the two proofs are merged without doublon
• the theorems lists are concatened

Parameters:

l - the proof that is concatened with the current proof.

gc

public void gc(IJml2bConfiguration config,
               boolean force)

Tries to suppress obvious goals, lemmas, theorems. The suppression is performed if the parameter is true or if memory criteria are overpassed.

Parameters:

force - true if the suppression should be forced.

isUsed

public boolean isUsed(VirtualFormula vf)

Test wheter an hypothesis is used in the theorems.

Parameters:

vf - the tested hypothese.

Returns:

true if the hypothese is pointed by a theorem false otherwise.

nbPo

public int nbPo()

Returns the number of goals (or proof obligations).

Returns:

the number of goals of the theorem list

nbTheorems

public int nbTheorems()

nbLemmas

public int nbLemmas()

nbPoChecked

public int nbPoChecked()

getLemma

public SimpleLemma getLemma(int i)

getTheorem

public Theorem getTheorem(int i)

nbPoProved

public int nbPoProved(java.lang.String prover)

Returns the number of goals that are in a specified state.

Returns:

the number of goals of the theorem list which have a state equals to the paremeter.

nbPoProved

public int nbPoProved()

Returns the number of goals that are in a specified state.

Returns:

the number of goals of the theorem list which have a state equals to the paremeter.

addBox

public Proofs addBox(ColoredInfo b)

Adds a colored info to the theorems.

Parameters:

b - : added colored info

Returns:

the current proof with a new colored info

findUsedLocHyp

public java.util.Vector findUsedLocHyp()

getLocFlow

public java.util.Vector getLocFlow()

mergeWith

public void mergeWith(Proofs jf)

Merge two proofs.

Parameters:

jf - proofs merged with the current one

Throws:

MergeException

proveObvious

public void proveObvious(boolean prove,
                         boolean atTheEnd)

Proves the obvious goals if asked. Cast all the remaining lemmas in SimpleLemma if asked. This task is performed during the WP calculus in order to avoid memory overflow and at the end.

Parameters:

prove - indicate whether obvious goals should be suppressed from the theorems

atTheEnd - indicate whether lemmas should be casted in simple lemma

garbageIdent

public void garbageIdent()

Annotates all the fields that appear in the theorem to declare them in the Atelier B files.

selectLabel

public Proofs selectLabel(java.util.Vector labels)
                   throws WrongLabelException

Selects in the lemmas corresponding to behaviours, the cases corresponding to labels.

Parameters:

labels - set of labels that have to be selected

Returns:

the current proof with some case that have be eliminated

Throws:

WrongLabelException - if a behaviour does not contain any remaining case after the selection.

getFields

public void getFields(java.util.Set fields)

Collect the fields present in the current proof obligation.

Parameters:

fields -

saveThl

public void saveThl(IJml2bConfiguration config,
                    JpoOutputStream s,
                    JmlFile jf)
             throws java.io.IOException

Throws:

java.io.IOException

save

public void save(IJml2bConfiguration config,
                 JpoOutputStream s,
                 JmlFile jf)
          throws java.io.IOException

Saves the proof in the a .jpo file

Parameters:

s - output stream for the jpo file

jf - current JmlFile

Throws:

java.io.IOException

See Also:

VirtualFormula#save(DataOutputStream, int, JmlFile), Theorem#save(DataOutputStream, JmlFile)