jml2b.pog.lemma
Class GoalOrigin

java.lang.Object
  jml2b.pog.lemma.GoalOrigin

public class GoalOrigin

extends java.lang.Object

This class describes the origin of a goal.

Author:

L. Burdy

Field Summary

static byte	ASSERT Goal origin value that corresponds to the proof of an assertion.
static byte	BLOCK_ENSURES Goal origin value that corresponds to the proof of an ensures clause of a specified block.
static byte	BLOCK_EXSURES Goal origin value that corresponds to the proof of an exsures clause of a specified block.
static byte	BLOCK_REQUIRES Goal origin value that corresponds to the proof of a requires clause of a specified block.
static byte	ENSURES Goal origin value that corresponds to the proof of an ensures clause.
static byte	EXSURES Goal origin value that corresponds to the proof of an exsures clause.
static byte	INSTANCE_CONSTRAINT
static byte	LOOP_EXSURES Goal origin value that corresponds to the proof of an exsures clause of a loop.
static byte	LOOP_INVARIANT_INIT Goal origin value that corresponds to the proof of the initialization of a loop invariant.
static byte	LOOP_INVARIANT_PRESERVE Goal origin value that corresponds to the proof of the preservation of a loop invariant.
static byte	LOOP_VARIANT Goal origin value that corresponds to the proof of a loop variant.
static byte	MEMBER_INVARIANT Goal origin value that corresponds to the proof of a non static invariant.
static byte	MODIFIES Goal origin value that corresponds to the proof of a modifies clause.
static byte	REQUIRES Goal origin value that corresponds to the proof of a requires clause.
static byte	STATIC_CONSTRAINT
static byte	STATIC_INVARIANT Goal origin value that corresponds to the proof of a static invariant.
static byte	SUPER_REQUIRES Goal origin value that corresponds to the proof of the requires clause of the super method.
static byte	WELL_DEFINED

Constructor Summary

GoalOrigin(byte origin)
Constructs a goal origin with no comment

GoalOrigin(byte origin, AField f)
Constructs a goal origin for a modifies

GoalOrigin(byte origin, AMethod m)
Constructs a goal origin for a requires

GoalOrigin(JpoInputStream s)
Constructs a goal origin from a loaded .jpo file

Method Summary

static java.lang.String	getGoalTypeString(byte type, java.lang.String comment) Returns a string describing the goal origin.
static int	getMaxGoalType() Returns the number of goal origin types.
byte	getOrigin() Returns the origin of the goal.
void	save(JpoOutputStream s) Saves the goal origin in a .jpo file

Methods inherited from class java.lang.Object

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

Field Detail

STATIC_INVARIANT

public static final byte STATIC_INVARIANT

Goal origin value that corresponds to the proof of a static invariant.

See Also:

Constant Field Values

MEMBER_INVARIANT

public static final byte MEMBER_INVARIANT

Goal origin value that corresponds to the proof of a non static invariant.

See Also:

Constant Field Values

ENSURES

public static final byte ENSURES

Goal origin value that corresponds to the proof of an ensures clause.

See Also:

Constant Field Values

REQUIRES

public static final byte REQUIRES

Goal origin value that corresponds to the proof of a requires clause.

See Also:

Constant Field Values

LOOP_INVARIANT_INIT

public static final byte LOOP_INVARIANT_INIT

Goal origin value that corresponds to the proof of the initialization of a loop invariant.

See Also:

Constant Field Values

EXSURES

public static final byte EXSURES

Goal origin value that corresponds to the proof of an exsures clause.

See Also:

Constant Field Values

LOOP_EXSURES

public static final byte LOOP_EXSURES

Goal origin value that corresponds to the proof of an exsures clause of a loop.

See Also:

Constant Field Values

MODIFIES

public static final byte MODIFIES

Goal origin value that corresponds to the proof of a modifies clause.

See Also:

Constant Field Values

SUPER_REQUIRES

public static final byte SUPER_REQUIRES

Goal origin value that corresponds to the proof of the requires clause of the super method.

See Also:

Constant Field Values

ASSERT

public static final byte ASSERT

Goal origin value that corresponds to the proof of an assertion.

See Also:

Constant Field Values

BLOCK_REQUIRES

public static final byte BLOCK_REQUIRES

Goal origin value that corresponds to the proof of a requires clause of a specified block.

See Also:

Constant Field Values

BLOCK_EXSURES

public static final byte BLOCK_EXSURES

Goal origin value that corresponds to the proof of an exsures clause of a specified block.

See Also:

Constant Field Values

BLOCK_ENSURES

public static final byte BLOCK_ENSURES

Goal origin value that corresponds to the proof of an ensures clause of a specified block.

See Also:

Constant Field Values

LOOP_VARIANT

public static final byte LOOP_VARIANT

Goal origin value that corresponds to the proof of a loop variant.

See Also:

Constant Field Values

WELL_DEFINED

public static final byte WELL_DEFINED

See Also:

Constant Field Values

STATIC_CONSTRAINT

public static final byte STATIC_CONSTRAINT

See Also:

Constant Field Values

INSTANCE_CONSTRAINT

public static final byte INSTANCE_CONSTRAINT

See Also:

Constant Field Values

LOOP_INVARIANT_PRESERVE

public static final byte LOOP_INVARIANT_PRESERVE

Goal origin value that corresponds to the proof of the preservation of a loop invariant.

See Also:

Constant Field Values

Constructor Detail

GoalOrigin

public GoalOrigin(JpoInputStream s)
           throws java.io.IOException,
                  LoadException

Constructs a goal origin from a loaded .jpo file

Parameters:

s - The input stream corresponding to the jpo file

GoalOrigin

public GoalOrigin(byte origin,
                  AField f)

Constructs a goal origin for a modifies

Parameters:

origin - The origin

f - The modified field

GoalOrigin

public GoalOrigin(byte origin,
                  AMethod m)

Constructs a goal origin for a requires

Parameters:

origin - The origin

m - The called method

GoalOrigin

public GoalOrigin(byte origin)

Constructs a goal origin with no comment

Parameters:

origin - The origin

Method Detail

getMaxGoalType

public static int getMaxGoalType()

Returns the number of goal origin types.

Returns:

MAXGOALTYPE

getGoalTypeString

public static java.lang.String getGoalTypeString(byte type,
                                                 java.lang.String comment)

Returns a string describing the goal origin.

Parameters:

type - The goal origin

comment - The comment associated with the origin

Returns:

a string to be displayed in manner to give informations about the goal origin.

save

public void save(JpoOutputStream s)
          throws java.io.IOException

Saves the goal origin in a .jpo file

Parameters:

s - The ouput stream representing the jpo file.

Throws:

java.io.IOException

getOrigin

public byte getOrigin()

Returns the origin of the goal.

Returns:

origin