A B C D E F G H I J K L M N O P Q R S T U V W Z

W

WAITING - Static variable in class jack.plugin.prove.ProofTask

Constant corresponding to the waiting state.

WELL_DEFINED - Static variable in class jml2b.pog.lemma.GoalOrigin

WHITE - Static variable in class jack.plugin.edit.JavaLineStyler

WORD - Static variable in class jack.plugin.edit.JavaLineStyler

WellDefInvProofs - class jpov.structure.WellDefInvProofs.

WellDefinedInvPO - class jml2b.pog.proofobligation.WellDefinedInvPO.

WellDefinedInvPO(IJml2bConfiguration, Class, Enumeration) - Constructor for class jml2b.pog.proofobligation.WellDefinedInvPO

WellDefinedMethodProofs - class jpov.structure.WellDefinedMethodProofs.

WellDefinedSpecPO - class jml2b.pog.proofobligation.WellDefinedSpecPO.

WellDefinedSpecPO(IJml2bConfiguration, Class, Method) - Constructor for class jml2b.pog.proofobligation.WellDefinedSpecPO

WithTypeExp - class jml2b.structure.statement.WithTypeExp.

This class implements expression with type, that is object and array creation, casting and instanceof.

WrongLabelException - exception jml2b.exceptions.WrongLabelException.

This class defines an exception that is thrown when a wrong label configuration is met, that is when after restricting possible lemma to labels, no lemmas remain.

WrongLabelException() - Constructor for class jml2b.exceptions.WrongLabelException

warning(JmlFile, int, int, String) - Static method in class jml2b.exceptions.ErrorHandler

Indicates an error in the specified file, line and column.

wellDefInvLemmas - Variable in class jml2b.structure.java.Class

wellDefinednessLemmas - Variable in class jml2b.structure.java.Method

wp(IJml2bConfiguration, String, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.ArrayInitializer

wp(IJml2bConfiguration, String, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.BinaryExp

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.Expression

wp(IJml2bConfiguration, String, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.Expression

Returns the proofs resulting where the WP calculus apply on this expression.

wp(IJml2bConfiguration, String, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.IsSubtypeOfExp

wp(IJml2bConfiguration, String, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.MethodCallExp

wp(IJml2bConfiguration, String, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.QuantifiedExp

wp(IJml2bConfiguration, String, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.QuestionExp

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StAssert

Adds the asserted predicate in hypothesis of the current normal behaviour proof and adds a new proof corresponding to the proof of the assertion.

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StBlock

Applies the encapsulated statement on the current proof context.

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StControlFlowBreak

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StDoWhile

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StFor

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StIf

Calculates the proof corresponding to each branch and guard each of them by the fact that the condition is respectively true or false.

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StImplementsLabel

Selects in the lemmas corresponding to normal behaviour, the cases corresponding to the set of implemented labels.

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StLabel

If the encapsulated statement is a loop, the finishOnContinueLab proofs is changed during its evaluation.

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StSequence

Calculates the second statement on the proof context and then the first with the resulting proof as normal behaviour.

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StSkip

Returns the normal behaviour, till skip has no effect.

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StSpecBlock

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StSwitch

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StTry

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.StVarDecl

wp(IJml2bConfiguration, Proofs, Proofs, LabeledProofsVector, LabeledProofsVector, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.Statement

Returns the proofs resulting where the WP calculus apply on this statement.

wp(IJml2bConfiguration, String, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.TTypeExp

Substitute in the normal behaviour proof the resulting temporary variable with the type.

wp(IJml2bConfiguration, String, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.TerminalExp

Returns the normal behaviour proof where the resulting variable has been substituted with the current expression.

wp(IJml2bConfiguration, String, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.UnaryExp

wp(IJml2bConfiguration, String, Proofs, ExceptionalBehaviourStack) - Method in class jml2b.structure.statement.WithTypeExp

write(byte[], int, int) - Method in class jml2b.util.JpoOutputStream

write(int) - Method in class jml2b.util.JpoOutputStream

write(byte[]) - Method in class jml2b.util.JpoOutputStream

writeBoolean(boolean) - Method in interface jml2b.util.IOutputStream

writeBoolean(boolean) - Method in class jml2b.util.JpoOutputStream

writeByte(int) - Method in interface jml2b.util.IOutputStream

writeByte(int) - Method in class jml2b.util.JpoOutputStream

writeBytes(String) - Method in class jml2b.util.JpoOutputStream

writeChar(int) - Method in class jml2b.util.JpoOutputStream

writeChars(String) - Method in class jml2b.util.JpoOutputStream

writeDouble(double) - Method in class jml2b.util.JpoOutputStream

writeFloat(float) - Method in class jml2b.util.JpoOutputStream

writeInt(int) - Method in interface jml2b.util.IOutputStream

writeInt(int) - Method in class jml2b.util.JpoOutputStream

writeLong(long) - Method in class jml2b.util.JpoOutputStream

writeShort(int) - Method in class jml2b.util.JpoOutputStream

writeUTF(String) - Method in interface jml2b.util.IOutputStream

writeUTF(String) - Method in class jml2b.util.JpoOutputStream