dk.brics.string.java
Interface AssertionCreator

All Known Implementing Classes:

AssertionCreatorImpl

public interface AssertionCreator

Analyzes the conditions of if and switch statements and produces corresponding assertion statement for the intermediate program.

Author:

Asger

Method Summary

AssertionBranches	createAssertions(IfStmt branch, AssertionContext context) 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 context) 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 context) Creates assertions that must hold when a switch statement branches to the default block.

Method Detail

createAssertions

AssertionBranches createAssertions(IfStmt branch,
                                   AssertionContext context)

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.

Parameters:

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

Returns:

assertions for when the condition is true or false, respectively

createSwitchAssertions

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

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.

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

context - see AssertionContext

Returns:

assertions that hold when this particular switch case is chosen

createSwitchDefaultAssertions

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

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.

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

context - see AssertionContext

Returns:

assertions that hold when the default case is chosen