jml2b.pog.lemma
Class VirtualFormula

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

All Implemented Interfaces:

java.io.Serializable

public class VirtualFormula

extends Profiler

implements java.io.Serializable

This class implements a formula with its set of colored informations.

Author:

L. Burdy

See Also:

Serialized Form

Field Summary

static byte	ASSERT Formula origin corresponding to an assertion
static byte	BLOCK_ENSURES Formula origin corresponding to an ensures clause of a specified block
static byte	BLOCK_EXSURES Formula origin corresponding to an exsures clause of a specified block
static byte	ENSURES Formula origin corresponding to an ensures clause of a called method
static byte	EXSURES Formula origin corresponding to an exsures clause of a called method
static byte	GOAL Formula origin corresponding to a goal
static byte	INVARIANT Formula origin corresponding to an invariant
static byte	LOCALES Formula origin corresponding to a local hypothese
static byte	LOOP_EXSURES Formula origin corresponding to a loop exsures
static byte	LOOP_INVARIANT Formula origin corresponding to a loop invariant
static byte	REQUIRES Formula origin corresponding to a require clause
static byte	STATIC_FINAL_FIELDS_INVARIANT Formula origin corresponding to a static final field initialization

Constructor Summary

VirtualFormula()

VirtualFormula(byte origin, Formula f, ColoredInfo b)
Constructs a virtual formula

VirtualFormula(byte origin, Formula f, java.util.Vector b)
Constructs a virtual formula

Method Summary

Formula	getFormula() Returns the formula
static java.lang.String	getHypTypeString(byte type) Returns the string corresponding to an hypothesis type
int	getIndex() Returns the index of the formula
static int	getMaxHypType() Returns the number of hypothese type
byte	getOrigin() Returns the origin.
boolean	getsFlow(byte b)
void	save(IJml2bConfiguration config, JpoOutputStream s, int index, JmlFile jf) Saves the virtual formula into a .jpo file
void	setOrigin(byte origin) Sets the origin.

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

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

Field Detail

REQUIRES

public static final byte REQUIRES

Formula origin corresponding to a require clause

See Also:

Constant Field Values

LOCALES

public static final byte LOCALES

Formula origin corresponding to a local hypothese

See Also:

Constant Field Values

ASSERT

public static final byte ASSERT

Formula origin corresponding to an assertion

See Also:

Constant Field Values

ENSURES

public static final byte ENSURES

Formula origin corresponding to an ensures clause of a called method

See Also:

Constant Field Values

EXSURES

public static final byte EXSURES

Formula origin corresponding to an exsures clause of a called method

See Also:

Constant Field Values

LOOP_INVARIANT

public static final byte LOOP_INVARIANT

Formula origin corresponding to a loop invariant

See Also:

Constant Field Values

LOOP_EXSURES

public static final byte LOOP_EXSURES

Formula origin corresponding to a loop exsures

See Also:

Constant Field Values

BLOCK_ENSURES

public static final byte BLOCK_ENSURES

Formula origin corresponding to an ensures clause of a specified block

See Also:

Constant Field Values

BLOCK_EXSURES

public static final byte BLOCK_EXSURES

Formula origin corresponding to an exsures clause of a specified block

See Also:

Constant Field Values

INVARIANT

public static final byte INVARIANT

Formula origin corresponding to an invariant

See Also:

Constant Field Values

STATIC_FINAL_FIELDS_INVARIANT

public static final byte STATIC_FINAL_FIELDS_INVARIANT

Formula origin corresponding to a static final field initialization

See Also:

Constant Field Values

GOAL

public static final byte GOAL

Formula origin corresponding to a goal

See Also:

Constant Field Values

Constructor Detail

VirtualFormula

public VirtualFormula()

VirtualFormula

public VirtualFormula(byte origin,
                      Formula f,
                      ColoredInfo b)

Constructs a virtual formula

Parameters:

origin - The origin

f - The formula

b - The associated colored information

VirtualFormula

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

Constructs a virtual formula

Parameters:

origin - The origin

f - The formula

b - The associated set of colored informations

Method Detail

getMaxHypType

public static int getMaxHypType()

Returns the number of hypothese type

getHypTypeString

public static java.lang.String getHypTypeString(byte type)

Returns the string corresponding to an hypothesis type

Parameters:

type - The hypothesis type

Returns:

The string to display

getFormula

public Formula getFormula()

Returns the formula

Returns:

f

getIndex

public int getIndex()

Returns the index of the formula

Returns:

index

save

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

Saves the virtual formula into a .jpo file

Parameters:

s - The ouput stream corresponding to the jpo file

index - The index of the formula into the hypothesis array

jf - The current JML file

Throws:

java.io.IOException

getOrigin

public byte getOrigin()

Returns the origin.

Returns:

origin

setOrigin

public void setOrigin(byte origin)

Sets the origin.

Parameters:

origin - The origin to set

getsFlow

public boolean getsFlow(byte b)