jml2b.pog.lemma
Class NormalLemma

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.lemma.Lemma
          jml2b.pog.lemma.BehaviourLemma
              jml2b.pog.lemma.NormalLemma

All Implemented Interfaces:

IFormToken, ILemma

public class NormalLemma

extends jml2b.pog.lemma.BehaviourLemma

This class defines lemmas resulting from the proof of a normal method specification. ensuresLemmas is a set of EnsuresLabelledLemma

Author:

L. Burdy

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

NormalLemma(IJml2bConfiguration config, Method m, SimpleLemma l, SimpleLemma sc, SimpleLemma ic, java.util.Vector fields)
Creates a set of ensures labelled lemma corresponding to the cases of a method specification corresponding to normal behaviours.

Method Summary

Lemma	catchException(Type type, Field catchParam) Creates an exceptional lemma set from the current one and a catched type with a catched parameter.
java.lang.Object	clone() Clones a lemma.
void	garbageIdent() Annotates all the fields that appear in the lemma to declare them in the Atelier B files.
void	getFields(java.util.Set fields)
void	oldParam(java.util.Vector enum) Adds a old param around the element of the enumeration corresponding to the parameter of the method.
boolean	proveObvious(java.util.Vector hyp, boolean atTheEnd) Supress in the lemma the obvious goals.
void	selectLabel(java.util.Vector labels) Selects in the labelled lemmas, the cases corresponding to labels.
void	sub(Substitution s) Apply a substitution to the lemma.
void	suppressSpecialOld(int token) Suppress the Called Old expressions.

Methods inherited from class jml2b.pog.lemma.Lemma

catches, getTypesException, nbPo, nbPoChecked, nbPoProved, nbPoProved, throwException, throwException

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

NormalLemma

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

Creates a set of ensures labelled lemma corresponding to the cases of a method specification corresponding to normal behaviours.

Parameters:

m - The analyzed method

l - The current invariant

fields - The set of modifiable fields

Method Detail

clone

public java.lang.Object clone()

Description copied from class: Lemma

Clones a lemma.

Specified by:

clone in class Lemma

Returns:

the cloned lemma

catchException

public Lemma catchException(Type type,
                            Field catchParam)

Creates an exceptional lemma set from the current one and a catched type with a catched parameter.

Overrides:

catchException in class Lemma

Parameters:

type - The catched type

catchParam - The catched parameter

Returns:

a ExceptionalLemma that corresponds to the current lemma encapsulated in a catched exception.

getFields

public void getFields(java.util.Set fields)

Specified by:

getFields in class Lemma

proveObvious

public final boolean proveObvious(java.util.Vector hyp,
                                  boolean atTheEnd)

Description copied from interface: ILemma

Supress in the lemma the obvious goals.

Returns:

true if the lemma contains only obvious goals, false otherwise.

See Also:

Proofs.proveObvious(boolean, boolean)

garbageIdent

public final void garbageIdent()

Description copied from interface: ILemma

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

See Also:

Theorem#garbageIdent()

oldParam

public final void oldParam(java.util.Vector enum)

Description copied from interface: ILemma

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

Parameters:

enum - fields enumeration

See Also:

Theorem#oldParam(Enumeration)

sub

public final void sub(Substitution s)

Description copied from interface: ILemma

Apply a substitution to the lemma.

Parameters:

s - substitution to apply.

See Also:

Proofs.sub(Substitution)

suppressSpecialOld

public final void suppressSpecialOld(int token)

Description copied from interface: ILemma

Suppress the Called Old expressions.

See Also:

Theorem#suppressCalledOld()

selectLabel

public final void selectLabel(java.util.Vector labels)
                       throws WrongLabelException

Description copied from class: Lemma

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

Specified by:

selectLabel in class Lemma

Parameters:

labels - set of labels that have to be selected

Throws:

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