jml2b.pog.lemma
Class Theorem

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.lemma.Theorem

All Implemented Interfaces:

IFormToken, jml.JmlDeclParserTokenTypes, MyToken

public class Theorem

extends Profiler

implements jml.JmlDeclParserTokenTypes, MyToken, IFormToken

This class describes a theorem. A theorem is a set of hypothesis and a set of lemmas corresponding to goals.

Author:

L. Burdy

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.structure.statement.MyToken

BTRUE, FIRST_TOKEN, METHOD_CALL, NEWARRAY, nodeString, SEQUENCE, SKIP, T_CALLED_OLD, T_FRESH_CALLED_OLD, T_VARIANT_OLD

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

Theorem()
Construct an empty theorem.

Theorem(IJml2bConfiguration config, java.util.Enumeration e, Expression b, GoalOrigin origin)
Construct a theorem from an enumeration of Exsures.

Theorem(IJml2bConfiguration config, Method m, SimpleLemma l, SimpleLemma sc, SimpleLemma ic, java.util.Vector fields)
Construct a theorem from a method specification corresponding to the proof of its normal behaviours.

Theorem(Lemma l)
Construct a theorem containing one lemma

Method Summary

java.lang.Object	clone() Clone the theorem
java.util.Vector	getHyp() Returns the hypothesis
java.lang.String	getName() Returns the name of the theorem.
static Theorem	getTrue(IJml2bConfiguration config)
Proofs	impliesExceptional(ExceptionalBehaviourStack ebs) Returns the proof that an exsures proof proof implies an exceptionnal behaviour.
void	oldParam(java.util.Vector e) Adds a old param around the element of the enumeration corresponding to the parameter of the method.
Theorem	renameParam(IAParameters signature, java.util.Vector newSignature) Renames the parameter of a method with new identifier in the theorem

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

Theorem

public Theorem()

Construct an empty theorem.

Theorem

public Theorem(IJml2bConfiguration config,
               java.util.Enumeration e,
               Expression b,
               GoalOrigin origin)
        throws Jml2bException,
               PogException

Construct a theorem from an enumeration of Exsures. A ExsuresLemma is constructed for each element of the enumeration,

Parameters:

e - Exsures enumeration

b - Expression to substitued to this in the exsures clause (may be null)

origin - origin of the exsures

Theorem

public Theorem(IJml2bConfiguration config,
               Method m,
               SimpleLemma l,
               SimpleLemma sc,
               SimpleLemma ic,
               java.util.Vector fields)
        throws Jml2bException,
               PogException

Construct a theorem from a method specification corresponding to the proof of its normal behaviours.

Parameters:

m - method from which lemmas should be created

l - The current invariant

sc - The current static constraint

ic - The current instance constraint

Theorem

public Theorem(Lemma l)

Construct a theorem containing one lemma

Parameters:

l - lemma to add to the theorem

Method Detail

getTrue

public static Theorem getTrue(IJml2bConfiguration config)
                       throws PogException,
                              Jml2bException

Throws:

PogException

Jml2bException

clone

public java.lang.Object clone()

Clone the theorem

Returns:

the cloned theorem

getName

public java.lang.String getName()

Returns the name of the theorem.

Returns:

the name of the theorem

getHyp

public java.util.Vector getHyp()

Returns the hypothesis

Returns:

the enumeration of hypothesis

oldParam

public void oldParam(java.util.Vector e)

Adds a old param around the element of the enumeration corresponding to the parameter of the method.

Parameters:

e - fields enumeration

renameParam

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

Renames the parameter of a method with new identifier in the theorem

Parameters:

signature - The parameters of a method

newSignature - The set of new names

Returns:

the substituted theorem

impliesExceptional

public Proofs impliesExceptional(ExceptionalBehaviourStack ebs)

Returns the proof that an exsures proof proof implies an exceptionnal behaviour.

Parameters:

ebs - The exceptional behaviour

Returns:

the calculated proof