public class OracleGenerator
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
PRE_STRING |
Constructor and Description |
---|
OracleGenerator(Services services,
ReflectionClassCreator rflCreator,
boolean useRFL) |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
generateMethodName() |
OracleTerm |
generateOracle(Term term,
boolean initialSelect) |
OracleMethod |
generateOracleMethod(Term term) |
java.util.Set<Term> |
getConstants() |
java.util.List<OracleVariable> |
getMethodArgs() |
OracleLocationSet |
getOracleLocationSet(Term modifierset) |
java.util.Set<OracleMethod> |
getOracleMethods() |
java.util.Set<java.lang.String> |
getPrestateTerms() |
public static final java.lang.String PRE_STRING
public OracleGenerator(Services services, ReflectionClassCreator rflCreator, boolean useRFL)
public OracleMethod generateOracleMethod(Term term)
public OracleLocationSet getOracleLocationSet(Term modifierset)
public java.util.List<OracleVariable> getMethodArgs()
public java.util.Set<OracleMethod> getOracleMethods()
public java.util.Set<Term> getConstants()
public OracleTerm generateOracle(Term term, boolean initialSelect)
public static java.lang.String generateMethodName()
public java.util.Set<java.lang.String> getPrestateTerms()
Copyright © 2003-2019 The KeY-Project.