de.uka.ilkd.key.informationflow.po

Class InfFlowProofSymbols

java.lang.Object

de.uka.ilkd.key.informationflow.po.InfFlowProofSymbols

public class InfFlowProofSymbols
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableSet<Pair<Function,java.lang.Boolean>>	functions
private boolean	isFreshContract
private ImmutableSet<Pair<Function,java.lang.Boolean>>	predicates
private ImmutableSet<Pair<ProgramVariable,java.lang.Boolean>>	programVariables
private ImmutableSet<Pair<SchemaVariable,java.lang.Boolean>>	schemaVariables
private ImmutableSet<Pair<Sort,java.lang.Boolean>>	sorts
private ImmutableSet<Pair<Taclet,java.lang.Boolean>>	taclets

Constructor Summary

Constructors

Constructor and Description
InfFlowProofSymbols()

Method Summary

Modifier and Type	Method and Description
void	add(Named symb)
void	add(Term t)
private void	addFunc(Function f, boolean labeled)
private void	addFunction(Function f, boolean labeled)
void	addLabeled(Named symb)
void	addLabeled(Term t)
void	addLabeledTotalTerm(Term t)
private void	addPredicate(Function p, boolean labeled)
private void	addProgramVariable(ProgramVariable pv, boolean labeled)
private void	addSchemaVariable(SchemaVariable sv, boolean labeled)
private void	addSort(Sort s, boolean labeled)
private void	addTaclet(Taclet t, boolean labeled)
void	addTotalTerm(Term t)
private boolean	containsFunction(Function f)
private boolean	containsPredicate(Function f)
private boolean	containsProgramVariable(ProgramVariable pv)
private boolean	containsSchemaVariable(SchemaVariable sv)
private boolean	containsSort(Sort s)
private boolean	containsTaclet(Taclet t)
private java.util.LinkedList<Sort>	ensureRightOrderOfSorts(ImmutableSet<Sort> s)
private ImmutableSet<Function>	getFunctions()
private ImmutableSet<Pair<Function,java.lang.Boolean>>	getLabeledFunctions()
private ImmutableSet<Pair<Function,java.lang.Boolean>>	getLabeledPredicates()
private ImmutableSet<Pair<ProgramVariable,java.lang.Boolean>>	getLabeledProgramVariables()
private ImmutableSet<Pair<SchemaVariable,java.lang.Boolean>>	getLabeledSchemaVariables()
private ImmutableSet<Pair<Sort,java.lang.Boolean>>	getLabeledSorts()
private InfFlowProofSymbols	getLabeledSymbols()
private ImmutableSet<Pair<Taclet,java.lang.Boolean>>	getLabeledTaclets()
private ImmutableSet<Function>	getPredicates()
private ImmutableSet<ProgramVariable>	getProgramVariables()
private ImmutableSet<SchemaVariable>	getSchemaVariables()
private ImmutableSet<Sort>	getSorts()
private ImmutableSet<Taclet>	getTaclets()
boolean	isFreshContract()
private boolean	isPredicate(Operator f)
private java.lang.String	printFunctions()
private java.lang.String	printPredicates()
private java.lang.String	printProgramVariables()
java.lang.String	printProofSymbols()
private java.lang.String	printSchemaVariables()
private java.lang.String	printSorts()
private java.lang.String	printSpace()
private java.lang.String	printTaclets()
private java.util.LinkedList<Sort>	removeArraySorts(java.util.LinkedList<Sort> sorts)
static ProgramVariable	searchPV(java.lang.String s, Services services)
InfFlowProofSymbols	union(InfFlowProofSymbols symbols)
InfFlowProofSymbols	unionLabeled(InfFlowProofSymbols symbols)
void	useProofSymbols()

Methods inherited from class java.lang.Object

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

Field Detail

isFreshContract

private boolean isFreshContract

sorts

private ImmutableSet<Pair<Sort,java.lang.Boolean>> sorts

predicates

private ImmutableSet<Pair<Function,java.lang.Boolean>> predicates

functions

private ImmutableSet<Pair<Function,java.lang.Boolean>> functions

programVariables

private ImmutableSet<Pair<ProgramVariable,java.lang.Boolean>> programVariables

schemaVariables

private ImmutableSet<Pair<SchemaVariable,java.lang.Boolean>> schemaVariables

taclets

private ImmutableSet<Pair<Taclet,java.lang.Boolean>> taclets

Constructor Detail

InfFlowProofSymbols

public InfFlowProofSymbols()

Method Detail

getLabeledSymbols

private InfFlowProofSymbols getLabeledSymbols()

getLabeledSorts

private ImmutableSet<Pair<Sort,java.lang.Boolean>> getLabeledSorts()

getLabeledPredicates

private ImmutableSet<Pair<Function,java.lang.Boolean>> getLabeledPredicates()

getLabeledFunctions

private ImmutableSet<Pair<Function,java.lang.Boolean>> getLabeledFunctions()

getLabeledProgramVariables

private ImmutableSet<Pair<ProgramVariable,java.lang.Boolean>> getLabeledProgramVariables()

getLabeledSchemaVariables

private ImmutableSet<Pair<SchemaVariable,java.lang.Boolean>> getLabeledSchemaVariables()

getLabeledTaclets

private ImmutableSet<Pair<Taclet,java.lang.Boolean>> getLabeledTaclets()

containsSort

private boolean containsSort(Sort s)

containsPredicate

private boolean containsPredicate(Function f)

containsFunction

private boolean containsFunction(Function f)

containsProgramVariable

private boolean containsProgramVariable(ProgramVariable pv)

containsSchemaVariable

private boolean containsSchemaVariable(SchemaVariable sv)

containsTaclet

private boolean containsTaclet(Taclet t)

addTaclet

private void addTaclet(Taclet t,
                       boolean labeled)

addSort

private void addSort(Sort s,
                     boolean labeled)

isPredicate

private boolean isPredicate(Operator f)

addPredicate

private void addPredicate(Function p,
                          boolean labeled)

addFunction

private void addFunction(Function f,
                         boolean labeled)

addFunc

private void addFunc(Function f,
                     boolean labeled)

addSchemaVariable

private void addSchemaVariable(SchemaVariable sv,
                               boolean labeled)

addProgramVariable

private void addProgramVariable(ProgramVariable pv,
                                boolean labeled)

useProofSymbols

public void useProofSymbols()

isFreshContract

public boolean isFreshContract()

searchPV

public static ProgramVariable searchPV(java.lang.String s,
                                       Services services)

add

public void add(Named symb)

addLabeled

public void addLabeled(Named symb)

add

public void add(Term t)

addLabeled

public void addLabeled(Term t)

union

public InfFlowProofSymbols union(InfFlowProofSymbols symbols)

unionLabeled

public InfFlowProofSymbols unionLabeled(InfFlowProofSymbols symbols)

addTotalTerm

public void addTotalTerm(Term t)

addLabeledTotalTerm

public void addLabeledTotalTerm(Term t)

getSorts

private ImmutableSet<Sort> getSorts()

ensureRightOrderOfSorts

private java.util.LinkedList<Sort> ensureRightOrderOfSorts(ImmutableSet<Sort> s)

removeArraySorts

private java.util.LinkedList<Sort> removeArraySorts(java.util.LinkedList<Sort> sorts)

getPredicates

private ImmutableSet<Function> getPredicates()

getFunctions

private ImmutableSet<Function> getFunctions()

getProgramVariables

private ImmutableSet<ProgramVariable> getProgramVariables()

getSchemaVariables

private ImmutableSet<SchemaVariable> getSchemaVariables()

getTaclets

private ImmutableSet<Taclet> getTaclets()

printSpace

private java.lang.String printSpace()

printSorts

private java.lang.String printSorts()

printPredicates

private java.lang.String printPredicates()

printFunctions

private java.lang.String printFunctions()

printProgramVariables

private java.lang.String printProgramVariables()

printSchemaVariables

private java.lang.String printSchemaVariables()

printTaclets

private java.lang.String printTaclets()

printProofSymbols

public java.lang.String printProofSymbols()