dk.brics.string.java
Class AssertionCreatorImpl

java.lang.Object
  dk.brics.string.java.AssertionCreatorImpl

All Implemented Interfaces:

AssertionCreator

public class AssertionCreatorImpl
extends Object
implements AssertionCreator

Constructor Summary

AssertionCreatorImpl()

Method Summary

AssertionBranches	createAssertions(IfStmt branch, AssertionContext assertionContext) Creates assertions that must hold when the if statement's condition is true and false, respectively.
AssertionBranch	createSwitchAssertions(ValueBox variable, int value, Unit switchStart, AssertionContext assertionContext) Creates assertions that must hold when a switch statement branches to the specified case block.
AssertionBranch	createSwitchDefaultAssertions(ValueBox variable, List<Integer> skippedValues, Unit switchStart, AssertionContext assertionContext) Creates assertions that must hold when a switch statement branches to the default block.

Methods inherited from class java.lang.Object

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

Constructor Detail

AssertionCreatorImpl

public AssertionCreatorImpl()

Method Detail

createAssertions

public AssertionBranches createAssertions(IfStmt branch,
                                          AssertionContext assertionContext)

Description copied from interface: AssertionCreator

Creates assertions that must hold when the if statement's condition is true and false, respectively. The assertions should be added to the intermediate factory using its addStatement method.

Specified by:

createAssertions in interface AssertionCreator

assertionContext - the ACME Assertion Creation Kit™ toolbox of useful stuff!

Returns:

assertions for when the condition is true or false, respectively

createSwitchAssertions

public AssertionBranch createSwitchAssertions(ValueBox variable,
                                              int value,
                                              Unit switchStart,
                                              AssertionContext assertionContext)

Description copied from interface: AssertionCreator

Creates assertions that must hold when a switch statement branches to the specified case block.

Fall-through from another case block should not be taken into account. The assertions may assume that this particular case was chosen first-hand.

Specified by:

createSwitchAssertions in interface AssertionCreator

Parameters:

variable - the expression x as used in switch(x) {...}.

value - the y as used in case y: ...

switchStart - the start of the switch statement

assertionContext - see AssertionContext

Returns:

assertions that hold when this particular switch case is chosen

createSwitchDefaultAssertions

public AssertionBranch createSwitchDefaultAssertions(ValueBox variable,
                                                     List<Integer> skippedValues,
                                                     Unit switchStart,
                                                     AssertionContext assertionContext)

Description copied from interface: AssertionCreator

Creates assertions that must hold when a switch statement branches to the default block.

Fall-through from a case block should not be taken into account. The assertions may assume that none of the case blocks were executed.

Specified by:

createSwitchDefaultAssertions in interface AssertionCreator

Parameters:

variable - the expression x as used in switch(x) {...}.

skippedValues - a list with all the case values in the switch

switchStart - the start of the switch statement

assertionContext - see AssertionContext

Returns:

assertions that hold when the default case is chosen