public final class Construct
extends java.lang.Object
Constructor and Description |
---|
Construct() |
Modifier and Type | Method and Description |
---|---|
static AndFormula |
andFormula(Expression base1,
Expression base2)
construct conjunction with components base1 and base2
|
static ApplicationExpression |
applicationExpression(Expression base1,
Expression[] base2)
construct application of base1 to base2
|
static ArrayTerm |
arrayTerm(TypedIdentifier[] variables,
Expression base)
construct array term of variables and base term
|
static ArrayType |
arrayType(Type index,
Type base)
construct array type with denoted index type and base type.
|
static AtomicType |
atomicType(java.lang.String name)
construct atomic type with denoted name.
|
static AxiomDeclaration |
axiomDeclaration(FormulaDeclIdentifier name,
Expression formula)
construct axiom declaration with denoted name and formula
|
static BitAndTerm |
bitAndTerm(Expression base1,
Expression base2)
construct bit conjunction with components base1 and base2
|
static BitLogical |
bitLogical(boolean value)
construct bit logical constant with denoted value.
|
static BitNotTerm |
bitNotTerm(Expression base)
construct negation (not term) of base term
|
static BitOrTerm |
bitOrTerm(Expression base1,
Expression base2)
construct bit disjunction with components base1 and base2
|
static DividesTerm |
dividesTerm(Expression base1,
Expression base2)
construct quotient with components base1 and base2
|
static EqualsFormula |
equalsFormula(Expression base1,
Expression base2)
construct equality with components base1 and base2
|
static EquivalentFormula |
equivalentFormula(Expression base1,
Expression base2)
construct equivalence with components base1 and base2
|
static ExistsFormula |
existsFormula(TypedIdentifier[] variables,
Expression base)
construct existentially quantifed formula of variables and base formula
|
static ForallFormula |
forallFormula(TypedIdentifier[] variables,
Expression base)
construct universally quantifed formula of variables and base formula
|
static FormulaDeclaration |
formulaDeclaration(FormulaDeclIdentifier name,
Expression formula)
construct formula declaration with denoted name and formula.
|
static FormulaDeclIdentifier |
formulaDeclIdentifier(java.lang.String name)
construct formula declaration identifier with denoted name.
|
static FunctionType |
functionType(Type[] domain,
Type range)
construct function type from types domain and range.
|
static GreaterEqualFormula |
greaterEqualFormula(Expression base1,
Expression base2)
construct greater-than-or-equal formula with components base1 and base2
|
static GreaterFormula |
greaterFormula(Expression base1,
Expression base2)
construct greater-than formula with components base1 and base2
|
static IfThenElseExpression |
ifThenElseExpression(Expression condition,
Expression thenbranch,
Expression elsebranch)
construct if-then-else expressions from condition, thenbranch, elsebranch.
|
static ImpliesFormula |
impliesFormula(Expression base1,
Expression base2)
construct implication with components base1 and base2
|
static LambdaTerm |
lambdaTerm(TypedIdentifier[] variables,
Expression base)
construct lambda term of variables and base term
|
static LessEqualFormula |
lessEqualFormula(Expression base1,
Expression base2)
construct less-than-or-equal formula with components base1 and base2
|
static LessFormula |
lessFormula(Expression base1,
Expression base2)
construct less-than formula with components base1 and base2
|
static LetExpression |
letExpression(ValueDeclaration[] declarations,
Expression base)
construct let expressions of declarations and base expressions
|
static LetType |
letType(TypeDeclaration[] declarations,
Type base)
construct let type of declarations and base type
|
static Logical |
logical(boolean value)
construct logical constant with denoted value.
|
static MinusTerm |
minusTerm(Expression base1,
Expression base2)
construct difference with components base1 and base2
|
static NegationTerm |
negationTerm(Expression base)
construct negation (minus term) of base term
|
static NotEqualsFormula |
notEqualsFormula(Expression base1,
Expression base2)
construct inequality with components base1 and base2
|
static NotEquivalentFormula |
notEquivalentFormula(Expression base1,
Expression base2)
construct exclusive disjunction with components base1 and base2
|
static NotFormula |
notFormula(Expression base)
construct negation (not formula) of base formula
|
static Number |
number(java.lang.String value)
construct number with denoted value.
|
static OrFormula |
orFormula(Expression base1,
Expression base2)
construct disjunction with components base1 and base2
|
static PlusTerm |
plusTerm(Expression base1,
Expression base2)
construct binary sum with components base1 and base2
|
static PowerTerm |
powerTerm(Expression base1,
Expression base2)
construct power term with components base1 and base2
|
static RecordTerm |
recordTerm(ValuedIdentifier[] base)
construct record term of base terms
|
static RecordType |
recordType(TypedIdentifier[] base)
construct record type with denoted base types.
|
static Reference |
reference(java.lang.String name)
construct reference with denoted name.
|
static Reference |
reference(Symbol symbol)
Construct reference from symbol.
|
static Reference |
reference(TypeDeclIdentifier ident)
construct reference from type declaration identifier.
|
static Reference |
reference(ValueDeclIdentifier ident)
construct reference from value declaration identifier.
|
static SelectionTerm |
selectionTerm(Expression base1,
Selector base2)
construct component selection from base1 and base2
|
static SelectorIdentifier |
selectorIdentifier(Reference base)
make selector from identifier base
|
static SelectorIndex |
selectorIndex(Expression base)
make selector from index expression base
|
static SelectorNumber |
selectorNumber(Number base)
make selector from number base
|
static SubrangeType |
subrangeType(Expression from,
Expression to)
construct subrangetype with denoted bounds.
|
static SubType |
subType(Expression predicate)
construct subtype with denoted predicate.
|
static TimesTerm |
timesTerm(Expression base1,
Expression base2)
construct binary product with components base1 and base2
|
static TupleTerm |
tupleTerm(Expression[] base)
construct tuple term of base terms
|
static TupleType |
tupleType(Type[] base)
construct tuple type with denoted base types.
|
static TypeDeclaration |
typeDeclaration(TypeDeclIdentifier name,
Type type)
construct type declaration with denoted name and type.
|
static TypeDeclIdentifier |
typeDeclIdentifier(java.lang.String name)
construct type declaration identifier with denoted name.
|
static TypedIdentifier |
typedIdentifier(ValueDeclIdentifier identifier,
Type type)
construct typed identifier from identifier and type.
|
static UpdateTerm |
updateTerm(Expression base1,
Selector[] base2,
Expression value)
construct component update by index selection from base, base2, and base3
|
static ValueDeclaration |
valueDeclaration(ValueDeclIdentifier name,
Type type,
Expression value)
construct value declaration with denoted name, type and value.
|
static ValueDeclIdentifier |
valueDeclIdentifier(java.lang.String name)
construct value declaration identifier with denoted name.
|
static ValuedIdentifier |
valuedIdentifier(Reference identifier,
Expression value)
construct identifier with value from identifier and value.
|
public static Reference reference(java.lang.String name)
name
- the name of the referencepublic static Reference reference(Symbol symbol)
symbol
- the symbolpublic static Reference reference(ValueDeclIdentifier ident)
ident
- the name of the referencepublic static Reference reference(TypeDeclIdentifier ident)
ident
- the name of the referencepublic static ValueDeclIdentifier valueDeclIdentifier(java.lang.String name)
name
- the name of the identifierpublic static TypeDeclIdentifier typeDeclIdentifier(java.lang.String name)
name
- the name of the identifierpublic static FormulaDeclIdentifier formulaDeclIdentifier(java.lang.String name)
name
- the name of the identifierpublic static TypedIdentifier typedIdentifier(ValueDeclIdentifier identifier, Type type)
identifier
- the identifiertype
- its typepublic static ValuedIdentifier valuedIdentifier(Reference identifier, Expression value)
identifier
- the identifiervalue
- its valuepublic static Number number(java.lang.String value)
value
- the digit representation of the numberpublic static Logical logical(boolean value)
value
- the value of the constantpublic static BitLogical bitLogical(boolean value)
value
- the value of the constantpublic static TypeDeclaration typeDeclaration(TypeDeclIdentifier name, Type type)
name
- the declared nametype
- the type associated to the namepublic static FormulaDeclaration formulaDeclaration(FormulaDeclIdentifier name, Expression formula)
name
- the declared nameformula
- the formula associated to the namepublic static AxiomDeclaration axiomDeclaration(FormulaDeclIdentifier name, Expression formula)
name
- the declared nameformula
- the formula associated to the namepublic static ValueDeclaration valueDeclaration(ValueDeclIdentifier name, Type type, Expression value)
name
- the declared nametype
- the type associated to the namevalue
- the value associated to the name (may be null)public static FunctionType functionType(Type[] domain, Type range)
domain
- the domain of the typerange
- the range of the typepublic static AtomicType atomicType(java.lang.String name)
name
- the name of the typepublic static TupleType tupleType(Type[] base)
base
- the base typespublic static RecordType recordType(TypedIdentifier[] base)
base
- the base types (field:type pairs)public static ArrayType arrayType(Type index, Type base)
index
- the index type of the arraybase
- the base type of the arraypublic static SubType subType(Expression predicate)
predicate
- the predicate defining the subtypepublic static SubrangeType subrangeType(Expression from, Expression to)
from
- the lower boundto
- the upper boundpublic static LetExpression letExpression(ValueDeclaration[] declarations, Expression base)
declarations
- the local bindings in the expressionsbase
- the base expressionspublic static LetType letType(TypeDeclaration[] declarations, Type base)
declarations
- the local bindings in the typebase
- the base typepublic static IfThenElseExpression ifThenElseExpression(Expression condition, Expression thenbranch, Expression elsebranch)
condition
- the formula deciding which branch is selectedthenbranch
- the branch selected if the formula yields trueelsebranch
- the branch selected if the formula yields falsepublic static NotFormula notFormula(Expression base)
base
- the base formulapublic static BitNotTerm bitNotTerm(Expression base)
base
- the base termpublic static NegationTerm negationTerm(Expression base)
base
- the base termpublic static TupleTerm tupleTerm(Expression[] base)
base
- the array of base terms, base.length gt 1public static RecordTerm recordTerm(ValuedIdentifier[] base)
base
- the array of base terms, base.length gt 1public static LambdaTerm lambdaTerm(TypedIdentifier[] variables, Expression base)
variables
- the quantified variablesbase
- the base termpublic static ArrayTerm arrayTerm(TypedIdentifier[] variables, Expression base)
variables
- the quantified variablesbase
- the base termpublic static ForallFormula forallFormula(TypedIdentifier[] variables, Expression base)
variables
- the quantified variablesbase
- the base formulapublic static ExistsFormula existsFormula(TypedIdentifier[] variables, Expression base)
variables
- the quantified variablesbase
- the base formulapublic static AndFormula andFormula(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static BitAndTerm bitAndTerm(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static OrFormula orFormula(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static BitOrTerm bitOrTerm(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static EquivalentFormula equivalentFormula(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static NotEquivalentFormula notEquivalentFormula(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static ImpliesFormula impliesFormula(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static EqualsFormula equalsFormula(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static NotEqualsFormula notEqualsFormula(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static PlusTerm plusTerm(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static MinusTerm minusTerm(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static TimesTerm timesTerm(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static DividesTerm dividesTerm(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static PowerTerm powerTerm(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static LessFormula lessFormula(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static LessEqualFormula lessEqualFormula(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static GreaterFormula greaterFormula(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static GreaterEqualFormula greaterEqualFormula(Expression base1, Expression base2)
base1
- the first componentbase2
- the second componentpublic static SelectorIndex selectorIndex(Expression base)
base
- the selector basepublic static SelectorNumber selectorNumber(Number base)
base
- the selector basepublic static SelectorIdentifier selectorIdentifier(Reference base)
base
- the selector basepublic static SelectionTerm selectionTerm(Expression base1, Selector base2)
base1
- the compound objectbase2
- the selectorpublic static UpdateTerm updateTerm(Expression base1, Selector[] base2, Expression value)
base1
- the compound objectbase2
- the sequence of selectorsvalue
- the update valuepublic static ApplicationExpression applicationExpression(Expression base1, Expression[] base2)
base1
- the function/predicatebase2
- the sequence of arguments