Package | Description |
---|---|
fmrisc.ProgramExplorer.InOut | |
fmrisc.ProgramExplorer.Judgements | |
fmrisc.ProgramExplorer.Parser | |
fmrisc.ProgramExplorer.Syntax | |
fmrisc.ProgramExplorer.Syntax.Logic |
Modifier and Type | Method and Description |
---|---|
void |
Breaks.visit(TypedIdentifier exp) |
void |
PrettyPrinter.visit(TypedIdentifier exp) |
void |
PrettyMathML.visit(TypedIdentifier exp) |
Modifier and Type | Method and Description |
---|---|
static Formula |
Satisfies.existsFormula(TypedIdentifier[] vars,
Formula formula)
Bind variables in formula by existential quantification.
|
static Formula |
Satisfies.forallFormula(TypedIdentifier[] vars,
Formula formula)
Bind variables in formula by universal quantification.
|
Modifier and Type | Method and Description |
---|---|
java.util.Vector<TypedIdentifier> |
SpecLangParser.paramList() |
Modifier and Type | Method and Description |
---|---|
void |
SpecLangParser.param(java.util.Vector<TypedIdentifier> sequence) |
Modifier and Type | Method and Description |
---|---|
void |
ASTVisitor.visit(TypedIdentifier tree) |
void |
ASTPrinter.visit(TypedIdentifier ident) |
void |
ASTCloner.visit(TypedIdentifier tree) |
void |
ASTVisitorBase.visit(TypedIdentifier tree) |
Modifier and Type | Method and Description |
---|---|
static TypedIdentifier |
TypedIdentifier.construct(Identifier name,
Type type)
Construct an identifier with a type.
|
TypedIdentifier[] |
RecordType.getBase()
Get named base types.
|
TypedIdentifier[] |
QuantifiedExpression.getVariables()
Get bound variables of the expression.
|
Modifier and Type | Method and Description |
---|---|
static RecordType |
RecordType.construct(TypedIdentifier[] base)
Construct record type.
|
static ExistsFormula |
ExistsFormula.construct(TypedIdentifier[] vars,
Formula body)
Construct an existentially quantified formula.
|
static LambdaFormula |
LambdaFormula.construct(TypedIdentifier[] vars,
Formula body)
Construct a function expression with a formula body.
|
static ForallFormula |
ForallFormula.construct(TypedIdentifier[] vars,
Formula body)
Construct a universally quantified formula.
|
static LambdaTerm |
LambdaTerm.construct(TypedIdentifier[] vars,
Term body)
Construct a function expression.
|
static ArrayTerm |
ArrayTerm.construct(TypedIdentifier[] vars,
Term body)
Construct a function expression.
|