Skip navigation links
A B C D E F G H I J K L M N O P Q R S T U V W X Z 

A

AbstractAssignable(int) - Constructor for class wyil.lang.Code.AbstractAssignable
Construct an abstract bytecode which assigns to a given target register.
AbstractAttributeMap<T extends Attribute> - Class in wyil.util
Provides a generic implementation of Attribute.Map which can be used as a starting point for constructing specific instances of Attribute.Map.
AbstractAttributeMap() - Constructor for class wyil.util.AbstractAttributeMap
 
AbstractBinaryAssignable(T, int, int, int) - Constructor for class wyil.lang.Code.AbstractBinaryAssignable
 
AbstractBinaryOp(T, int, int) - Constructor for class wyil.lang.Code.AbstractBinaryOp
 
AbstractContext(Attribute...) - Constructor for class wycs.syntax.WyalFile.AbstractContext
 
AbstractContext(Collection<Attribute>) - Constructor for class wycs.syntax.WyalFile.AbstractContext
 
AbstractEntry<T> - Class in wyfs.util
Provides a simple implementation of Path.Entry.
AbstractEntry(Path.ID) - Constructor for class wyfs.util.AbstractEntry
 
AbstractFolder - Class in wyfs.util
An abstract folder contains other folders, and path entries.
AbstractFolder(Path.ID) - Constructor for class wyfs.util.AbstractFolder
Construct an Abstract Folder representing a given ID (taken relative to the enclosing root).
AbstractFunctionOrMethod(String, Collection<SyntacticType>, Attribute...) - Constructor for class wyc.lang.Expr.AbstractFunctionOrMethod
 
AbstractFunctionOrMethod(String, Collection<SyntacticType>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.AbstractFunctionOrMethod
 
AbstractIndirectInvoke(Expr, Collection<Expr>, Attribute...) - Constructor for class wyc.lang.Expr.AbstractIndirectInvoke
 
AbstractIndirectInvoke(Expr, Collection<Expr>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.AbstractIndirectInvoke
 
AbstractInvoke(String, Path.ID, Collection<Expr>, Attribute...) - Constructor for class wyc.lang.Expr.AbstractInvoke
 
AbstractInvoke(String, Path.ID, Collection<Expr>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.AbstractInvoke
 
AbstractLexer - Class in wycc.io
Provides a generic mechanism for turning an input file or string into a list of tokens.
AbstractLexer(AbstractLexer.Rule[], InputStream) - Constructor for class wycc.io.AbstractLexer
Construct from an input stream using UTF-8 as the default character encoding.
AbstractLexer(AbstractLexer.Rule[], InputStream, CharsetDecoder) - Constructor for class wycc.io.AbstractLexer
Construct from an input stream using a given character set decoder.
AbstractLexer(AbstractLexer.Rule[], Reader) - Constructor for class wycc.io.AbstractLexer
Construct from a reader (which already has some notion of character enconding included).
AbstractLexer.BlockCommentRule - Class in wycc.io
Standard rule for parsing block comments with user-defineable start and end syntax.
AbstractLexer.CharRule - Class in wycc.io
A standard rule for parsing characters which begin with single quote marks.
AbstractLexer.DecimalRule - Class in wycc.io
A standard rule for parsing numbers represented in decimal (i.e.
AbstractLexer.Error - Exception in wycc.io
Used to report lexing errors.
AbstractLexer.IdentifierRule - Class in wycc.io
A standard rule for parsing identifiers.
AbstractLexer.KeywordRule - Class in wycc.io
Standard rule for parsing keywords.
AbstractLexer.LineCommentRule - Class in wycc.io
Standard rule for parsing line comments with user-defineable syntax.
AbstractLexer.OperatorRule - Class in wycc.io
Standard rule for parsing Operators.
AbstractLexer.Rule - Class in wycc.io
A lexer rule is responsible for matching a given character sequence and turning it into a token.
AbstractLexer.StringRule - Class in wycc.io
A standard rule for parsing strings which begin with quote marks.
AbstractLexer.WhitespaceRule - Class in wycc.io
Standard rule for parsing Whitespace.
AbstractNaryAssignable(T, int, int...) - Constructor for class wyil.lang.Code.AbstractNaryAssignable
 
AbstractRoot<T extends Path.Folder> - Class in wyfs.util
Provides a simple implementation of Path.Root.
AbstractRoot(Content.Registry) - Constructor for class wyfs.util.AbstractRoot
 
AbstractUnaryAssignable(T, int, int) - Constructor for class wyil.lang.Code.AbstractUnaryAssignable
 
AbstractUnaryOp(T, int) - Constructor for class wyil.lang.Code.AbstractUnaryOp
 
AbstractVariable(String, Attribute...) - Constructor for class wyc.lang.Expr.AbstractVariable
 
AbstractVariable(String, Collection<Attribute>) - Constructor for class wyc.lang.Expr.AbstractVariable
 
accepts(Automaton, DefaultInterpretation.Term) - Method in class wyautl_old.lang.DefaultInterpretation
 
accepts(int, Automaton, DefaultInterpretation.Term) - Method in class wyautl_old.lang.DefaultInterpretation
 
accepts(Automaton, T) - Method in interface wyautl_old.lang.Interpretation
Returns true iff the given automaton accepts the given value.
accepts(Interpretation, Automaton, ArrayList<DefaultInterpretation.Term>) - Static method in class wyautl_old.util.Tester
 
accepts(Automaton, DefaultInterpretation.Term) - Method in class wyil.util.type.TypeTester.TypeInterpretation
 
accepts(int, Automaton, DefaultInterpretation.Term) - Method in class wyil.util.type.TypeTester.TypeInterpretation
 
add(Build.Rule) - Method in class wybs.util.StdProject
Add a new builder to this project.
add(WhileyFile.Declaration) - Method in class wyc.lang.WhileyFile
 
add(Value) - Method in class wycs.core.Value.Array
 
add(Value.Decimal) - Method in class wycs.core.Value.Decimal
 
add(Value.Integer) - Method in class wycs.core.Value.Integer
 
Add(Automaton, int, int) - Static method in class wycs.solver.SolverUtil
Construct an automaton node representing the addition of two arithmetic expressions.
add(WyalFile.Declaration) - Method in class wycs.syntax.WyalFile
 
add(Code) - Method in class wyil.lang.CodeBlock
Append a bytecode onto the end of this block.
add(int, Code) - Method in class wyil.lang.CodeBlock
Insert a bytecode at a given position in this block.
add(Constant.Decimal) - Method in class wyil.lang.Constant.Decimal
 
add(Constant.Integer) - Method in class wyil.lang.Constant.Integer
 
add(Constant.Rational) - Method in class wyil.lang.Constant.Rational
 
add(Code, Attribute...) - Method in class wyil.util.AttributedCodeBlock
Append a bytecode onto the end of this block, along with any attributes to be associated with that bytecode.
add(Code, Collection<Attribute>) - Method in class wyil.util.AttributedCodeBlock
Append a bytecode onto the end of this block, along with any attributes to be associated with that bytecode.
add(int, Code, Attribute...) - Method in class wyil.util.AttributedCodeBlock
Insert a bytecode at a given position in this block.
add(int, Code, Collection<Attribute>) - Method in class wyil.util.AttributedCodeBlock
Insert a bytecode at a given position in this block.
add(int) - Method in class wyjc.runtime.WyRat
 
add(long) - Method in class wyjc.runtime.WyRat
 
add(BigInteger) - Method in class wyjc.runtime.WyRat
 
add(WyRat) - Method in class wyjc.runtime.WyRat
 
addAll(AttributedCodeBlock) - Method in class wyil.util.AttributedCodeBlock
Add all bytecodes to this block from another include all attributes associated with each bytecode.
addAttributes(Attribute.Map<Attribute>) - Method in class wyil.util.AttributedCodeBlock
 
addBuildRules(StdProject) - Method in class wyc.util.WycBuildTask
Add all build rules to the project.
addBuildRules(StdProject) - Method in class wyjc.util.WyjcBuildTask
 
addCoercion(Type, Type, int, HashMap<Wyil2JavaBuilder.JvmConstant, Integer>, ArrayList<Bytecode>) - Method in class wyjc.Wyil2JavaBuilder
 
addCompileBuildRules(StdProject) - Method in class wycs.util.WycsBuildTask
Add all build rules to the project.
addDeclaredVariables(int, TypePattern, Type, CodeGenerator.Environment, AttributedCodeBlock) - Static method in class wyc.builder.CodeGenerator
The purpose of this method is to construct aliases for variables declared as part of type patterns.
addDeclaredVariables(TypePattern, Nominal, List<VariableDeclarations.Declaration>, CodeGenerator.Environment) - Static method in class wyc.builder.CodeGenerator
 
addDeclaredVariables(Collection<String>) - Method in class wyc.lang.TypePattern
 
addDeclaredVariables(Collection<String>) - Method in class wyc.lang.TypePattern.Intersection
 
addDeclaredVariables(Collection<String>) - Method in class wyc.lang.TypePattern.Leaf
 
addDeclaredVariables(Collection<String>) - Method in class wyc.lang.TypePattern.Rational
 
addDeclaredVariables(Collection<String>) - Method in class wyc.lang.TypePattern.Record
 
addDeclaredVariables(Collection<String>) - Method in class wyc.lang.TypePattern.Tuple
 
addDeclaredVariables(Collection<String>) - Method in class wyc.lang.TypePattern.Union
 
addDeclaredVariables(Code, TypePattern, HashMap<String, Code>) - Method in class wycs.builders.CodeGeneration
 
addDeclaredVariables(Collection<String>) - Method in class wycs.syntax.TypePattern
 
addDeclaredVariables(Collection<String>) - Method in class wycs.syntax.TypePattern.Intersection
 
addDeclaredVariables(Collection<String>) - Method in class wycs.syntax.TypePattern.Leaf
 
addDeclaredVariables(Collection<String>) - Method in class wycs.syntax.TypePattern.Rational
 
addDeclaredVariables(Collection<String>) - Method in class wycs.syntax.TypePattern.Record
 
addDeclaredVariables(Collection<String>) - Method in class wycs.syntax.TypePattern.Tuple
 
addDeclaredVariables(Collection<String>) - Method in class wycs.syntax.TypePattern.Union
 
addDecompileBuildRules(StdProject) - Method in class wycs.util.WycsBuildTask
 
addQuantifiedVariables(TypePattern, ArrayList<Pair<SemanticType, Integer>>, HashMap<String, Code>) - Method in class wycs.builders.CodeGeneration
 
afterPoint - Variable in class wycc.io.Token.Number
 
afterType - Variable in class wyc.lang.Expr.AssignedVariable
 
afterType - Variable in class wyil.lang.Codes.Update
 
allocate(Type) - Method in class wyc.builder.CodeGenerator.Environment
 
allocate(Type, String) - Method in class wyc.builder.CodeGenerator.Environment
 
ALLOCATION_NOT_PERMITTED_IN_FUNCTION - Static variable in class wyil.util.ErrorMessages
 
AMBIGUOUS_COERCION - Static variable in class wyil.util.ErrorMessages
 
and(Code...) - Static method in class wycs.builders.CodeGeneration
 
And(SemanticType...) - Static method in class wycs.core.SemanticType
 
And(Collection<SemanticType>) - Static method in class wycs.core.SemanticType
 
And(Automaton, int...) - Static method in class wycs.solver.Solver
 
And(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
and(Content.Filter<T>, Content.Filter<T>) - Static method in class wyfs.lang.Content
Combine two filters together produce one filter whose items must be matched by both of the original filters.
and(WyByte) - Method in class wyjc.runtime.WyByte
 
AndT(Automaton, int...) - Static method in class wycs.core.Types
 
AndT(Automaton, List<Integer>) - Static method in class wycs.core.Types
 
AndT(Automaton, int...) - Static method in class wycs.solver.Solver
 
AndT(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
Any(Attribute...) - Constructor for class wyc.lang.SyntacticType.Any
 
Any - Static variable in class wycs.core.SemanticType
 
ANY - Static variable in class wycs.solver.smt.Sort
The singleton any sort.
Any(Attribute...) - Constructor for class wycs.syntax.SyntacticType.Any
 
Any(Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Any
 
ANY - Static variable in class wyjc.runtime.WyType
 
AnyT - Static variable in class wycs.core.Types
 
AnyT - Static variable in class wycs.solver.Solver
 
append(Automaton, Automaton.State) - Static method in class wyautl_old.lang.Automata
Append a new state onto the end of an automaton.
append(Automaton, Automaton) - Static method in class wyautl_old.lang.Automata
Append an automaton (the tail) onto the back of another (the head).
append(Element...) - Method in class wycs.solver.smt.Block
Appends the given elements to this block.
append(Collection<? extends Element>) - Method in class wycs.solver.smt.Block
Appends the given elements to this block.
append(Element...) - Method in class wycs.solver.smt.Smt2File
Appends the given elements to this file.
append(Collection<? extends Element>) - Method in class wycs.solver.smt.Smt2File
Appends the given elements to this file.
append(String) - Method in interface wyfs.lang.Path.ID
Append a component onto the end of this id.
append(String) - Method in class wyfs.util.Trie
 
append(CodeBlock.Index) - Method in class wyil.lang.CodeBlock.Index
Append a given index onto the end of this index;
append(WyList, WyList) - Static method in class wyjc.runtime.WyList
 
append(WyList, Object) - Static method in class wyjc.runtime.WyList
 
append(Object, WyList) - Static method in class wyjc.runtime.WyList
 
apply(Collection<? extends Path.Entry<?>>) - Method in interface wybs.lang.Build.Rule
Apply this rule to a given compilation group, producing a set of generated or modified files.
apply(Collection<? extends Path.Entry<?>>) - Method in class wybs.util.StdBuildRule
 
apply(List<Pipeline.Modifier>) - Method in class wycc.lang.Pipeline
Apply a list of modifiers in the order of appearance.
apply(T) - Method in interface wycc.lang.Transform
Apply this transform to the given module.
apply(WycsFile) - Method in class wycs.transforms.MacroExpansion
 
apply(WycsFile) - Method in class wycs.transforms.SmtVerificationCheck
Apply this transform to the given module.
apply(WyalFile) - Method in class wycs.transforms.TypePropagation
 
apply(WycsFile) - Method in class wycs.transforms.VerificationCheck
Verify the given list of Wycs statements.
apply(WyilFile) - Method in class wyil.checks.CoercionCheck
 
apply(WyilFile) - Method in class wyil.checks.DefiniteAssignmentCheck
 
apply(WyilFile) - Method in class wyil.checks.ModuleCheck
 
apply(WyilFile) - Method in class wyil.io.WyilFilePrinter
 
apply(WyilFile) - Method in class wyil.transforms.ConstantPropagation
 
apply(WyilFile) - Method in class wyil.transforms.DeadCodeElimination
Apply this transformation to all type, function and method declarations of a given module.
apply(WyilFile) - Method in class wyil.transforms.LiveVariablesAnalysis
 
apply(WyilFile) - Method in class wyil.transforms.LoopVariants
 
apply(WyilFile) - Method in class wyil.util.dfa.BackwardFlowAnalysis
 
apply(WyilFile) - Method in class wyil.util.dfa.ForwardFlowAnalysis
 
argument - Variable in class wycc.util.OptArg
The kind of argument accepted by this option (if any).
arguments - Variable in class wyc.lang.Expr.AbstractIndirectInvoke
 
arguments - Variable in class wyc.lang.Expr.AbstractInvoke
 
arguments - Variable in class wyc.lang.Expr.ArrayInitialiser
 
arguments - Variable in class wyil.lang.Constant.Lambda
 
argValues(Method) - Static method in class wyc.WycMain
 
argValues(Method) - Static method in class wycs.WycsMain
 
Array(SyntacticType, Attribute...) - Constructor for class wyc.lang.SyntacticType.Array
 
Array(SemanticType) - Static method in class wycs.core.SemanticType
 
Array(Collection<Value>) - Static method in class wycs.core.Value
 
Array(String, String) - Constructor for class wycs.solver.smt.Sort.Array
 
Array(Automaton, int...) - Static method in class wycs.solver.Solver
 
Array(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
Array(Type, boolean) - Static method in class wyil.lang.Type
Construct a list type using the given element type.
ArrayAny - Static variable in class wycs.core.SemanticType
 
ArrayGenerator(Expr, Expr, Attribute...) - Constructor for class wyc.lang.Expr.ArrayGenerator
 
ArrayInitialiser(Collection<Expr>, Attribute...) - Constructor for class wyc.lang.Expr.ArrayInitialiser
 
ArrayInitialiser(Attribute, Expr...) - Constructor for class wyc.lang.Expr.ArrayInitialiser
 
ArrayT(Automaton, int) - Static method in class wycs.core.Types
 
ArrayT(Automaton, int) - Static method in class wycs.solver.Solver
 
arrayToString(int...) - Static method in class wyil.lang.CodeUtils
 
asList() - Method in class wyc.builder.CodeGenerator.Environment
 
Assert(Expr, Attribute...) - Constructor for class wyc.lang.Stmt.Assert
Create a given assert statement.
Assert(String, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Assert
Create a given assert statement.
Assert(String, Code<?>, Attribute...) - Constructor for class wycs.core.WycsFile.Assert
 
Assert(String, Code<?>, Collection<Attribute>) - Constructor for class wycs.core.WycsFile.Assert
 
Assert(String) - Constructor for class wycs.solver.smt.Stmt.Assert
Creates a new Assert statement with the given expression.
Assert(String, Expr, Attribute...) - Constructor for class wycs.syntax.WyalFile.Assert
 
Assert(String, Expr, Collection<Attribute>) - Constructor for class wycs.syntax.WyalFile.Assert
 
Assert(Collection<Code>) - Static method in class wyil.lang.Codes
Construct an assert bytecode which represents a user-defined assertion check.
assertion() - Method in exception wycs.transforms.VerificationCheck.AssertionFailure
 
AssertionFailure(String, WycsFile.Assert) - Constructor for exception wycs.transforms.SmtVerificationCheck.AssertionFailure
Creates a new AssertionFailure with the given error message and assertion.
AssertionFailure(WycsFile.Assert) - Constructor for exception wycs.transforms.SmtVerificationCheck.AssertionFailure
Creates a new AssertionFailure with the given assertion.
AssertionFailure(String, WycsFile.Assert, Rewriter, Automaton, Automaton) - Constructor for exception wycs.transforms.VerificationCheck.AssertionFailure
 
Assign(Expr.LVal, Expr, Attribute...) - Constructor for class wyc.lang.Stmt.Assign
Create an assignment from a given lhs and rhs.
Assign(Expr.LVal, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Assign
Create an assignment from a given lhs and rhs.
Assign(Type, int, int) - Static method in class wyil.lang.Codes
Construct a copy bytecode which copies the value from a given operand register into a given target register.
assign(int, Constant, ConstantPropagation.Env, CodeBlock.Index) - Method in class wyil.transforms.ConstantPropagation
Update the environment to record an assignment of a constant to a given register.
assignedType() - Method in class wyil.lang.Code.AbstractAssignable
Return the type of value assigned to the target register by this bytecode.
assignedType() - Method in class wyil.lang.Code.AbstractNaryAssignable
 
assignedType() - Method in class wyil.lang.Codes.Const
 
assignedType() - Method in class wyil.lang.Codes.Dereference
 
assignedType() - Method in class wyil.lang.Codes.FieldLoad
 
assignedType() - Method in class wyil.lang.Codes.IndexOf
 
assignedType() - Method in class wyil.lang.Codes.IndirectInvoke
 
assignedType() - Method in class wyil.lang.Codes.Invoke
 
assignedType() - Method in class wyil.lang.Codes.Lambda
 
assignedType() - Method in class wyil.lang.Codes.LengthOf
 
assignedType() - Method in class wyil.lang.Codes.TupleLoad
 
assignedType() - Method in class wyil.lang.Codes.Update
 
assignedType() - Method in class wyil.lang.Codes.Void
 
AssignedVariable(String, Attribute...) - Constructor for class wyc.lang.Expr.AssignedVariable
 
AssignedVariable(String, Collection<Attribute>) - Constructor for class wyc.lang.Expr.AssignedVariable
 
associate(Path.Entry) - Method in class wyc.util.WycBuildTask.Registry
 
associate(Path.Entry) - Method in class wycs.util.WycsBuildTask.Registry
 
associate(Path.Entry<?>) - Method in interface wyfs.lang.Content.Registry
Attempt to associate a content type with this entry.
associate(Content.Type<T>, T) - Method in interface wyfs.lang.Path.Entry
Associate this entry with a content type, and optionally provide the contents.
associate(Content.Type<T>, T) - Method in class wyfs.util.AbstractEntry
 
associate(Path.Entry) - Method in class wyil.Main.Registry
 
associate(Path.Entry) - Method in class wyjc.util.WyjcBuildTask.Registry
 
Assume(Expr, Attribute...) - Constructor for class wyc.lang.Stmt.Assume
Create a given assume statement.
Assume(String, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Assume
Create a given assume statement.
Assume(String, Expr, Attribute...) - Constructor for class wycs.syntax.WyalFile.Assume
 
Assume(String, Expr, Collection<Attribute>) - Constructor for class wycs.syntax.WyalFile.Assume
 
assume(Expr) - Method in class wyil.builders.VcBranch
Assume a given condition holds on this branch.
Assume(Collection<Code>) - Static method in class wyil.lang.Codes
Construct an assume bytecode which represents a user-defined assumption.
Atom(int) - Constructor for class wycs.core.SemanticType.Atom
 
Attribute - Interface in wycc.lang
Represents a piece of meta-information that may be associated with a WYIL bytecode or declaration.
attribute(Class<T>) - Method in interface wycc.lang.SyntacticElement
Get the first attribute of the given class type.
attribute(Class<T>) - Method in class wycc.lang.SyntacticElement.Impl
 
Attribute - Interface in wyil.lang
An Attribute represents a chunk of meta-data associated with one or more aspects of a WyIL file.
attribute(Class<T>) - Method in class wyil.lang.WyilFile.Block
 
attribute(CodeBlock.Index, Class<T>) - Method in class wyil.util.AttributedCodeBlock
Return the attribute of a given kind associated with a bytecode.
Attribute.Map<T extends Attribute> - Interface in wyil.lang
An attribute map is an attribute which specifically associates meta-data with individual bytecodes, as opposed to other attributes which associated data with larger constructs (e.g.
Attribute.Origin - Class in wycc.lang
Represents an originating source location for a given syntactic element.
Attribute.Source - Class in wycc.lang
Represents a location in the source code of a Whiley Module.
AttributedCodeBlock - Class in wyil.util
An attributed code block represents a bytecode block where each bytecode can be attributed with a pre-defined set of attributes.
AttributedCodeBlock(Attribute.Map<? extends Attribute>...) - Constructor for class wyil.util.AttributedCodeBlock
 
AttributedCodeBlock(Collection<? extends Attribute.Map<Attribute>>) - Constructor for class wyil.util.AttributedCodeBlock
 
AttributedCodeBlock(Collection<Code>, Attribute.Map<Attribute>...) - Constructor for class wyil.util.AttributedCodeBlock
 
AttributedCodeBlock(Collection<Code>, Collection<Attribute.Map<Attribute>>) - Constructor for class wyil.util.AttributedCodeBlock
 
AttributedCodeBlock(CodeBlock.Index, AttributedCodeBlock) - Constructor for class wyil.util.AttributedCodeBlock
This constructor is used when creating a subblock only.
attributes() - Method in interface wycc.lang.SyntacticElement
Get the list of attributes associated with this syntactice element.
attributes() - Method in class wycc.lang.SyntacticElement.Impl
 
attributes(SyntacticElement) - Static method in class wycs.builders.CodeGeneration
 
attributes() - Method in class wyil.lang.WyilFile.Block
 
attributes(CodeBlock.Index) - Method in class wyil.util.AttributedCodeBlock
 
attributes() - Method in class wyil.util.AttributedCodeBlock
 
Automata - Class in wyautl_old.lang
This class provides various algorithms for manipulating automata.
Automata() - Constructor for class wyautl_old.lang.Automata
 
Automaton - Class in wyautl_old.lang
A finite-state automaton for representing Whiley types.
Automaton(Automaton.State...) - Constructor for class wyautl_old.lang.Automaton
 
Automaton(List<Automaton.State>) - Constructor for class wyautl_old.lang.Automaton
 
Automaton(Automaton) - Constructor for class wyautl_old.lang.Automaton
 
automaton - Variable in class wycs.core.SemanticType
 
automaton() - Method in class wycs.core.SemanticType
 
automaton - Variable in class wyil.lang.Type.Compound
 
Automaton.State - Class in wyautl_old.lang
Represents a state in an automaton.

B

BackwardFlowAnalysis<T> - Class in wyil.util.dfa
 
BackwardFlowAnalysis() - Constructor for class wyil.util.dfa.BackwardFlowAnalysis
 
base - Variable in class wycc.io.Token.Number
 
beforePoint - Variable in class wycc.io.Token.Number
 
bin2str(int) - Static method in class wyfs.io.BinaryOutputStream
 
Binary(SemanticType, Code.Op, Code<?>, Code<?>, Attribute...) - Static method in class wycs.core.Code
 
Binary(SemanticType, Code.Op, Code<?>, Code<?>, Collection<Attribute>) - Static method in class wycs.core.Code
 
Binary(Expr.Binary.Op, Expr, Expr, Attribute...) - Constructor for class wycs.syntax.Expr.Binary
 
Binary(Expr.Binary.Op, Expr, Expr, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.Binary
 
BinaryAutomataReader - Class in wyautl_old.io
Responsible for reading an automaton in a binary format from an input stream.
BinaryAutomataReader(BinaryInputStream) - Constructor for class wyautl_old.io.BinaryAutomataReader
 
BinaryAutomataWriter - Class in wyautl_old.io
Responsible for writing an automaton in a binary format to an output stream.
BinaryAutomataWriter(BinaryOutputStream) - Constructor for class wyautl_old.io.BinaryAutomataWriter
 
BinaryInputStream - Class in wyfs.io
 
BinaryInputStream(InputStream) - Constructor for class wyfs.io.BinaryInputStream
 
BinaryMatrix - Class in wyautl_old.util
A binary matrix represents a matrix of binary digits.
BinaryMatrix(int, int, boolean) - Constructor for class wyautl_old.util.BinaryMatrix
Construct an empty binary matrix of a given number of rows and columns.
BinaryOperator(Type, int, int, int, Codes.BinaryOperatorKind) - Static method in class wyil.lang.Codes
 
BinaryOutputStream - Class in wyfs.io
 
BinaryOutputStream(OutputStream) - Constructor for class wyfs.io.BinaryOutputStream
Write out data in big-endian format.
BinaryReader(BinaryInputStream) - Constructor for class wyil.lang.Type.BinaryReader
 
BinaryTypeWriter(BinaryOutputStream) - Constructor for class wyil.util.type.TypeGenerator.BinaryTypeWriter
 
BinaryWriter(BinaryOutputStream) - Constructor for class wyil.lang.Type.BinaryWriter
 
bind(SemanticType, SemanticType, Map<String, SemanticType>) - Static method in class wycs.core.SemanticType
Attempt to bind a generic type against a concrete type.
bindGenerics(NameID, SemanticType, SyntacticElement) - Method in class wycs.builders.CodeGeneration
This function attempts to find an appropriate binding for the generic types accepted by a given function, and the supplied argument type.
binding - Variable in class wycs.core.Code.FunCall
 
bindParameters(Object[]) - Method in class wyjc.runtime.WyLambda
 
BinOp(Expr.BOp, Expr, Expr, Attribute...) - Constructor for class wyc.lang.Expr.BinOp
 
BinOp(Expr.BOp, Expr, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Expr.BinOp
 
Block - Class in wycs.solver.smt
Represents a block of statements.
Block() - Constructor for class wycs.solver.smt.Block
 
Block(Collection<Attribute>) - Constructor for class wyil.lang.WyilFile.Block
 
Block(Attribute[]) - Constructor for class wyil.lang.WyilFile.Block
 
block - Variable in class wyil.util.Interpreter.Context
 
BLOCK_Assert - Static variable in class wycs.io.WycsFileWriter
 
BLOCK_Body - Static variable in class wyil.io.WyilFileWriter
 
BLOCK_Code - Static variable in class wycs.io.WycsFileWriter
 
BLOCK_Constant - Static variable in class wyil.io.WyilFileWriter
 
BLOCK_Constraint - Static variable in class wyil.io.WyilFileWriter
 
BLOCK_Documentation - Static variable in class wycs.io.WycsFileWriter
 
BLOCK_Documentation - Static variable in class wyil.io.WyilFileWriter
 
BLOCK_Function - Static variable in class wycs.io.WycsFileWriter
 
BLOCK_Function - Static variable in class wyil.io.WyilFileWriter
 
BLOCK_Header - Static variable in class wycs.io.WycsFileWriter
 
BLOCK_Header - Static variable in class wyil.io.WyilFileWriter
 
BLOCK_License - Static variable in class wycs.io.WycsFileWriter
 
BLOCK_License - Static variable in class wyil.io.WyilFileWriter
 
BLOCK_Macro - Static variable in class wycs.io.WycsFileWriter
 
BLOCK_Method - Static variable in class wyil.io.WyilFileWriter
 
BLOCK_Module - Static variable in class wycs.io.WycsFileWriter
 
BLOCK_Module - Static variable in class wyil.io.WyilFileWriter
 
BLOCK_Postcondition - Static variable in class wyil.io.WyilFileWriter
 
BLOCK_Precondition - Static variable in class wyil.io.WyilFileWriter
 
BLOCK_Type - Static variable in class wycs.io.WycsFileWriter
 
BLOCK_Type - Static variable in class wyil.io.WyilFileWriter
 
BlockComment(String, int) - Constructor for class wycc.io.Token.BlockComment
 
BlockCommentRule(String, String) - Constructor for class wycc.io.AbstractLexer.BlockCommentRule
 
blocks() - Method in class wyil.lang.WyilFile
Returns all declarations declared in this WyilFile.
body - Variable in class wyc.lang.Expr.Lambda
 
body - Variable in class wyc.lang.Stmt.DoWhile
 
body - Variable in class wyc.lang.Stmt.While
 
body - Variable in class wycs.syntax.WyalFile.Macro
 
body() - Method in class wyil.lang.WyilFile.FunctionOrMethod
 
Bool(Attribute...) - Constructor for class wyc.lang.SyntacticType.Bool
 
Bool - Static variable in class wycs.core.SemanticType
 
Bool(boolean) - Static method in class wycs.core.Value
 
BOOL - Static variable in class wycs.solver.smt.Sort
The singleton boolean sort.
Bool(Attribute...) - Constructor for class wycs.syntax.SyntacticType.Bool
 
Bool(Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Bool
 
BOOL - Static variable in class wyjc.runtime.WyType
 
BoolT - Static variable in class wycs.core.Types
 
BoolT - Static variable in class wycs.solver.Solver
 
bootpath - Variable in class wyc.util.WycBuildTask
The boot path contains the location of the whiley runtime (wyrt) library.
bootpath - Variable in class wycs.util.WycsBuildTask
The boot path contains the location of the wycs standard library.
bounds - Variable in class wyc.lang.SyntacticType.Intersection
 
bounds - Variable in class wyc.lang.SyntacticType.Union
 
bounds() - Method in class wyil.lang.Type.Union
Return the bounds of this union type.
bounds - Variable in class wyjc.runtime.WyType.Union
 
BRANCH_ALWAYS_TAKEN - Static variable in class wyil.util.ErrorMessages
 
branches - Variable in class wyil.lang.Codes.Switch
 
Break(Attribute...) - Constructor for class wyc.lang.Stmt.Break
 
BREAK_OUTSIDE_LOOP - Static variable in class wyil.util.ErrorMessages
 
Build - Interface in wybs.lang
 
build(Collection<Pair<Path.Entry<?>, Path.Root>>) - Method in interface wybs.lang.Builder
Build a given set of source files to produce target files in specified locations.
build(Collection<? extends Path.Entry<?>>) - Method in class wybs.util.StdProject
Build a given set of source entries, including all files which depend upon them.
build(Collection<Pair<Path.Entry<?>, Path.Root>>) - Method in class wyc.builder.WhileyBuilder
 
build(List<File>) - Method in class wyc.util.WycBuildTask
Building the given source files.
build(Collection<Pair<Path.Entry<?>, Path.Root>>) - Method in class wycs.builders.Wyal2WycsBuilder
 
build(Collection<Pair<Path.Entry<?>, Path.Root>>) - Method in class wycs.builders.Wycs2WyalBuilder
 
build(List<File>) - Method in class wycs.util.WycsBuildTask
Building the given source files.
build(Collection<Pair<Path.Entry<?>, Path.Root>>) - Method in class wyil.builders.Wyil2WyalBuilder
 
build(Collection<Pair<Path.Entry<?>, Path.Root>>) - Method in class wyjc.Wyil2JavaBuilder
 
Build.Project - Interface in wybs.lang
Represents a top-level entity responsible for managing everything related to a given build.
Build.Rule - Interface in wybs.lang
A build rule is an abstraction describing how a set of one or more source files should be compiled.
BUILD_NUMBER - Static variable in class wyc.WycMain
 
BUILD_NUMBER - Static variable in class wycs.WycsMain
 
buildAll() - Method in class wyc.util.WycBuildTask
Build all source files which have been modified.
buildAll() - Method in class wycs.util.WycsBuildTask
Build all source files which have been modified.
buildCoercion(Type, Type, int, HashMap<Wyil2JavaBuilder.JvmConstant, Integer>, ClassFile) - Method in class wyjc.Wyil2JavaBuilder
The build coercion method constructs a static final private method which accepts a value of type "from", and coerces it into a value of type "to".
buildCoercion(Type, Type, int, HashMap<Wyil2JavaBuilder.JvmConstant, Integer>, ArrayList<Bytecode>) - Method in class wyjc.Wyil2JavaBuilder
 
buildCoercion(Type.Tuple, Type.Tuple, int, HashMap<Wyil2JavaBuilder.JvmConstant, Integer>, ArrayList<Bytecode>) - Method in class wyjc.Wyil2JavaBuilder
 
buildCoercion(Type.Array, Type.Array, int, HashMap<Wyil2JavaBuilder.JvmConstant, Integer>, ArrayList<Bytecode>) - Method in class wyjc.Wyil2JavaBuilder
 
buildEntries(List<Path.Entry<T>>) - Method in class wyc.util.WycBuildTask
 
buildEntries(List<Path.Entry<T>>) - Method in class wycs.util.WycsBuildTask
 
Builder - Interface in wybs.lang
Responsible for transforming files from one content type to another.
builder - Variable in class wyc.util.WycAntTask
 
builder - Variable in class wyc.WycMain
The build-task responsible for actually compiling and building files.
builder - Variable in class wycs.util.WycsAntTask
 
builder - Variable in class wycs.WycsMain
The build-task responsible for actually compiling and building files.
buildFunctionBlock(String, List<Type>, Type) - Method in class wyil.builders.VcGenerator
Construct a function with a given name representing a block of code.
buildInvariantCall(VcBranch, String, boolean[]) - Method in class wyil.builders.VcGenerator
Construct invocation of loop invariant macro.
buildLabelMap(AttributedCodeBlock) - Static method in class wyil.lang.CodeUtils
Construct a mapping from labels to their block indices within a root block.
buildLambda(NameID, Type.FunctionOrMethod, int) - Method in class wyjc.Wyil2JavaBuilder
Construct a class which implements a lambda expression.
buildMacroBlock(String, CodeBlock.Index, AttributedCodeBlock, List<Type>, boolean) - Method in class wyil.builders.VcGenerator
Construct a macro with a given name representing a block of code.
buildVariableDeclarations(List<Stmt>, List<VariableDeclarations.Declaration>, CodeGenerator.Environment, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
Construct the set of variable declarations for a given list of variables.
buildVariableDeclarations(Stmt, List<VariableDeclarations.Declaration>, CodeGenerator.Environment, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
 
buildVerificationCondition(Expr, VcBranch, Type[], AttributedCodeBlock, Expr...) - Method in class wyil.builders.VcGenerator
Construct a verification condition which asserts a given expression on the current branch.
Byte(Attribute...) - Constructor for class wyc.lang.SyntacticType.Byte
 
Byte(Attribute...) - Constructor for class wycs.syntax.SyntacticType.Byte
 
Byte(Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Byte
 
BYTE - Static variable in class wyjc.runtime.WyType
 
bytecodes - Variable in class wyil.lang.CodeBlock
 
bytecodes() - Method in class wyil.lang.CodeBlock
Returns a reference to the internal bytecode array.

C

call(Object[]) - Method in class wyjc.runtime.WyLambda
 
canonicalise(Automaton, Comparator<Automaton.State>) - Static method in class wyautl_old.lang.Automata
Turn an automaton into its canonical form.
canonicaliseTest(Interpretation, ArrayList<DefaultInterpretation.Term>, ArrayList<Automaton>, boolean) - Static method in class wyautl_old.util.Tester
 
Case(List<Expr>, List<Stmt>, Attribute...) - Constructor for class wyc.lang.Stmt.Case
 
cases - Variable in class wyc.lang.Stmt.Switch
 
Cast(SyntacticType, Expr, Attribute...) - Constructor for class wyc.lang.Expr.Cast
 
Cast(SemanticType, Code<?>, SemanticType, Attribute...) - Static method in class wycs.core.Code
 
Cast(SemanticType, Code<?>, SemanticType, Collection<Attribute>) - Static method in class wycs.core.Code
 
Cast(SyntacticType, Expr, Attribute...) - Constructor for class wycs.syntax.Expr.Cast
 
Cast(SyntacticType, Expr, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.Cast
 
ceil() - Method in class wyjc.runtime.WyRat
 
Char(char, String, int) - Constructor for class wycc.io.Token.Char
 
Char(Attribute...) - Constructor for class wycs.syntax.SyntacticType.Char
 
Char(Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Char
 
CHAR - Static variable in class wyjc.runtime.WyType
 
character - Variable in class wycc.io.Token.Char
 
CharRule() - Constructor for class wycc.io.AbstractLexer.CharRule
 
check(WyilFile.FunctionOrMethod) - Method in class wyil.checks.CoercionCheck
 
check(CodeBlock.Index, CodeBlock, AttributedCodeBlock, WyilFile.FunctionOrMethod) - Method in class wyil.checks.CoercionCheck
 
check(Type, Type, HashSet<Pair<Type, Type>>, SourceLocation) - Method in class wyil.checks.CoercionCheck
Recursively check that there is no ambiguity in coercing type from into type to.
check(WyilFile.FunctionOrMethod) - Method in class wyil.checks.ModuleCheck
 
checkFunctionPure(WyilFile.FunctionOrMethod) - Method in class wyil.checks.ModuleCheck
Check a given function is pure.
checkFunctionPure(CodeBlock.Index, CodeBlock, AttributedCodeBlock) - Method in class wyil.checks.ModuleCheck
 
CheckSat() - Constructor for class wycs.solver.smt.Stmt.CheckSat
 
checkUses(CodeBlock.Index, Code, HashSet<Integer>) - Method in class wyil.checks.DefiniteAssignmentCheck
 
children - Variable in class wyautl_old.lang.Automaton.State
 
children - Variable in class wyautl_old.lang.DefaultInterpretation.Term
 
classDir - Variable in class wyjc.util.WyjcBuildTask
The class directory is the filesystem directory where all generated jvm class files are stored.
classFileFilter - Static variable in class wyjc.util.WyjcBuildTask
The purpose of the class file filter is simply to ensure only binary files are loaded in a given directory root.
clazz - Variable in class wycc.lang.Pipeline.Template
 
clear() - Method in class wycs.solver.smt.Block
Clears this block, removing all elements.
clear() - Method in class wycs.solver.smt.Smt2File
Clears this file, removing all elements.
clone(SemanticType, Code.Op, Code<?>[]) - Method in class wycs.core.Code.Binary
 
clone(SemanticType, Code.Op, Code<?>[]) - Method in class wycs.core.Code.Cast
 
clone(T, Code.Op, Code<?>[]) - Method in class wycs.core.Code
 
clone(SemanticType, Code.Op, Code<?>[]) - Method in class wycs.core.Code.Constant
 
clone(SemanticType.Function, Code.Op, Code<?>[]) - Method in class wycs.core.Code.FunCall
 
clone(SemanticType.Array, Code.Op, Code<?>[]) - Method in class wycs.core.Code.IndexOf
 
clone(SemanticType, Code.Op, Code<?>[]) - Method in class wycs.core.Code.Is
 
clone(SemanticType.Tuple, Code.Op, Code<?>[]) - Method in class wycs.core.Code.Load
 
clone(SemanticType, Code.Op, Code<?>[]) - Method in class wycs.core.Code.Nary
 
clone(SemanticType, Code.Op, Code<?>[]) - Method in class wycs.core.Code.Quantifier
 
clone(SemanticType, Code.Op, Code<?>[]) - Method in class wycs.core.Code.Unary
 
clone(SemanticType, Code.Op, Code<?>[]) - Method in class wycs.core.Code.Variable
 
clone(List<Expr>) - Static method in class wycs.syntax.Expr
Clone all expressions in a list.
clone(List<SyntacticType>) - Static method in class wycs.syntax.SyntacticType.Util
Clone a list of syntactic types.
clone(int, int) - Method in class wyil.lang.Code.AbstractBinaryOp
 
clone(int, int[]) - Method in class wyil.lang.Code.AbstractNaryAssignable
 
clone(int) - Method in class wyil.lang.Code.AbstractUnaryOp
 
clone() - Method in class wyil.lang.Code.Compound
 
clone() - Method in class wyil.lang.Codes.Assert
 
clone(int, int[]) - Method in class wyil.lang.Codes.Assign
 
clone() - Method in class wyil.lang.Codes.Assume
 
clone(int, int[]) - Method in class wyil.lang.Codes.BinaryOperator
 
clone(int, int[]) - Method in class wyil.lang.Codes.Convert
 
clone(int) - Method in class wyil.lang.Codes.Debug
 
clone(int, int[]) - Method in class wyil.lang.Codes.Dereference
 
clone(int, int[]) - Method in class wyil.lang.Codes.FieldLoad
 
clone(int, int) - Method in class wyil.lang.Codes.If
 
clone(int) - Method in class wyil.lang.Codes.IfIs
 
clone(int, int[]) - Method in class wyil.lang.Codes.IndexOf
 
clone(int, int[]) - Method in class wyil.lang.Codes.IndirectInvoke
 
clone() - Method in class wyil.lang.Codes.Invariant
 
clone(int, int[]) - Method in class wyil.lang.Codes.Invert
 
clone(int, int[]) - Method in class wyil.lang.Codes.Invoke
 
clone(int, int[]) - Method in class wyil.lang.Codes.Lambda
 
clone(int, int[]) - Method in class wyil.lang.Codes.LengthOf
 
clone(int, int[]) - Method in class wyil.lang.Codes.ListGenerator
 
clone() - Method in class wyil.lang.Codes.Loop
 
clone(int, int[]) - Method in class wyil.lang.Codes.Move
 
clone(int, int[]) - Method in class wyil.lang.Codes.NewList
 
clone(int, int[]) - Method in class wyil.lang.Codes.NewObject
 
clone(int, int[]) - Method in class wyil.lang.Codes.NewRecord
 
clone(int, int[]) - Method in class wyil.lang.Codes.NewTuple
 
clone(int, int[]) - Method in class wyil.lang.Codes.Not
 
clone(int) - Method in class wyil.lang.Codes.Return
 
clone(int) - Method in class wyil.lang.Codes.Switch
 
clone(int, int[]) - Method in class wyil.lang.Codes.TupleLoad
 
clone(int, int[]) - Method in class wyil.lang.Codes.UnaryOperator
 
clone(int, int[]) - Method in class wyil.lang.Codes.Update
 
clone(int, int[]) - Method in class wyil.lang.Codes.Void
 
clone() - Method in class wyil.transforms.ConstantPropagation.Env
 
cloneTypes(List<SyntacticType>) - Static method in class wycs.syntax.Expr
Clone all types in a list.
close() - Method in class wyautl_old.io.BinaryAutomataReader
 
close() - Method in class wyautl_old.io.BinaryAutomataWriter
 
close() - Method in interface wyautl_old.io.GenericReader
 
close() - Method in interface wyautl_old.io.GenericWriter
 
close() - Method in class wyautl_old.io.TextAutomataWriter
 
close() - Method in class wycs.io.WycsFileReader
 
close() - Method in class wyfs.io.BinaryOutputStream
 
close() - Method in class wyil.io.WyilFileReader
 
close() - Method in class wyil.io.WyilFileWriter
 
close() - Method in class wyil.util.type.TypeGenerator.TextTypeWriter
 
Code<T extends SemanticType> - Class in wycs.core
Represents a "bytecode" in the language of the Wycs theorem prover.
Code(T, Code.Op, Code<?>[], Attribute...) - Constructor for class wycs.core.Code
 
Code(T, Code.Op, Code<?>[], Collection<Attribute>) - Constructor for class wycs.core.Code
 
Code - Interface in wyil.lang
Represents a WyIL bytecode.
Code.AbstractAssignable - Class in wyil.lang
Represents the set of all bytecodes which assign a result to a single target register.
Code.AbstractBinaryAssignable<T> - Class in wyil.lang
Represents the set of all bytcodes which take two register operands and write a result to the target register.
Code.AbstractBinaryOp<T> - Class in wyil.lang
Represents the set of all bytcodes which take two register operands and perform a comparison of their values.
Code.AbstractNaryAssignable<T> - Class in wyil.lang
Represents the set of all bytcodes which take an arbitrary number of register operands and write a result to the target register.
Code.AbstractUnaryAssignable<T> - Class in wyil.lang
Represents the set of all bytcodes which take a single register operand and assign a result to the target register.
Code.AbstractUnaryOp<T> - Class in wyil.lang
Represents the set of all bytcodes which take a single register operand, and do not assign to a target register.
Code.Binary - Class in wycs.core
 
Code.Cast - Class in wycs.core
 
Code.Compound - Class in wyil.lang
A compound bytecode represents a bytecode that contains sequence of zero or more bytecodes.
Code.Constant - Class in wycs.core
 
Code.FunCall - Class in wycs.core
 
Code.IndexOf - Class in wycs.core
 
Code.Is - Class in wycs.core
 
Code.Load - Class in wycs.core
 
Code.Nary - Class in wycs.core
 
Code.Op - Enum in wycs.core
 
Code.Quantifier - Class in wycs.core
 
Code.Unary - Class in wycs.core
 
Code.Unit - Class in wyil.lang
A Unit bytecode is one which does not contain other bytecodes.
Code.Variable - Class in wycs.core
 
CodeBlock - Class in wyil.lang
Represents a complete sequence of bytecode instructions.
CodeBlock() - Constructor for class wyil.lang.CodeBlock
 
CodeBlock(Code...) - Constructor for class wyil.lang.CodeBlock
 
CodeBlock(Collection<Code>) - Constructor for class wyil.lang.CodeBlock
 
CodeBlock.Index - Class in wyil.lang
Provides a mechanism for identifying bytecodes within arbitrarily nested blocks.
CodeGeneration - Class in wycs.builders
Responsible for translating an individual WyalFile into a WycsFile.
CodeGeneration(Wyal2WycsBuilder) - Constructor for class wycs.builders.CodeGeneration
 
CodeGenerator - Class in wyc.builder
Responsible for compiling the declarations, statements and expression found in a WhileyFile into WyIL declarations and bytecode blocks.
CodeGenerator(WhileyBuilder, FlowTypeChecker) - Constructor for class wyc.builder.CodeGenerator
Construct a code generator object for translating WhileyFiles into WyilFiles.
CodeGenerator.Environment - Class in wyc.builder
Maintains a mapping from Variable names to their allocated register slot, and their declared types.
Codes - Class in wyil.lang
 
Codes() - Constructor for class wyil.lang.Codes
 
Codes.Assert - Class in wyil.lang
Represents a block of bytecode instructions representing an assertion.
Codes.AssertOrAssume - Class in wyil.lang
An abstract class representing either an assert or assume bytecode block.
Codes.Assign - Class in wyil.lang
Copy the contents from a given operand register into a given target register.
Codes.Assume - Class in wyil.lang
Represents a block of bytecode instructions representing an assumption.
Codes.BinaryOperator - Class in wyil.lang
A binary operation which reads two numeric values from the operand registers, performs an operation on them and writes the result to the target register.
Codes.BinaryOperatorKind - Enum in wyil.lang
Represents a binary operator (e.g.
Codes.Comparator - Enum in wyil.lang
Represents a comparison operator (e.g.
Codes.Const - Class in wyil.lang
Writes a constant value to a target register.
Codes.Convert - Class in wyil.lang
Reads a value from the operand register, converts it to a given type and writes the result to the target register.
Codes.Debug - Class in wyil.lang
Read a string from the operand register and prints it to the debug console.
Codes.Dereference - Class in wyil.lang
Reads a reference value from the operand register, dereferences it (i.e.
Codes.Fail - Class in wyil.lang
A bytecode that halts execution by raising a runtime fault.
Codes.FieldLoad - Class in wyil.lang
Reads a record value from an operand register, extracts the value of a given field and writes this to the target register.
Codes.Goto - Class in wyil.lang
Branches unconditionally to the given label.
Codes.If - Class in wyil.lang
Branches conditionally to the given label by reading the values from two operand registers and comparing them.
Codes.IfIs - Class in wyil.lang
Branches conditionally to the given label based on the result of a runtime type test against a value from the operand register.
Codes.IndexOf - Class in wyil.lang
Reads an effective list or map from the source (left) operand register, and a key value from the key (right) operand register and returns the value associated with that key.
Codes.IndirectInvoke - Class in wyil.lang
Represents an indirect function call.
Codes.Invariant - Class in wyil.lang
Represents a block of bytecode instructions representing an assertion.
Codes.Invert - Class in wyil.lang
Corresponds to a bitwise inversion operation, which reads a byte value from the operand register, inverts it and writes the result to the target resgister.
Codes.Invoke - Class in wyil.lang
Corresponds to a function or method call whose parameters are read from zero or more operand registers.
Codes.Label - Class in wyil.lang
Represents the labelled destination of a branch or loop statement.
Codes.Lambda - Class in wyil.lang
 
Codes.LengthOf - Class in wyil.lang
Reads an (effective) collection (i.e.
Codes.ListGenerator - Class in wyil.lang
Constructs a new list value from the values given by zero or more operand registers.
Codes.ListLVal - Class in wyil.lang
An LVal with list type.
Codes.Loop - Class in wyil.lang
Represents a block of code which loops continuously until e.g.
Codes.LVal<T> - Class in wyil.lang
Represents a type which may appear on the left of an assignment expression.
Codes.Move - Class in wyil.lang
Moves the contents of a given operand register into a given target register.
Codes.NewList - Class in wyil.lang
Constructs a new list value from the values given by zero or more operand registers.
Codes.NewObject - Class in wyil.lang
Instantiate a new object from the value in a given operand register, and write the result (a reference to that object) to a given target register.
Codes.NewRecord - Class in wyil.lang
Constructs a new record value from the values of zero or more operand register, each of which is associated with a field name.
Codes.NewTuple - Class in wyil.lang
Constructs a new tuple value from the values given by zero or more operand registers.
Codes.Nop - Class in wyil.lang
Represents a no-operation bytecode which, as the name suggests, does nothing.
Codes.Not - Class in wyil.lang
Read a boolean value from the operand register, inverts it and writes the result to the target register.
Codes.Quantify - Class in wyil.lang
 
Codes.RecordLVal - Class in wyil.lang
An LVal with record type.
Codes.ReferenceLVal - Class in wyil.lang
An LVal with list type.
Codes.Return - Class in wyil.lang
Returns from the enclosing function or method, possibly returning a value.
Codes.Switch - Class in wyil.lang
Performs a multi-way branch based on the value contained in the operand register.
Codes.TupleLoad - Class in wyil.lang
Read a tuple value from the operand register, extract the value it contains at a given index and write that to the target register.
Codes.UnaryOperator - Class in wyil.lang
Read a number (int or real) from the operand register, perform a unary arithmetic operation on it (e.g.
Codes.UnaryOperatorKind - Enum in wyil.lang
 
Codes.Update - Class in wyil.lang
Pops a compound structure, zero or more indices and a value from the stack and updates the compound structure with the given value.
Codes.Void - Class in wyil.lang
The void bytecode is used to indicate that the given register(s) are no longer live.
codeString() - Method in class wyil.lang.Codes.If
 
CodeUtils - Class in wyil.lang
 
CodeUtils() - Constructor for class wyil.lang.CodeUtils
 
CoercionCheck - Class in wyil.checks
The point of the coercion check is to check that all convert bytecodes make sense, and are not ambiguous.
CoercionCheck(Builder) - Constructor for class wyil.checks.CoercionCheck
 
Comment(String, int) - Constructor for class wycc.io.Token.Comment
 
COMPARATOR - Static variable in class wyjc.runtime.Util
 
compare(Object, Object) - Method in class wyjc.runtime.Util.Comparator
 
compare(Object, Object) - Static method in class wyjc.runtime.Util
 
compare(BigInteger, Object) - Static method in class wyjc.runtime.Util
 
compare(WyRat, Object) - Static method in class wyjc.runtime.Util
 
compare(WyList, Object) - Static method in class wyjc.runtime.Util
 
compare(WyList, WyList) - Static method in class wyjc.runtime.Util
 
compare(WyTuple, Object) - Static method in class wyjc.runtime.Util
 
compare(WyTuple, WyTuple) - Static method in class wyjc.runtime.Util
 
compare(WyRecord, Object) - Static method in class wyjc.runtime.Util
 
compare(WyRecord, WyRecord) - Static method in class wyjc.runtime.Util
 
compareTo(Value) - Method in class wycs.core.Value.Array
 
compareTo(Value) - Method in class wycs.core.Value.Bool
 
compareTo(Value) - Method in class wycs.core.Value.Decimal
 
compareTo(Value) - Method in class wycs.core.Value.Integer
 
compareTo(Value) - Method in class wycs.core.Value.Null
 
compareTo(Value) - Method in class wycs.core.Value.String
 
compareTo(Value) - Method in class wycs.core.Value.Tuple
 
compareTo(Path.ID) - Method in class wyfs.util.Trie
 
compareTo(Constant) - Method in class wyil.lang.Constant.Bool
 
compareTo(Constant) - Method in class wyil.lang.Constant.Byte
 
compareTo(Constant) - Method in class wyil.lang.Constant.Decimal
 
compareTo(Constant) - Method in class wyil.lang.Constant.Integer
 
compareTo(Constant) - Method in class wyil.lang.Constant.Lambda
 
compareTo(Constant) - Method in class wyil.lang.Constant.List
 
compareTo(Constant) - Method in class wyil.lang.Constant.Null
 
compareTo(Constant) - Method in class wyil.lang.Constant.Rational
 
compareTo(Constant) - Method in class wyil.lang.Constant.Record
 
compareTo(Constant) - Method in class wyil.lang.Constant.Tuple
 
compareTo(Constant) - Method in class wyil.lang.Constant.Type
 
compareTo(WyByte) - Method in class wyjc.runtime.WyByte
 
compareTo(WyRat) - Method in class wyjc.runtime.WyRat
 
CompilationUnit - Interface in wycc.lang
 
compliment() - Method in class wyjc.runtime.WyByte
 
Compound(Code...) - Constructor for class wyil.lang.Code.Compound
 
Compound(Collection<Code>) - Constructor for class wyil.lang.Code.Compound
 
Compound(Automaton) - Constructor for class wyil.lang.Type.Compound
 
computeFixpoint(Relation) - Static method in class wyautl_old.lang.Automata
Determine whether a relationship between two automaton exists.
condition - Variable in class wyc.lang.Expr.Quantifier
 
condition - Variable in class wyc.lang.Stmt.DoWhile
 
condition - Variable in class wyc.lang.Stmt.IfElse
 
condition - Variable in class wyc.lang.Stmt.While
 
condition - Variable in class wycs.core.WycsFile.Assert
 
condition - Variable in class wycs.core.WycsFile.Macro
 
Config() - Constructor for class wyautl_old.util.Generator.Config
 
configure(Map<String, Object>) - Method in class wyc.WycMain
 
configure(Map<String, Object>) - Method in class wyjc.WyjcMain
 
Const(int, Constant) - Static method in class wyil.lang.Codes
Construct a const bytecode which loads a given constant onto the stack.
Constant(Constant, Attribute...) - Constructor for class wyc.lang.Expr.Constant
 
Constant(List<Modifier>, Expr, String, Attribute...) - Constructor for class wyc.lang.WhileyFile.Constant
 
constant - Variable in class wyc.lang.WhileyFile.Constant
 
Constant(Value, Attribute...) - Static method in class wycs.core.Code
 
Constant(Value, Collection<Attribute>) - Static method in class wycs.core.Code
 
Constant(Value, Attribute...) - Constructor for class wycs.syntax.Expr.Constant
 
Constant(Value, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.Constant
 
constant - Variable in class wyil.lang.Codes.Const
 
Constant - Class in wyil.lang
 
Constant() - Constructor for class wyil.lang.Constant
 
constant(String) - Method in class wyil.lang.WyilFile
Looks up a constant declaration in this WyilFile with the given name; if none exists, returns null.
Constant(Collection<Modifier>, String, Constant, Attribute...) - Constructor for class wyil.lang.WyilFile.Constant
 
Constant(Collection<Modifier>, String, Constant, Collection<Attribute>) - Constructor for class wyil.lang.WyilFile.Constant
 
constant() - Method in class wyil.lang.WyilFile.Constant
 
Constant.Bool - Class in wyil.lang
 
Constant.Byte - Class in wyil.lang
 
Constant.Decimal - Class in wyil.lang
 
Constant.Integer - Class in wyil.lang
 
Constant.Lambda - Class in wyil.lang
 
Constant.List - Class in wyil.lang
 
Constant.Null - Class in wyil.lang
 
Constant.Rational - Class in wyil.lang
 
Constant.Record - Class in wyil.lang
 
Constant.Tuple - Class in wyil.lang
 
Constant.Type - Class in wyil.lang
 
CONSTANT_Array - Static variable in class wycs.io.WycsFileWriter
 
CONSTANT_Byte - Static variable in class wyil.io.WyilFileWriter
 
CONSTANT_False - Static variable in class wycs.io.WycsFileWriter
 
CONSTANT_False - Static variable in class wyil.io.WyilFileWriter
 
CONSTANT_Function - Static variable in class wyil.io.WyilFileWriter
 
CONSTANT_Int - Static variable in class wycs.io.WycsFileWriter
 
CONSTANT_Int - Static variable in class wyil.io.WyilFileWriter
 
CONSTANT_List - Static variable in class wyil.io.WyilFileWriter
 
CONSTANT_Method - Static variable in class wyil.io.WyilFileWriter
 
CONSTANT_Null - Static variable in class wycs.io.WycsFileWriter
 
CONSTANT_Null - Static variable in class wyil.io.WyilFileWriter
 
CONSTANT_Real - Static variable in class wycs.io.WycsFileWriter
 
CONSTANT_Real - Static variable in class wyil.io.WyilFileWriter
 
CONSTANT_Record - Static variable in class wyil.io.WyilFileWriter
 
CONSTANT_String - Static variable in class wycs.io.WycsFileWriter
 
CONSTANT_True - Static variable in class wycs.io.WycsFileWriter
 
CONSTANT_True - Static variable in class wyil.io.WyilFileWriter
 
CONSTANT_Tuple - Static variable in class wycs.io.WycsFileWriter
 
CONSTANT_Tuple - Static variable in class wyil.io.WyilFileWriter
 
ConstantAccess(String, Path.ID, Attribute...) - Constructor for class wyc.lang.Expr.ConstantAccess
 
ConstantAccess(String, Path.ID, Collection<Attribute>) - Constructor for class wyc.lang.Expr.ConstantAccess
 
ConstantAccess(String, Path.ID, Attribute...) - Constructor for class wycs.syntax.Expr.ConstantAccess
 
ConstantAccess(String, Path.ID, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.ConstantAccess
 
ConstantPropagation - Class in wyil.transforms
Propagates constants throughout the bytecodes making up the functions, methods and invariants of a WyIL file.
ConstantPropagation(Builder) - Constructor for class wyil.transforms.ConstantPropagation
 
ConstantPropagation.Env - Class in wyil.transforms
 
constants - Variable in class wyc.lang.Stmt.Case
 
constants() - Method in class wyil.lang.WyilFile
Returns all constant declarations in this WyilFile.
constants - Variable in class wyjc.Wyil2JavaBuilder
Map of Constant values to their pool index
constraint - Variable in class wycs.core.WycsFile.Function
 
constraint - Variable in class wycs.syntax.WyalFile.Function
 
constraints() - Method in class wyil.builders.VcBranch
Return the constraints which are known to hold on this branch segment, excluding those which hold on ancestor branches.
construct(Automaton) - Static method in class wyautl_old.lang.DefaultInterpretation
Construct a value from an automata.
construct(Type, Type) - Static method in class wyc.lang.Nominal
 
construct(Automaton) - Static method in class wycs.core.SemanticType
Construct a given type from an automaton.
construct(Automaton) - Static method in class wyil.lang.Type
The construct methods constructs a Type from an automaton.
contains(Path.Entry<?>) - Method in interface wybs.lang.Build.Project
Check whether or not a given entry is contained in this root;
contains(Path.Entry<?>) - Method in class wybs.util.StdProject
Check whether or not a given entry is contained in this root;
contains(Automaton, Automaton.List) - Static method in class wycs.solver.Solver$native
Determine whether a given variable v is contained within a given expression e.
contains(Automaton, int, int) - Static method in class wycs.solver.Solver$native
 
contains(Path.Entry<?>) - Method in interface wyfs.lang.Path.Folder
Check whether or not a given entry is contained in this folder;
contains(Path.Entry<?>) - Method in interface wyfs.lang.Path.Root
Check whether or not a given entry is contained in this root;
contains(Path.Entry<?>) - Method in class wyfs.util.AbstractFolder
 
contains(Path.Entry<?>) - Method in class wyfs.util.AbstractRoot
 
contains(CodeBlock.Index) - Method in class wyil.lang.CodeBlock
Check whether a given index is contained within this block.
Content - Class in wyfs.lang
 
Content() - Constructor for class wyfs.lang.Content
 
Content.Filter<T> - Interface in wyfs.lang
A generic mechanism for selecting a subset of content based on a path filter and a content type.
Content.Registry - Interface in wyfs.lang
Responsible for associating content types to path entries.
Content.Type<T> - Interface in wyfs.lang
Provides an abstract mechanism for reading and writing file in a given format.
contents - Variable in class wyfs.util.AbstractEntry
 
contents() - Method in class wyfs.util.AbstractFolder
Extract all entries from the given folder.
contents() - Method in class wyfs.util.DirectoryRoot.Folder
 
contents() - Method in class wyfs.util.JarFileRoot.Folder
 
contents() - Method in class wyfs.util.VirtualRoot.Folder
 
ContentType - Static variable in class wyc.lang.WhileyFile
 
ContentType - Static variable in class wycs.core.WycsFile
 
ContentType - Static variable in class wycs.syntax.WyalFile
 
contentType() - Method in interface wyfs.lang.Path.Entry
Get the content type associated with this file.
contentType - Variable in class wyfs.util.AbstractEntry
 
contentType() - Method in class wyfs.util.AbstractEntry
 
ContentType - Static variable in class wyil.lang.WyilFile
Responsible for identifying and reading/writing WyilFiles.
ContentType - Static variable in class wyjc.util.WyjcBuildTask
 
contentTypes - Variable in class wyfs.util.AbstractRoot
 
Context(CodeBlock.Index, AttributedCodeBlock) - Constructor for class wyil.util.Interpreter.Context
 
Continue(Attribute...) - Constructor for class wyc.lang.Stmt.Continue
 
convert(TypePattern, List<String>, WyalFile.Context) - Method in class wycs.builders.Wyal2WycsBuilder
 
convert(SyntacticType, Set<String>, WyalFile.Context) - Method in class wycs.builders.Wyal2WycsBuilder
Convert a syntactic type into a semantic type.
convert(Automaton, SemanticType) - Method in class wycs.transforms.VerificationCheck
Construct an automaton node representing a given semantic type.
convert(Constant, AttributedCodeBlock, VcBranch) - Method in class wyil.builders.VcGenerator
Convert a WyIL constant into its equivalent WyCS constant.
Convert(Type, int, int, Type) - Static method in class wyil.lang.Codes
 
cop - Variable in class wyc.lang.Expr.Quantifier
 
copy() - Method in class wycs.syntax.Expr.Binary
 
copy() - Method in class wycs.syntax.Expr.Cast
 
copy() - Method in class wycs.syntax.Expr.Constant
 
copy() - Method in class wycs.syntax.Expr.ConstantAccess
 
copy() - Method in class wycs.syntax.Expr
 
copy() - Method in class wycs.syntax.Expr.Exists
 
copy() - Method in class wycs.syntax.Expr.FieldAccess
 
copy() - Method in class wycs.syntax.Expr.ForAll
 
copy() - Method in class wycs.syntax.Expr.IndexOf
 
copy() - Method in class wycs.syntax.Expr.IndirectInvoke
 
copy() - Method in class wycs.syntax.Expr.Invoke
 
copy() - Method in class wycs.syntax.Expr.Is
 
copy() - Method in class wycs.syntax.Expr.Nary
 
copy() - Method in class wycs.syntax.Expr.Record
 
copy() - Method in class wycs.syntax.Expr.Unary
 
copy() - Method in class wycs.syntax.Expr.Variable
 
copy() - Method in class wycs.syntax.SyntacticType.Any
 
copy() - Method in class wycs.syntax.SyntacticType.Bool
 
copy() - Method in class wycs.syntax.SyntacticType.Byte
 
copy() - Method in class wycs.syntax.SyntacticType.Char
 
copy() - Method in interface wycs.syntax.SyntacticType
 
copy() - Method in class wycs.syntax.SyntacticType.Function
 
copy() - Method in class wycs.syntax.SyntacticType.Int
 
copy() - Method in class wycs.syntax.SyntacticType.Intersection
 
copy() - Method in class wycs.syntax.SyntacticType.List
 
copy() - Method in class wycs.syntax.SyntacticType.Negation
 
copy() - Method in class wycs.syntax.SyntacticType.Nominal
 
copy() - Method in class wycs.syntax.SyntacticType.Null
 
copy() - Method in class wycs.syntax.SyntacticType.Real
 
copy() - Method in class wycs.syntax.SyntacticType.Record
 
copy() - Method in class wycs.syntax.SyntacticType.Reference
 
copy() - Method in class wycs.syntax.SyntacticType.Strung
 
copy() - Method in class wycs.syntax.SyntacticType.Tuple
 
copy() - Method in class wycs.syntax.SyntacticType.Union
 
copy() - Method in class wycs.syntax.SyntacticType.Variable
 
copy() - Method in class wycs.syntax.SyntacticType.Void
 
copy() - Method in class wycs.syntax.TypePattern
 
copy() - Method in class wycs.syntax.TypePattern.Intersection
 
copy() - Method in class wycs.syntax.TypePattern.Leaf
 
copy() - Method in class wycs.syntax.TypePattern.Rational
 
copy() - Method in class wycs.syntax.TypePattern.Record
 
copy() - Method in class wycs.syntax.TypePattern.Tuple
 
copy() - Method in class wycs.syntax.TypePattern.Union
 
count - Variable in class wyc.lang.Expr.ArrayGenerator
 
count - Variable in class wyfs.io.BinaryInputStream
 
count - Variable in class wyfs.io.BinaryOutputStream
 
create(Path.ID, Content.Type<T>) - Method in interface wyfs.lang.Path.Folder
Create a new entry in this folder with the given ID (taken relative to this folder) and content-type.
create(Path.ID, Content.Type<T>) - Method in interface wyfs.lang.Path.Root
Create an entry of a given content type at a given path.
create(Path.ID, Content.Type<T>) - Method in class wyfs.util.AbstractRoot
 
create(Path.ID, Content.Type<T>) - Method in class wyfs.util.DirectoryRoot.Folder
 
create(Path.ID, Content.Type<T>) - Method in class wyfs.util.JarFileRoot
 
create(Path.ID, Content.Type<T>) - Method in class wyfs.util.JarFileRoot.Folder
 
create(Path.ID, Content.Type<T>) - Method in class wyfs.util.VirtualRoot.Folder
 
createSubBlock() - Method in class wyil.util.AttributedCodeBlock
Construct a temporary sub-block for use in creating an attributed compound bytecode (e.g.
CYCLIC_CONSTANT_DECLARATION - Static variable in class wyil.util.ErrorMessages
 

D

data - Variable in class wyautl_old.lang.Automaton.State
 
data - Variable in class wyautl_old.lang.DefaultInterpretation.Term
 
DATA - Variable in class wyautl_old.util.Generator.Kind
A method for generating approprate supplementary data.
DATA_COMPARATOR - Static variable in class wyil.util.type.TypeAlgorithms
The data comparator is used in the type canonicalisation process.
DEAD_CODE - Static variable in class wyil.util.ErrorMessages
 
DeadCodeElimination - Class in wyil.transforms
Removes dead-code from method and function bodies, preconditions, postconditions and type invariants.
DeadCodeElimination(Builder) - Constructor for class wyil.transforms.DeadCodeElimination
 
Debug(Expr, Attribute...) - Constructor for class wyc.lang.Stmt.Debug
 
Debug(Expr, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Debug
 
debug - Variable in class wycs.builders.Wyal2WycsBuilder
 
debug - Variable in class wycs.builders.Wycs2WyalBuilder
 
debug(Automaton) - Static method in class wycs.transforms.VerificationCheck
 
debug(Code, String) - Static method in class wycs.transforms.VerificationCheck
 
debug - Variable in class wycs.util.WycsBuildTask
Indicates whether or the compiler should produce debugging information during compilation.
Debug(int) - Static method in class wyil.lang.Codes
 
Decimal(BigDecimal) - Static method in class wycs.core.Value
 
DecimalRule() - Constructor for class wycc.io.AbstractLexer.DecimalRule
 
declaration(String) - Method in class wyc.lang.WhileyFile
 
declaration(String) - Method in class wycs.core.WycsFile
 
declaration(String, SemanticType) - Method in class wycs.core.WycsFile
 
declaration(String, Class<T>) - Method in class wycs.core.WycsFile
 
declaration(String) - Method in class wycs.syntax.WyalFile
 
declaration(String, Class<T>) - Method in class wycs.syntax.WyalFile
 
Declaration(Type, String) - Constructor for class wyil.attributes.VariableDeclarations.Declaration
 
Declaration(String, Collection<Modifier>, Attribute...) - Constructor for class wyil.lang.WyilFile.Declaration
 
Declaration(String, Collection<Modifier>, Collection<Attribute>) - Constructor for class wyil.lang.WyilFile.Declaration
 
declarations - Variable in class wyc.lang.WhileyFile
 
declarations(Class<T>) - Method in class wyc.lang.WhileyFile
 
declarations(Class<T>, String) - Method in class wyc.lang.WhileyFile
 
declarations() - Method in class wycs.core.WycsFile
 
declarations() - Method in class wycs.syntax.WyalFile
 
DeclareFun(String, List<String>, String) - Constructor for class wycs.solver.smt.Stmt.DeclareFun
 
DeclareSort(String, int) - Constructor for class wycs.solver.smt.Stmt.DeclareSort
 
decompile(WycsFile) - Method in class wycs.builders.Wycs2WyalBuilder
 
decompile - Variable in class wycs.util.WycsBuildTask
In decompilation mode, the build task will generate wyal files from wycs files (rather than the other way around).
Default(PrintStream) - Constructor for class wycc.util.Logger.Default
 
DEFAULT_OPTIONS - Static variable in class wyc.WycMain
 
DEFAULT_OPTIONS - Static variable in class wycs.WycsMain
 
DEFAULT_OPTIONS - Static variable in class wyjc.WyjcMain
 
DefaultInterpretation - Class in wyautl_old.lang
Provides a standard (ie simplistic) interpretation of automata which provides a suitable base for more complex systems.
DefaultInterpretation() - Constructor for class wyautl_old.lang.DefaultInterpretation
 
DefaultInterpretation.Term - Class in wyautl_old.lang
Represents a term which may be accepted by an automaton under the default interpretation.
defaultPipeline - Static variable in class wyc.util.WycBuildTask
 
defaultPipeline - Static variable in class wycs.util.WycsBuildTask
 
DefaultSubsumption - Class in wyautl_old.lang
This default interpretation of subsumption provides a useful starting point for many interpretations.
DefaultSubsumption(Automaton, Automaton) - Constructor for class wyautl_old.lang.DefaultSubsumption
 
defaultTarget - Variable in class wyil.lang.Codes.Switch
 
defaultValue - Variable in class wycc.util.OptArg
A default value for the option (assuming it accepts an argument).
DefineFun(String, List<Pair<String, String>>, String, String) - Constructor for class wycs.solver.smt.Stmt.DefineFun
 
DefineSort(String, List<String>, String) - Constructor for class wycs.solver.smt.Stmt.DefineSort
 
DefiniteAssignmentCheck - Class in wyil.checks
The purpose of this class is to check that all variables are defined before being used.
DefiniteAssignmentCheck(Builder) - Constructor for class wyil.checks.DefiniteAssignmentCheck
 
defs(Code) - Method in class wyil.checks.DefiniteAssignmentCheck
 
denominator - Variable in class wyc.lang.Expr.RationalLVal
 
denominator - Variable in class wyc.lang.TypePattern.Rational
 
denominator - Variable in class wycs.syntax.TypePattern.Rational
 
denominator() - Method in class wyjc.runtime.WyRat
 
dependencies() - Method in interface wyfs.lang.Path.Entry
Return those entries (if any) upon which this entry depends.
dependencies() - Method in class wyfs.util.AbstractEntry
 
dependents() - Method in interface wyfs.lang.Path.Entry
Return those entries (if any) which depend upon this entry.
dependents() - Method in class wyfs.util.AbstractEntry
 
Dereference(Expr, Attribute...) - Constructor for class wyc.lang.Expr.Dereference
 
Dereference(Type.Reference, int, int) - Static method in class wyil.lang.Codes
 
describeAttributes() - Static method in class wyil.io.WyilFilePrinter
 
describeDebug() - Static method in class wycs.transforms.SmtVerificationCheck
Gets the description of the debug option.
describeDebug() - Static method in class wycs.transforms.VerificationCheck
 
describeEnable() - Static method in class wycs.transforms.MacroExpansion
 
describeEnable() - Static method in class wycs.transforms.SmtVerificationCheck
Gets the description of the enable option.
describeEnable() - Static method in class wycs.transforms.TypePropagation
 
describeEnable() - Static method in class wycs.transforms.VerificationCheck
 
describeEnable() - Static method in class wyil.checks.DefiniteAssignmentCheck
 
describeEnable() - Static method in class wyil.transforms.ConstantPropagation
 
describeEnable() - Static method in class wyil.transforms.DeadCodeElimination
 
describeEnable() - Static method in class wyil.transforms.LiveVariablesAnalysis
 
describeEnable() - Static method in class wyil.transforms.LoopVariants
 
describeLabels() - Static method in class wyil.io.WyilFilePrinter
 
describeMaxInferences() - Static method in class wycs.transforms.VerificationCheck
 
describeNops() - Static method in class wyil.transforms.LiveVariablesAnalysis
 
describeRwMode() - Static method in class wycs.transforms.VerificationCheck
 
describeSlots() - Static method in class wyil.io.WyilFilePrinter
 
describeSolver() - Static method in class wycs.transforms.SmtVerificationCheck
Gets the description of the solver option.
description - Variable in class wycc.util.OptArg
A description of the option.
destruct(Type) - Static method in class wyil.lang.Type
Destruct is the opposite of construct.
deterministic - Variable in class wyautl_old.lang.Automaton.State
 
DETERMINISTIC - Variable in class wyautl_old.util.Generator.Kind
Determine whether this kind is deterministic or not.
Dictionary(WyType, WyType) - Constructor for class wyjc.runtime.WyType.Dictionary
 
difference(Value.Array) - Method in class wycs.core.Value.Array
 
DirectoryRoot - Class in wyfs.util
Provides an implementation of Path.Root for representing a file system directory.
DirectoryRoot(String, Content.Registry) - Constructor for class wyfs.util.DirectoryRoot
Construct a directory root from a filesystem path expressed as a string, and an appropriate file filter.
DirectoryRoot(String, FileFilter, Content.Registry) - Constructor for class wyfs.util.DirectoryRoot
Construct a directory root from a filesystem path expressed as a string, and an appropriate file filter.
DirectoryRoot(File, Content.Registry) - Constructor for class wyfs.util.DirectoryRoot
Construct a directory root from a filesystem path expressed as a string, and an appropriate file filter.
DirectoryRoot(File, FileFilter, Content.Registry) - Constructor for class wyfs.util.DirectoryRoot
Construct a directory root from a filesystem path expressed as a string, and an appropriate file filter.
DirectoryRoot.Entry<T> - Class in wyfs.util
An entry is a file on the file system which represents a Whiley module.
DirectoryRoot.Folder - Class in wyfs.util
Represents a directory on a physical file system.
Div(Automaton, int...) - Static method in class wycs.solver.Solver
 
Div(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
Div(Automaton, int, int) - Static method in class wycs.solver.SolverUtil
Construct an automaton node representing the multiplication of two arithmetic expressions.
divide(Value.Decimal) - Method in class wycs.core.Value.Decimal
 
divide(Value.Integer) - Method in class wycs.core.Value.Integer
 
divide(Constant.Decimal) - Method in class wyil.lang.Constant.Decimal
 
divide(Constant.Integer) - Method in class wyil.lang.Constant.Integer
 
divide(Constant.Rational) - Method in class wyil.lang.Constant.Rational
 
divide(int) - Method in class wyjc.runtime.WyRat
 
divide(long) - Method in class wyjc.runtime.WyRat
 
divide(BigInteger) - Method in class wyjc.runtime.WyRat
 
divide(WyRat) - Method in class wyjc.runtime.WyRat
 
divideByZeroCheck(Codes.BinaryOperator, VcBranch) - Method in class wyil.builders.VcGenerator
Generate preconditions to protected against a possible divide by zero.
doubleValue() - Method in class wyjc.runtime.WyRat
 
DoWhile(Expr, List<Expr>, Collection<Stmt>, Attribute...) - Constructor for class wyc.lang.Stmt.DoWhile
Construct a Do-While statement from a given condition and body of statements.
DoWhile(Expr, List<Expr>, Collection<Stmt>, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.DoWhile
Construct a Do-While statement from a given condition and body of statements.
DUPLICATE_CASE_LABEL - Static variable in class wyil.util.ErrorMessages
 
DUPLICATE_DEFAULT_LABEL - Static variable in class wyil.util.ErrorMessages
 

E

effectiveFunctionOrMethod(Type) - Static method in class wyil.lang.Type
 
effectiveReference(Type) - Static method in class wyil.lang.Type
 
element - Variable in class wyc.lang.Expr.ArrayGenerator
 
element() - Method in class wyc.lang.Nominal.List
 
element() - Method in class wyc.lang.Nominal.Reference
 
element(int) - Method in class wyc.lang.Nominal.Tuple
 
element - Variable in class wyc.lang.SyntacticType.Array
 
element - Variable in class wyc.lang.SyntacticType.Negation
 
element - Variable in class wyc.lang.SyntacticType.Reference
 
element() - Method in class wycs.core.SemanticType.Array
 
element(int) - Method in class wycs.core.SemanticType.Nary
 
element() - Method in class wycs.core.SemanticType.Not
 
Element - Interface in wycs.solver.smt
An element in a Smt2File.
element - Variable in class wycs.syntax.SyntacticType.List
 
element - Variable in class wycs.syntax.SyntacticType.Negation
 
element - Variable in class wycs.syntax.SyntacticType.Reference
 
element() - Method in class wyil.lang.Type.Array
 
element() - Method in interface wyil.lang.Type.EffectiveArray
 
element(int) - Method in interface wyil.lang.Type.EffectiveTuple
 
element() - Method in class wyil.lang.Type.Negation
 
element() - Method in class wyil.lang.Type.Reference
 
element(int) - Method in class wyil.lang.Type.Tuple
 
element() - Method in class wyil.lang.Type.UnionOfArrays
 
element(int) - Method in class wyil.lang.Type.UnionOfTuples
 
element - Variable in class wyjc.runtime.WyType.List
 
element - Variable in class wyjc.runtime.WyType.Negation
 
element - Variable in class wyjc.runtime.WyType.Reference
 
element - Variable in class wyjc.runtime.WyType.Set
 
elements() - Method in class wyc.lang.Nominal.Tuple
 
elements - Variable in class wyc.lang.TypePattern.Intersection
 
elements - Variable in class wyc.lang.TypePattern.Record
 
elements - Variable in class wyc.lang.TypePattern.Tuple
 
elements - Variable in class wyc.lang.TypePattern.Union
 
elements() - Method in class wycs.core.SemanticType.Nary
 
elements - Variable in class wycs.syntax.SyntacticType.Intersection
 
elements - Variable in class wycs.syntax.SyntacticType.Record
 
elements - Variable in class wycs.syntax.SyntacticType.Tuple
 
elements - Variable in class wycs.syntax.SyntacticType.Union
 
elements - Variable in class wycs.syntax.TypePattern.Intersection
 
elements - Variable in class wycs.syntax.TypePattern.Record
 
elements - Variable in class wycs.syntax.TypePattern.Tuple
 
elements - Variable in class wycs.syntax.TypePattern.Union
 
elements() - Method in interface wyil.lang.Type.EffectiveTuple
 
elements() - Method in class wyil.lang.Type.Tuple
 
elements() - Method in class wyil.lang.Type.UnionOfTuples
 
end() - Method in class wyc.io.WhileyFileLexer.Token
 
end() - Method in class wycc.io.Token
Get the last position in the original stream which contains a character from this token.
end - Variable in class wycc.lang.Attribute.Origin
 
end - Variable in class wycc.lang.Attribute.Source
 
end() - Method in exception wycc.lang.SyntaxError
Get index of last character of offending location.
end() - Method in class wycs.io.WyalFileLexer.Token
 
end() - Method in class wyil.attributes.SourceLocation
 
endOperand - Variable in class wyil.lang.Codes.Quantify
 
ensures - Variable in class wyc.lang.WhileyFile.FunctionOrMethod
 
Entry(Path.ID, File) - Constructor for class wyfs.util.DirectoryRoot.Entry
 
Entry(Path.ID, Content.Registry) - Constructor for class wyfs.util.VirtualRoot.Entry
 
Env() - Constructor for class wyil.transforms.ConstantPropagation.Env
 
Env(Collection<Constant>) - Constructor for class wyil.transforms.ConstantPropagation.Env
 
Env() - Constructor for class wyil.transforms.LiveVariablesAnalysis.Env
 
Env(LiveVariablesAnalysis.Env) - Constructor for class wyil.transforms.LiveVariablesAnalysis.Env
 
Environment() - Constructor for class wyc.builder.CodeGenerator.Environment
 
Environment(CodeGenerator.Environment) - Constructor for class wyc.builder.CodeGenerator.Environment
 
equals(Object) - Method in class wyautl_old.lang.Automaton
This method compares two compound types to test whether they are identical.
equals(Object) - Method in class wyautl_old.lang.Automaton.State
 
equals(Object) - Method in class wyautl_old.lang.DefaultInterpretation.Term
 
equals(Object) - Method in class wyc.lang.Nominal.Base
 
equals(Object) - Method in class wyc.lang.Nominal.Function
 
equals(Object) - Method in class wyc.lang.Nominal.List
 
equals(Object) - Method in class wyc.lang.Nominal.Method
 
equals(Object) - Method in class wyc.lang.Nominal.Record
 
equals(Object) - Method in class wyc.lang.Nominal.Reference
 
equals(Object) - Method in class wyc.lang.Nominal.Tuple
 
equals(Object) - Method in class wycc.lang.NameID
 
equals(Object) - Method in class wycc.util.Pair
 
equals(Object) - Method in class wycc.util.Triple
 
equals(Object) - Method in class wycs.core.SemanticType
 
equals(Object) - Method in class wycs.core.Value.Array
 
equals(Object) - Method in class wycs.core.Value.Bool
 
equals(Object) - Method in class wycs.core.Value.Decimal
 
equals(Object) - Method in class wycs.core.Value.Integer
 
equals(Object) - Method in class wycs.core.Value.Null
 
equals(Object) - Method in class wycs.core.Value.String
 
equals(Object) - Method in class wycs.core.Value.Tuple
 
equals(Object) - Method in class wycs.solver.smt.Stmt.Assert
equals(Object) - Method in class wycs.solver.smt.Stmt.DeclareFun
equals(Object) - Method in class wycs.solver.smt.Stmt.DeclareSort
equals(Object) - Method in class wycs.solver.smt.Stmt.DefineFun
equals(Object) - Method in class wycs.solver.smt.Stmt.DefineSort
equals(Object) - Method in class wycs.solver.smt.Stmt.Exit
 
Equals(Automaton, int...) - Static method in class wycs.solver.Solver
 
Equals(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
Equals(Automaton, int, int, int) - Static method in class wycs.solver.SolverUtil
Construct an automaton node representing the equality of two expressions.
equals(Object) - Method in class wyfs.util.Trie
 
equals(Object) - Method in class wyil.lang.Code.AbstractBinaryOp
 
equals(Object) - Method in class wyil.lang.Code.AbstractNaryAssignable
 
equals(Object) - Method in class wyil.lang.Code.AbstractUnaryOp
 
equals(Object) - Method in class wyil.lang.CodeBlock.Index
 
equals(Object) - Method in class wyil.lang.Codes.Assert
 
equals(Object) - Method in class wyil.lang.Codes.Assign
 
equals(Object) - Method in class wyil.lang.Codes.Assume
 
equals(Object) - Method in class wyil.lang.Codes.BinaryOperator
 
equals(Object) - Method in class wyil.lang.Codes.Const
 
equals(Object) - Method in class wyil.lang.Codes.Convert
 
equals(Object) - Method in class wyil.lang.Codes.Debug
 
equals(Object) - Method in class wyil.lang.Codes.Dereference
 
equals(Object) - Method in class wyil.lang.Codes.FieldLoad
 
equals(Object) - Method in class wyil.lang.Codes.Goto
 
equals(Object) - Method in class wyil.lang.Codes.If
 
equals(Object) - Method in class wyil.lang.Codes.IfIs
 
equals(Object) - Method in class wyil.lang.Codes.IndexOf
 
equals(Object) - Method in class wyil.lang.Codes.IndirectInvoke
 
equals(Object) - Method in class wyil.lang.Codes.Invariant
 
equals(Object) - Method in class wyil.lang.Codes.Invert
 
equals(Object) - Method in class wyil.lang.Codes.Invoke
 
equals(Object) - Method in class wyil.lang.Codes.Label
 
equals(Object) - Method in class wyil.lang.Codes.Lambda
 
equals(Object) - Method in class wyil.lang.Codes.LengthOf
 
equals(Object) - Method in class wyil.lang.Codes.ListGenerator
 
equals(Object) - Method in class wyil.lang.Codes.Loop
 
equals(Object) - Method in class wyil.lang.Codes.Move
 
equals(Object) - Method in class wyil.lang.Codes.NewList
 
equals(Object) - Method in class wyil.lang.Codes.NewObject
 
equals(Object) - Method in class wyil.lang.Codes.NewRecord
 
equals(Object) - Method in class wyil.lang.Codes.NewTuple
 
equals(Object) - Method in class wyil.lang.Codes.Not
 
equals(Object) - Method in class wyil.lang.Codes.Quantify
 
equals(Object) - Method in class wyil.lang.Codes.Return
 
equals(Object) - Method in class wyil.lang.Codes.Switch
 
equals(Object) - Method in class wyil.lang.Codes.TupleLoad
 
equals(Object) - Method in class wyil.lang.Codes.UnaryOperator
 
equals(Object) - Method in class wyil.lang.Codes.Update
 
equals(Object) - Method in class wyil.lang.Codes.Void
 
equals(Object) - Method in class wyil.lang.Constant.Bool
 
equals(Object) - Method in class wyil.lang.Constant.Byte
 
equals(Object) - Method in class wyil.lang.Constant.Decimal
 
equals(Object) - Method in class wyil.lang.Constant.Integer
 
equals(Object) - Method in class wyil.lang.Constant.Lambda
 
equals(Object) - Method in class wyil.lang.Constant.List
 
equals(Object) - Method in class wyil.lang.Constant.Null
 
equals(Object) - Method in class wyil.lang.Constant.Rational
 
equals(Object) - Method in class wyil.lang.Constant.Record
 
equals(Object) - Method in class wyil.lang.Constant.Tuple
 
equals(Object) - Method in class wyil.lang.Constant.Type
 
equals(Object) - Method in class wyil.lang.Type.Any
 
equals(Object) - Method in class wyil.lang.Type.Bool
 
equals(Object) - Method in class wyil.lang.Type.Byte
 
equals(Object) - Method in class wyil.lang.Type.Compound
 
equals(Object) - Method in class wyil.lang.Type.Int
 
equals(Object) - Method in class wyil.lang.Type.Meta
 
equals(Object) - Method in class wyil.lang.Type.Nominal
 
equals(Object) - Method in class wyil.lang.Type.Null
 
equals(Object) - Method in class wyil.lang.Type.Real
 
equals(Object) - Method in class wyil.lang.Type.Record.State
 
equals(Object) - Method in class wyil.lang.Type.Void
 
equals(Object, Object) - Static method in class wyjc.runtime.Util
This method is used for the special case when the left-hand side of an equality operation may be null.
equals(Object) - Method in class wyjc.runtime.WyBool
 
equals(Object) - Method in class wyjc.runtime.WyByte
 
equals(Object) - Method in class wyjc.runtime.WyRat
 
Equation(Automaton, int...) - Static method in class wycs.solver.Solver
 
Equation(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
equivalent(Expr) - Method in class wycs.syntax.Expr.Binary
 
equivalent(Expr) - Method in class wycs.syntax.Expr.Cast
 
equivalent(Expr) - Method in class wycs.syntax.Expr.Constant
 
equivalent(Expr) - Method in class wycs.syntax.Expr.ConstantAccess
 
equivalent(Expr) - Method in class wycs.syntax.Expr
 
equivalent(List<SyntacticType>, List<SyntacticType>) - Static method in class wycs.syntax.Expr
 
equivalent(Expr) - Method in class wycs.syntax.Expr.FieldAccess
 
equivalent(Expr) - Method in class wycs.syntax.Expr.IndexOf
 
equivalent(Expr) - Method in class wycs.syntax.Expr.IndirectInvoke
 
equivalent(Expr) - Method in class wycs.syntax.Expr.Invoke
 
equivalent(Expr) - Method in class wycs.syntax.Expr.Is
 
equivalent(Expr) - Method in class wycs.syntax.Expr.Nary
 
equivalent(Expr) - Method in class wycs.syntax.Expr.Quantifier
 
equivalent(Expr) - Method in class wycs.syntax.Expr.Record
 
equivalent(Expr) - Method in class wycs.syntax.Expr.Unary
 
equivalent(Expr) - Method in class wycs.syntax.Expr.Variable
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Any
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Bool
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Byte
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Char
 
equivalent(SyntacticType) - Method in interface wycs.syntax.SyntacticType
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Function
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Int
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Intersection
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.List
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Negation
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Nominal
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Null
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Real
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Record
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Reference
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Strung
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Tuple
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Union
 
equivalent(List<SyntacticType>, List<SyntacticType>) - Static method in class wycs.syntax.SyntacticType.Util
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Variable
 
equivalent(SyntacticType) - Method in class wycs.syntax.SyntacticType.Void
 
equivalent(TypePattern) - Method in class wycs.syntax.TypePattern
 
equivalent(List<? extends TypePattern>, List<? extends TypePattern>) - Static method in class wycs.syntax.TypePattern
 
equivalent(TypePattern) - Method in class wycs.syntax.TypePattern.Intersection
 
equivalent(TypePattern) - Method in class wycs.syntax.TypePattern.Leaf
 
equivalent(TypePattern) - Method in class wycs.syntax.TypePattern.Rational
 
equivalent(TypePattern) - Method in class wycs.syntax.TypePattern.Record
 
equivalent(TypePattern) - Method in class wycs.syntax.TypePattern.Tuple
 
equivalent(TypePattern) - Method in class wycs.syntax.TypePattern.Union
 
Error(String, int) - Constructor for exception wycc.io.AbstractLexer.Error
 
errorMessage(ErrorMessages.MsgWithNoParams) - Static method in class wyil.util.ErrorMessages
Return the error message for an error with no parameters.
errorMessage(ErrorMessages.MsgWithStringParam, String) - Static method in class wyil.util.ErrorMessages
Return the error message for an error with a single string parameter.
errorMessage(ErrorMessages.MsgWithTypeParam, Type) - Static method in class wyil.util.ErrorMessages
Return the error message for an error with a single type parameter.
errorMessage(ErrorMessages.MsgWithTypeParams, Type, Type) - Static method in class wyil.util.ErrorMessages
Return the error message for an error with two type parameters.
ErrorMessages - Class in wyil.util
Contains global constants mapping syntax errors to their error messages.
ErrorMessages() - Constructor for class wyil.util.ErrorMessages
 
errout - Static variable in class wycs.WycsMain
 
errout - Static variable in class wyil.Main
 
execute() - Method in class wyc.util.WycAntTask
 
execute() - Method in class wycs.util.WycsAntTask
 
execute(NameID, Type.FunctionOrMethod, Constant...) - Method in class wyil.util.Interpreter
Execute a function or method identified by a name and type signature with the given arguments, producing a return value or null (if none).
exists(Path.ID, Content.Type<?>) - Method in interface wybs.lang.Build.Project
Check whether or not a given entry and content-type is contained in this root.
exists(Path.ID, Content.Type<?>) - Method in class wybs.util.StdProject
Check whether or not a given entry and content-type is contained in this root.
exists(Path.ID) - Method in class wyc.builder.WhileyBuilder
 
exists(Path.ID) - Method in class wycs.builders.Wyal2WycsBuilder
Check whether or not a given Wycs module exists.
Exists(Automaton, int...) - Static method in class wycs.solver.Solver
 
Exists(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
Exists(TypePattern, Expr, Attribute...) - Constructor for class wycs.syntax.Expr.Exists
 
Exists(TypePattern, Expr, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.Exists
 
exists(Path.ID, Content.Type<?>) - Method in interface wyfs.lang.Path.Folder
folder) and content-type is contained in this folder.
exists(Path.ID, Content.Type<?>) - Method in interface wyfs.lang.Path.Root
Check whether or not a given entry and content-type is contained in this root.
exists(Path.ID, Content.Type<?>) - Method in class wyfs.util.AbstractFolder
 
exists(Path.ID, Content.Type<?>) - Method in class wyfs.util.AbstractRoot
 
Exit() - Constructor for class wycs.solver.smt.Stmt.Exit
 
expand(SemanticType, boolean, WyalFile.Context) - Method in class wycs.builders.Wyal2WycsBuilder
Expand a semantic type by expanding all nominal types it contains with their underlying type.
expandAsEffectiveList(Nominal) - Method in class wyc.builder.FlowTypeChecker
 
expandAsEffectiveRecord(Nominal) - Method in class wyc.builder.FlowTypeChecker
 
expandAsEffectiveTuple(Nominal) - Method in class wyc.builder.FlowTypeChecker
 
expandAsFunctionOrMethod(Nominal) - Method in class wyc.builder.FlowTypeChecker
 
expandAsReference(Nominal) - Method in class wyc.builder.FlowTypeChecker
 
expander - Variable in class wyjc.Wyil2JavaBuilder
The type expander is useful for managing nominal types and converting them into their underlying types.
ExplicitCoercionOperator - Class in wyil.util.type
The explicit coercion operator extends the implicit coercion operator to include coercions which must be specified with an explicit cast operation.
ExplicitCoercionOperator(Automaton, Automaton) - Constructor for class wyil.util.type.ExplicitCoercionOperator
 
EXPORT - Static variable in interface wyil.lang.Modifier
 
Expr - Interface in wyc.lang
Provides classes for representing expressions in Whiley's source language.
expr - Variable in class wyc.lang.Expr.Cast
 
expr - Variable in class wyc.lang.Expr.New
 
expr - Variable in class wyc.lang.Stmt.Assert
 
expr - Variable in class wyc.lang.Stmt.Assume
 
expr - Variable in class wyc.lang.Stmt.Case
 
expr - Variable in class wyc.lang.Stmt.Debug
 
expr - Variable in class wyc.lang.Stmt.Return
 
expr - Variable in class wyc.lang.Stmt.Switch
 
expr - Variable in class wyc.lang.Stmt.VariableDeclaration
 
Expr - Class in wycs.syntax
 
Expr(Attribute...) - Constructor for class wycs.syntax.Expr
 
Expr(Collection<Attribute>) - Constructor for class wycs.syntax.Expr
 
expr - Variable in class wycs.syntax.WyalFile.Assert
 
expr - Variable in class wycs.syntax.WyalFile.Assume
 
Expr.AbstractFunctionOrMethod - Class in wyc.lang
 
Expr.AbstractIndirectInvoke - Class in wyc.lang
 
Expr.AbstractInvoke - Class in wyc.lang
 
Expr.AbstractVariable - Class in wyc.lang
 
Expr.ArrayGenerator - Class in wyc.lang
Represents an array generator expression, which is of the form:
Expr.ArrayInitialiser - Class in wyc.lang
Represents an array initialiser expression, which is of the form:
Expr.AssignedVariable - Class in wyc.lang
 
Expr.Binary - Class in wycs.syntax
 
Expr.Binary.Op - Enum in wycs.syntax
 
Expr.BinOp - Class in wyc.lang
 
Expr.BOp - Enum in wyc.lang
 
Expr.Cast - Class in wyc.lang
Represents a cast expression, which has the form:
Expr.Cast - Class in wycs.syntax
 
Expr.Constant - Class in wyc.lang
 
Expr.Constant - Class in wycs.syntax
 
Expr.ConstantAccess - Class in wyc.lang
 
Expr.ConstantAccess - Class in wycs.syntax
 
Expr.Dereference - Class in wyc.lang
 
Expr.Exists - Class in wycs.syntax
 
Expr.FieldAccess - Class in wyc.lang
 
Expr.FieldAccess - Class in wycs.syntax
 
Expr.ForAll - Class in wycs.syntax
 
Expr.FunctionCall - Class in wyc.lang
Parse a function invocation expression, which has the form:
Expr.FunctionOrMethod - Class in wyc.lang
 
Expr.IndexOf - Class in wyc.lang
 
Expr.IndexOf - Class in wycs.syntax
 
Expr.IndirectFunctionCall - Class in wyc.lang
 
Expr.IndirectInvoke - Class in wycs.syntax
 
Expr.IndirectMethodCall - Class in wyc.lang
 
Expr.Invoke - Class in wycs.syntax
 
Expr.Is - Class in wycs.syntax
 
Expr.Lambda - Class in wyc.lang
 
Expr.LengthOf - Class in wyc.lang
 
Expr.LocalVariable - Class in wyc.lang
 
Expr.LVal - Interface in wyc.lang
An LVal is a special form of expression which may appear on the left-hand side of an assignment.
Expr.MethodCall - Class in wyc.lang
 
Expr.Nary - Class in wycs.syntax
 
Expr.Nary.Op - Enum in wycs.syntax
 
Expr.New - Class in wyc.lang
 
Expr.QOp - Enum in wyc.lang
 
Expr.Quantifier - Class in wyc.lang
 
Expr.Quantifier - Class in wycs.syntax
 
Expr.RationalLVal - Class in wyc.lang
 
Expr.Record - Class in wyc.lang
 
Expr.Record - Class in wycs.syntax
 
Expr.Tuple - Class in wyc.lang
 
Expr.TypeVal - Class in wyc.lang
 
Expr.Unary - Class in wycs.syntax
 
Expr.Unary.Op - Enum in wycs.syntax
 
Expr.UnOp - Class in wyc.lang
 
Expr.UOp - Enum in wyc.lang
 
Expr.Variable - Class in wycs.syntax
 
Exprs - Class in wyc.lang
 
Exprs() - Constructor for class wyc.lang.Exprs
 
EXTRA_OPTIONS - Static variable in class wyjc.WyjcMain
 
extract(Automaton, int) - Static method in class wyautl_old.lang.Automata
Traverse the automaton rooted at the given state and recursively extract all reachable states to produce a (potentially smaller) automaton.
extract(int) - Method in class wycs.core.SemanticType
Extract the type described by a given node in the automaton.
extractOnto(int, Automaton, ArrayList<Automaton.State>) - Static method in class wyautl_old.lang.Automata
 
extractQuantifiers(Codes.Quantify, VcBranch, VcBranch, List<VcBranch>) - Method in class wyil.builders.VcGenerator
This extracts quantifiers from exit branches of a forall loop.
extractUniversals(Code) - Static method in class wycs.core.NormalForms
 

F

Fail() - Static method in class wyil.lang.Codes
Construct a fail bytecode which halts execution by raising a fault.
False - Static variable in class wycs.solver.Solver
 
FALSE - Static variable in class wyjc.runtime.WyBool
 
falseBranch - Variable in class wyc.lang.Stmt.IfElse
 
field(String) - Method in class wyc.lang.Nominal.Record
 
field - Variable in class wyil.lang.Codes.FieldLoad
 
field - Variable in class wyil.lang.Codes.RecordLVal
 
field(String) - Method in interface wyil.lang.Type.EffectiveRecord
 
field(String) - Method in class wyil.lang.Type.Record
 
field(String) - Method in class wyil.lang.Type.UnionOfRecords
 
FieldAccess(Expr, String, Attribute...) - Constructor for class wyc.lang.Expr.FieldAccess
 
FieldAccess(Expr, String, Collection<Attribute>) - Constructor for class wyc.lang.Expr.FieldAccess
 
FieldAccess(Expr, String, Attribute...) - Constructor for class wycs.syntax.Expr.FieldAccess
 
FieldAccess(Expr, String, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.FieldAccess
 
FieldLoad(Type.EffectiveRecord, int, int, String) - Static method in class wyil.lang.Codes
Construct a fieldload bytecode which reads a given field from a record of a given type.
fields - Variable in class wyc.lang.Expr.Record
 
fields - Variable in class wyc.lang.Expr.Tuple
 
fields() - Method in class wyc.lang.Nominal.Record
 
fields - Variable in class wyil.lang.Codes.Update
 
fields() - Method in interface wyil.lang.Type.EffectiveRecord
 
fields() - Method in class wyil.lang.Type.Record
Return a mapping from field names to their types.
fields() - Method in class wyil.lang.Type.UnionOfRecords
 
fieldType() - Method in class wyil.lang.Codes.FieldLoad
 
file() - Method in interface wyc.lang.WhileyFile.Context
 
FILE - Static variable in class wycc.util.OptArg
 
file() - Method in class wycs.syntax.WyalFile.AbstractContext
 
file() - Method in interface wycs.syntax.WyalFile.Context
 
file() - Method in class wyfs.util.DirectoryRoot.Entry
 
FILEDIR - Static variable in class wycc.util.OptArg
 
FILELIST - Static variable in class wycc.util.OptArg
 
filename - Variable in class wyc.lang.WhileyFile
 
filename - Variable in class wycc.lang.Attribute.Origin
 
filename() - Method in exception wycc.lang.SyntaxError
Filename for file where the error arose.
filename() - Method in class wycs.core.WycsFile
 
filename() - Method in class wycs.syntax.WyalFile
 
filename() - Method in class wyil.lang.WyilFile
Returns the originating source file for this WyilFile.
filename - Variable in class wyil.util.dfa.BackwardFlowAnalysis
The filename of the module currently being propagated through
filename - Variable in class wyil.util.dfa.ForwardFlowAnalysis
The filename of the module currently being propagated through
filename - Variable in class wyjc.Wyil2JavaBuilder
Filename of module being translated
Filter - Class in wyautl_old.util
 
Filter() - Constructor for class wyautl_old.util.Filter
 
filter - Variable in class wyc.lang.WhileyFile.Import
 
filter - Variable in class wycs.syntax.WyalFile.Import
 
filter(Path.Filter, Content.Type<T>) - Static method in class wyfs.lang.Content
Construct a content filter from a path filter and a content type.
filter(String, Content.Type<T>) - Static method in class wyfs.lang.Content
Construct a content filter from a string representing a path filter and a content type.
find(List<File>, Content.Type<T>) - Method in class wyfs.util.DirectoryRoot
Given a list of physical files on the file system, determine their corresponding Path.Entry instances in this root (if there are any).
findPostcondition(NameID, Type.FunctionOrMethod, AttributedCodeBlock, VcBranch) - Method in class wyil.builders.VcGenerator
Find the postcondition associated with a given function or method.
findPrecondition(NameID, Type.FunctionOrMethod, AttributedCodeBlock, VcBranch) - Method in class wyil.builders.VcGenerator
Find the precondition associated with a given function or method.
first - Variable in class wycc.util.Pair
 
first() - Method in class wycc.util.Pair
 
firstWithin() - Method in class wyil.lang.CodeBlock.Index
Return the first index nested within this index.
floatValue() - Method in class wyjc.runtime.WyRat
 
floor() - Method in class wyjc.runtime.WyRat
 
FlowTypeChecker - Class in wyc.builder
Propagates type information in a flow-sensitive fashion from declared parameter and return types through variable declarations and assigned expressions, to determine types for all intermediate expressions and variables.
FlowTypeChecker(WhileyBuilder) - Constructor for class wyc.builder.FlowTypeChecker
 
flush() - Method in class wyautl_old.io.BinaryAutomataWriter
 
flush() - Method in interface wyautl_old.io.GenericWriter
 
flush() - Method in class wyautl_old.io.TextAutomataWriter
 
flush() - Method in class wybs.util.StdProject
Force root to flush entries to permanent storage (where appropriate).
flush() - Method in class wyc.util.WycBuildTask
Flush all built files to disk.
flush() - Method in class wycs.util.WycsBuildTask
Flush all built files to disk.
flush() - Method in class wyfs.io.BinaryOutputStream
 
flush() - Method in interface wyfs.lang.Path.Item
Force item to write contents to permanent storage (where appropriate).
flush() - Method in interface wyfs.lang.Path.Root
Force root to flush entries to permanent storage (where appropriate).
flush() - Method in class wyfs.util.AbstractEntry
 
flush() - Method in class wyfs.util.AbstractFolder
 
flush() - Method in class wyfs.util.AbstractRoot
 
flush() - Method in class wyfs.util.JarFileRoot
 
flush() - Method in class wyil.util.type.TypeGenerator.TextTypeWriter
 
flush() - Method in class wyjc.util.WyjcBuildTask
 
FMT_BINARYASSIGN - Static variable in interface wyil.lang.Code
 
FMT_BINARYOP - Static variable in interface wyil.lang.Code
 
FMT_EMPTY - Static variable in interface wyil.lang.Code
 
FMT_MASK - Static variable in interface wyil.lang.Code
 
FMT_NARYASSIGN - Static variable in interface wyil.lang.Code
 
FMT_NARYOP - Static variable in interface wyil.lang.Code
 
FMT_OTHER - Static variable in interface wyil.lang.Code
 
FMT_SHIFT - Static variable in interface wyil.lang.Code
 
FMT_UNARYASSIGN - Static variable in interface wyil.lang.Code
 
FMT_UNARYOP - Static variable in interface wyil.lang.Code
 
Fn(Automaton, int...) - Static method in class wycs.solver.Solver
 
Fn(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
Folder(Path.ID) - Constructor for class wyfs.util.DirectoryRoot.Folder
 
Folder(Path.ID) - Constructor for class wyfs.util.JarFileRoot.Folder
 
Folder(Path.ID) - Constructor for class wyfs.util.VirtualRoot.Folder
 
ForAll(Automaton, int...) - Static method in class wycs.solver.Solver
 
ForAll(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
ForAll(TypePattern, Expr, Attribute...) - Constructor for class wycs.syntax.Expr.ForAll
 
ForAll(TypePattern, Expr, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.ForAll
 
fork() - Method in class wyil.builders.VcBranch
Fork this branch into a child branch with this branch as parent.
ForwardFlowAnalysis<T> - Class in wyil.util.dfa
 
ForwardFlowAnalysis() - Constructor for class wyil.util.dfa.ForwardFlowAnalysis
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.Binary
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.Cast
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.Constant
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.ConstantAccess
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.FieldAccess
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.IndexOf
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.IndirectInvoke
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.Invoke
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.Is
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.Nary
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.Quantifier
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.Record
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.Unary
 
freeVariables(Set<String>) - Method in class wycs.syntax.Expr.Variable
 
freshLabel() - Static method in class wyil.lang.CodeUtils
 
freshLabel() - Method in class wyjc.Wyil2JavaBuilder
 
from() - Method in class wyautl_old.lang.DefaultSubsumption
 
from() - Method in interface wyautl_old.lang.Relation
Get the automaton in the "from" position.
from() - Method in class wycs.core.SemanticType.Function
 
from - Variable in class wycs.syntax.WyalFile.Function
 
from - Variable in class wycs.syntax.WyalFile.Macro
 
from - Variable in class wyil.util.type.SubtypeOperator
 
fromString(String) - Static method in class wycc.lang.NameID
Create a NameID from a string representation.
fromString(String) - Static method in class wyfs.util.Trie
Construct a Trie from a string, where '/' is the separator.
fromString(Path.ID) - Static method in class wyfs.util.Trie
Construct a Trie from a Path ID.
fromString(Path.ID, String) - Static method in class wyfs.util.Trie
Construct a Trie by appending a string onto a Path ID.
fromString(String) - Static method in class wyil.lang.Type
The following code converts a "type string" into an actual type.
fromStringList(String[]) - Static method in class wyjc.runtime.Util
This method is used to convert the arguments supplied to main (which have type String[]) into an appropriate Whiley List.
FUN_ADD_NAME - Static variable in class wycs.solver.smt.Sort.Set
 
FUN_CONTAINS_NAME - Static variable in class wycs.solver.smt.Sort.Set
 
FUN_EMPTY_NAME - Static variable in class wycs.solver.smt.Sort.Set
 
FUN_GET_NAME - Static variable in class wycs.solver.smt.Sort.Tuple
 
FUN_LENGTH_NAME - Static variable in class wycs.solver.smt.Sort.Set
 
FUN_REMOVE_NAME - Static variable in class wycs.solver.smt.Sort.Set
 
FUN_SUBSET_NAME - Static variable in class wycs.solver.smt.Sort.Set
 
FUN_SUBSETEQ_NAME - Static variable in class wycs.solver.smt.Sort.Set
 
FunCall(SemanticType.Function, Code<?>, NameID, SemanticType[], Attribute...) - Static method in class wycs.core.Code
 
FunCall(SemanticType.Function, Code<?>, NameID, SemanticType[], Collection<Attribute>) - Static method in class wycs.core.Code
 
Function(Type.Function, Type.Function) - Constructor for class wyc.lang.Nominal.Function
 
Function(SyntacticType, SyntacticType, Collection<SyntacticType>, Attribute...) - Constructor for class wyc.lang.SyntacticType.Function
 
Function(SyntacticType, SyntacticType, Collection<SyntacticType>, Collection<Attribute>) - Constructor for class wyc.lang.SyntacticType.Function
 
Function(List<Modifier>, String, TypePattern, List<WhileyFile.Parameter>, List<Expr>, List<Expr>, SyntacticType, List<Stmt>, Attribute...) - Constructor for class wyc.lang.WhileyFile.Function
 
Function(SemanticType, SemanticType, SemanticType...) - Static method in class wycs.core.SemanticType
 
Function(String, SemanticType.Function, Code<?>, Attribute...) - Constructor for class wycs.core.WycsFile.Function
 
Function(SyntacticType, SyntacticType, Collection<SyntacticType>, Attribute...) - Constructor for class wycs.syntax.SyntacticType.Function
 
Function(SyntacticType, SyntacticType, Collection<SyntacticType>, Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Function
 
Function(String, List<String>, TypePattern, TypePattern, Expr, Attribute...) - Constructor for class wycs.syntax.WyalFile.Function
 
Function(Type, Type, Collection<Type>) - Static method in class wyil.lang.Type
Construct a function type using the given return and parameter types.
Function(Type, Type, Type...) - Static method in class wyil.lang.Type
Construct a function type using the given return and parameter types.
FunctionCall(NameID, Path.ID, Collection<Expr>, Attribute...) - Constructor for class wyc.lang.Expr.FunctionCall
 
FunctionCall(NameID, Path.ID, Collection<Expr>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.FunctionCall
 
FunctionOrMethod(NameID, Collection<SyntacticType>, Attribute...) - Constructor for class wyc.lang.Expr.FunctionOrMethod
 
FunctionOrMethod(NameID, Collection<SyntacticType>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.FunctionOrMethod
 
FunctionOrMethod() - Constructor for class wyc.lang.Nominal.FunctionOrMethod
 
FunctionOrMethod(SyntacticType, SyntacticType, Collection<SyntacticType>, Attribute...) - Constructor for class wyc.lang.SyntacticType.FunctionOrMethod
 
FunctionOrMethod(SyntacticType, SyntacticType, Collection<SyntacticType>, Collection<Attribute>) - Constructor for class wyc.lang.SyntacticType.FunctionOrMethod
 
FunctionOrMethod(List<Modifier>, String, TypePattern, List<WhileyFile.Parameter>, List<Expr>, List<Expr>, SyntacticType, List<Stmt>, Attribute...) - Constructor for class wyc.lang.WhileyFile.FunctionOrMethod
Construct an object representing a Whiley function.
functionOrMethod(String) - Method in class wyil.lang.WyilFile
Returns all function or method declarations in this WyilFile with the given name.
functionOrMethod(String, Type.FunctionOrMethod) - Method in class wyil.lang.WyilFile
Looks up a function or method declaration in this WyilFile with the given name and type; if none exists, returns null.
FunctionOrMethod(Collection<Modifier>, String, Type.FunctionOrMethod, AttributedCodeBlock, List<AttributedCodeBlock>, List<AttributedCodeBlock>, Attribute...) - Constructor for class wyil.lang.WyilFile.FunctionOrMethod
 
FunctionOrMethod(Collection<Modifier>, String, Type.FunctionOrMethod, AttributedCodeBlock, List<AttributedCodeBlock>, List<AttributedCodeBlock>, Collection<Attribute>) - Constructor for class wyil.lang.WyilFile.FunctionOrMethod
 
functionOrMethods() - Method in class wyil.lang.WyilFile
Returns all function or method declarations in this WyilFile.
FunctionT(Automaton, int...) - Static method in class wycs.core.Types
 
FunctionT(Automaton, List<Integer>) - Static method in class wycs.core.Types
 
FunctionT(Automaton, int...) - Static method in class wycs.solver.Solver
 
FunctionT(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
functionType - Variable in class wyc.lang.Expr.FunctionCall
 
functionType - Variable in class wyc.lang.Expr.IndirectFunctionCall
 

G

gcd(Automaton, Automaton.List) - Static method in class wycs.solver.Solver$native
 
generate(Automaton.State) - Method in interface wyautl_old.util.Generator.Data
Generate all possible forms of supplementary data for the given state.
generate(GenericWriter<Automaton>, Generator.Config) - Static method in class wyautl_old.util.Generator
The generate method generates all possible automata matching of a given size.
generate(WhileyFile) - Method in class wyc.builder.CodeGenerator
Generate a WyilFile from a given WhileyFile by translating all of the declarations, statements and expressions into WyIL declarations and bytecode blocks.
generate(Expr, CodeGenerator.Environment, AttributedCodeBlock, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
Translate a source-level expression into a WYIL bytecode block, using a given environment mapping named variables to registers.
generate(Expr.MethodCall, CodeGenerator.Environment, AttributedCodeBlock, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
 
generate(Expr.MethodCall, int, CodeGenerator.Environment, AttributedCodeBlock, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
 
generate(Expr.FunctionCall, CodeGenerator.Environment, AttributedCodeBlock, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
 
generate(Expr.FunctionCall, int, CodeGenerator.Environment, AttributedCodeBlock, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
 
generate(Expr.IndirectFunctionCall, CodeGenerator.Environment, AttributedCodeBlock, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
 
generate(Expr.IndirectFunctionCall, int, CodeGenerator.Environment, AttributedCodeBlock, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
 
generate(Expr.IndirectMethodCall, CodeGenerator.Environment, AttributedCodeBlock, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
 
generate(Expr.IndirectMethodCall, int, CodeGenerator.Environment, AttributedCodeBlock, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
 
generate(WyalFile) - Method in class wycs.builders.CodeGeneration
 
generate(WyalFile.Declaration) - Method in class wycs.builders.CodeGeneration
 
generate(WyalFile.Macro) - Method in class wycs.builders.CodeGeneration
 
generate(WyalFile.Function) - Method in class wycs.builders.CodeGeneration
 
generate(WyalFile.Type) - Method in class wycs.builders.CodeGeneration
 
generate(WyalFile.Assert) - Method in class wycs.builders.CodeGeneration
 
generate(Expr, HashMap<String, Code>, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
generate(Expr.Variable, HashMap<String, Code>, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
generate(Expr.Constant, HashMap<String, Code>, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
generate(Expr.Cast, HashMap<String, Code>, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
generate(Expr.Unary, HashMap<String, Code>, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
generate(Expr.Binary, HashMap<String, Code>, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
generate(Expr.Nary, HashMap<String, Code>, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
generate(Expr.Quantifier, HashMap<String, Code>, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
generate(Expr.Invoke, HashMap<String, Code>, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
generate(Expr.IndexOf, HashMap<String, Code>, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
generate(Expr.Is, HashMap<String, Code>, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
generate(Object, BigInteger) - Static method in class wyjc.runtime.WyList
 
generateCanonicalisationTests(ArrayList<Automaton>) - Static method in class wyil.util.type.TypeTester
 
generateCondition(String, Expr, CodeGenerator.Environment, AttributedCodeBlock, WhileyFile.Context) - Method in class wyc.builder.CodeGenerator
Translate a source-level condition into a WyIL block, using a given environment mapping named variables to slots.
generateGetFunctionName(int) - Static method in class wycs.solver.smt.Sort.Tuple
 
generateInitialisers() - Method in class wycs.solver.smt.Sort.Any
Generates the required statements to use this generic sort.
generateInitialisers() - Method in class wycs.solver.smt.Sort.Array
Generates the required statements to use this generic sort.
generateInitialisers() - Method in class wycs.solver.smt.Sort.Bool
Generates the required statements to use this generic sort.
generateInitialisers() - Method in class wycs.solver.smt.Sort
Generates the required statements to use this generic sort.
generateInitialisers() - Method in class wycs.solver.smt.Sort.Int
Generates the required statements to use this generic sort.
generateInitialisers() - Method in class wycs.solver.smt.Sort.Real
Generates the required statements to use this generic sort.
generateInitialisers() - Method in class wycs.solver.smt.Sort.Set
Generates the required statements to use this generic sort.
generateInitialisers() - Method in class wycs.solver.smt.Sort.Tuple
Generates the required statements to use this generic sort.
generateSubtypeTests(ArrayList<Automaton>, ArrayList<DefaultInterpretation.Term>) - Static method in class wyil.util.type.TypeTester
 
Generator - Class in wyautl_old.util
The generator class is used generate automata, primarily for testing purposes.
Generator() - Constructor for class wyautl_old.util.Generator
 
Generator.Config - Class in wyautl_old.util
 
Generator.Data - Interface in wyautl_old.util
 
Generator.Kind - Class in wyautl_old.util
 
GenericReader<T> - Interface in wyautl_old.io
An interface for reading specific values from a binary stream.
generics() - Method in class wycs.core.SemanticType.Function
 
generics - Variable in class wycs.syntax.Expr.IndirectInvoke
 
generics - Variable in class wycs.syntax.Expr.Invoke
 
generics - Variable in class wycs.syntax.WyalFile.Function
 
generics - Variable in class wycs.syntax.WyalFile.Macro
 
generics - Variable in class wycs.syntax.WyalFile.Type
 
GenericWriter<T> - Interface in wyautl_old.io
An interface for writing out specific values to a binary stream.
get(int, int) - Method in class wyautl_old.util.BinaryMatrix
 
get(Path.ID, Content.Type<T>) - Method in interface wybs.lang.Build.Project
Get the entry corresponding to a given ID and content type.
get(Content.Filter<T>) - Method in interface wybs.lang.Build.Project
Get all objects matching a given content filter stored in this root.
get(Path.ID, Content.Type<T>) - Method in class wybs.util.StdProject
Get the entry corresponding to a given ID and content type.
get(Content.Filter<T>) - Method in class wybs.util.StdProject
Get all objects matching a given content filter stored in this root.
get(String) - Method in class wyc.builder.CodeGenerator.Environment
 
get(int) - Method in class wyc.builder.CodeGenerator.Environment
 
get(Path.ID, Content.Type<T>) - Method in interface wyfs.lang.Path.Folder
Get the entry corresponding to a given ID (taken relative to this folder) and content type.
get(int) - Method in interface wyfs.lang.Path.ID
Return the component at a given index.
get(Path.ID, Content.Type<T>) - Method in interface wyfs.lang.Path.Root
Get the entry corresponding to a given ID and content type.
get(Content.Filter<T>) - Method in interface wyfs.lang.Path.Root
Get all objects matching a given content filter stored in this root.
get(Path.ID, Content.Type<T>) - Method in class wyfs.util.AbstractFolder
 
get(Path.ID, Content.Type<T>) - Method in class wyfs.util.AbstractRoot
 
get(Content.Filter<T>) - Method in class wyfs.util.AbstractRoot
 
get(int) - Method in class wyfs.util.Trie
 
get(CodeBlock.Index) - Method in class wyil.attributes.SourceLocationMap
 
get(int) - Method in class wyil.attributes.VariableDeclarations
 
get(CodeBlock.Index) - Method in interface wyil.lang.Attribute.Map
Get the meta-data associated with a given bytecode location.
get(int) - Method in class wyil.lang.CodeBlock
 
get(CodeBlock.Index) - Method in class wyil.lang.CodeBlock
Get the entry associated with a given bytecode id.
get(CodeBlock.Index) - Method in class wyil.util.AbstractAttributeMap
Get the attribute associated with a given bytecode location.
get(CodeBlock.Index) - Method in class wyil.util.AttributedCodeBlock
 
get(WyList, BigInteger) - Static method in class wyjc.runtime.WyList
 
get(String) - Method in class wyjc.runtime.WyRecord
 
get(WyRecord, String) - Static method in class wyjc.runtime.WyRecord
 
get(WyTuple, int) - Static method in class wyjc.runtime.WyTuple
 
getAll() - Method in interface wyfs.lang.Path.Folder
Get all objects contained in this folder (including those contained in subfolders).
getAll(Content.Filter<T>, List<Path.Entry<T>>) - Method in interface wyfs.lang.Path.Folder
Get all objects matching a given content filter stored in this folder (including its subfolders).
getAll(Content.Filter<T>, Set<Path.ID>) - Method in interface wyfs.lang.Path.Folder
Identify all entries matching a given content filter stored in this folder (including its subfolders).
getAll() - Method in class wyfs.util.AbstractFolder
 
getAll(Content.Filter<T>, List<Path.Entry<T>>) - Method in class wyfs.util.AbstractFolder
 
getAll(Content.Filter<T>, Set<Path.ID>) - Method in class wyfs.util.AbstractFolder
 
getAssertion() - Method in exception wycs.transforms.SmtVerificationCheck.AssertionFailure
Gets the assertion that caused this failure.
getAttributes() - Static method in class wyil.io.WyilFilePrinter
 
getCount() - Method in class wycs.solver.smt.Stmt.Pop
 
getCount() - Method in class wycs.solver.smt.Stmt.Push
 
getDebug() - Static method in class wycs.transforms.SmtVerificationCheck
Gets the default value of the debug option.
getDebug() - Static method in class wycs.transforms.VerificationCheck
 
getEmptyNameAsQualified() - Method in class wycs.solver.smt.Sort.Set
 
getEnable() - Static method in class wycs.transforms.MacroExpansion
 
getEnable() - Static method in class wycs.transforms.SmtVerificationCheck
Gets the default value of the enable option.
getEnable() - Static method in class wycs.transforms.TypePropagation
 
getEnable() - Static method in class wycs.transforms.VerificationCheck
 
getEnable() - Static method in class wyil.checks.DefiniteAssignmentCheck
 
getEnable() - Static method in class wyil.transforms.ConstantPropagation
 
getEnable() - Static method in class wyil.transforms.DeadCodeElimination
 
getEnable() - Static method in class wyil.transforms.LiveVariablesAnalysis
 
getEnable() - Static method in class wyil.transforms.LoopVariants
 
getExpr() - Method in class wycs.solver.smt.Stmt.Assert
Gets the expression.
getExpr() - Method in class wycs.solver.smt.Stmt.DefineFun
 
getExpr() - Method in class wycs.solver.smt.Stmt.DefineSort
 
getFolder(String) - Method in class wyfs.util.AbstractFolder
 
getLabel(String) - Method in class wyil.util.Interpreter.Context
 
getLabels() - Static method in class wyil.io.WyilFilePrinter
 
getLogic() - Method in class wycs.solver.smt.Stmt.SetLogic
 
getMatchingFiles(List<File>, DirectoryRoot, Content.Type<T>) - Static method in class wycs.util.WycsBuildTask
Generate the list of matching path entries corresponding to thegiven files on the filesystem.
getMaximallyConsumedType(Type) - Method in class wyil.util.TypeExpander
Return the maximally consumed type of a given type.
getMaxInferences() - Static method in class wycs.transforms.VerificationCheck
 
getMessage() - Method in exception wycc.lang.SyntaxError
 
getMessage() - Method in exception wycc.lang.SyntaxError.InternalFailure
 
getModifiedSourceFiles() - Method in class wyc.util.WycBuildTask
 
getModifiedSourceFiles(Path.Root, Content.Filter<T>, Path.Root, Content.Type<S>) - Static method in class wyc.util.WycBuildTask
Generate the list of source files which need to be recompiled.
getModifiedSourceFiles(Path.Root, Content.Filter<T>, Path.Root, Content.Type<S>) - Static method in class wycs.util.WycsBuildTask
Generate the list of source files whose modification time is after that of their binary counterpart.
getModifiedSourceFiles() - Method in class wyjc.util.WyjcBuildTask
 
getModule(Path.ID) - Method in class wyc.builder.WhileyBuilder
Get the (compiled) module associated with a given module identifier.
getModule(Path.ID) - Method in class wycs.builders.Wyal2WycsBuilder
Get the Wycs module associated with a given module identifier.
getModuleStub(WyalFile) - Method in class wycs.builders.Wyal2WycsBuilder
This converts a WyalFile into a WycsFile stub.
getName() - Method in class wycs.solver.smt.Sort.Any
 
getName() - Method in class wycs.solver.smt.Sort.Array
 
getName() - Method in class wycs.solver.smt.Sort.Bool
 
getName() - Method in class wycs.solver.smt.Sort.Int
 
getName() - Method in class wycs.solver.smt.Sort.Real
 
getName() - Method in class wycs.solver.smt.Sort.Set
Gets the name of this set sort.
getName() - Method in class wycs.solver.smt.Sort.Tuple
Gets the name of this tuple sort.
getName() - Method in class wycs.solver.smt.Stmt.DeclareFun
 
getName() - Method in class wycs.solver.smt.Stmt.DeclareSort
 
getName() - Method in class wycs.solver.smt.Stmt.DefineFun
 
getName() - Method in class wycs.solver.smt.Stmt.DefineSort
 
getNops() - Static method in class wyil.transforms.LiveVariablesAnalysis
 
getOption() - Method in class wycs.solver.smt.Stmt.SetOption
 
getParameters() - Method in class wycs.solver.smt.Stmt.DefineFun
 
getParameters() - Method in class wycs.solver.smt.Stmt.DefineSort
 
getParameterSorts() - Method in class wycs.solver.smt.Stmt.DeclareFun
 
getPosition() - Method in exception wycc.io.AbstractLexer.Error
 
getPreconditions(Code.Unit, VcBranch, Type[], AttributedCodeBlock) - Method in class wyil.builders.VcGenerator
Generate verification conditions to enforce the necessary preconditions for a given bytecode.
getReturnSort() - Method in class wycs.solver.smt.Stmt.DeclareFun
 
getReturnSort() - Method in class wycs.solver.smt.Stmt.DefineFun
 
getRwmode() - Static method in class wycs.transforms.VerificationCheck
 
getSize() - Method in class wycs.solver.smt.Stmt.DeclareSort
 
getSlots() - Static method in class wyil.io.WyilFilePrinter
 
getSolver() - Static method in class wycs.transforms.SmtVerificationCheck
Gets the default value of the solver option.
getSourceFile(Path.ID) - Method in class wyc.builder.WhileyBuilder
Get the source file associated with a given module identifier.
getTypeHelper(Type, boolean, ArrayList<Automaton.State>, HashMap<NameID, Integer>) - Method in class wyil.util.TypeExpander
Expand the given type by loading it's contents into the list of states.
getUnderlyingType(Type) - Method in class wyil.util.TypeExpander
Expand a given type by inlining all visible nominal information.
getUsedVariables(Set<Code.Variable>) - Method in class wycs.core.Code
Determine the complete set of used variables, including both bound and unbound variables.
getUsedVariables(Set<Code.Variable>) - Method in class wycs.core.Code.Quantifier
 
getUsedVariables(Set<Code.Variable>) - Method in class wycs.core.Code.Variable
 
getValue() - Method in class wycs.solver.smt.Stmt.SetOption
 
getVerification() - Method in class wyc.util.WycBuildTask
 
getVerificationConditions() - Method in class wyc.util.WycBuildTask
 
goTo(CodeBlock.Index) - Method in class wyil.builders.VcBranch
Update the program counter for this branch.
Goto(String) - Static method in class wyil.lang.Codes
Construct a goto bytecode which branches unconditionally to a given label.

H

hashCode() - Method in class wyautl_old.lang.Automaton
Determine the hashCode of a type.
hashCode() - Method in class wyautl_old.lang.Automaton.State
 
hashCode() - Method in class wyautl_old.lang.DefaultInterpretation.Term
 
hashCode() - Method in class wyc.lang.Nominal.Base
 
hashCode() - Method in class wyc.lang.Nominal.Function
 
hashCode() - Method in class wyc.lang.Nominal.List
 
hashCode() - Method in class wyc.lang.Nominal.Method
 
hashCode() - Method in class wyc.lang.Nominal.Record
 
hashCode() - Method in class wyc.lang.Nominal.Reference
 
hashCode() - Method in class wyc.lang.Nominal.Tuple
 
hashCode() - Method in class wycc.lang.NameID
 
hashCode() - Method in class wycc.util.Pair
 
hashCode() - Method in class wycc.util.Triple
 
hashCode() - Method in class wycs.core.SemanticType
 
hashCode() - Method in class wycs.core.Value.Array
 
hashCode() - Method in class wycs.core.Value.Bool
 
hashCode() - Method in class wycs.core.Value.Decimal
 
hashCode() - Method in class wycs.core.Value.Integer
 
hashCode() - Method in class wycs.core.Value.Null
 
hashCode() - Method in class wycs.core.Value.String
 
hashCode() - Method in class wycs.core.Value.Tuple
 
hashCode() - Method in class wycs.solver.smt.Stmt.Assert
hashCode() - Method in class wycs.solver.smt.Stmt.DeclareFun
hashCode() - Method in class wycs.solver.smt.Stmt.DeclareSort
hashCode() - Method in class wycs.solver.smt.Stmt.DefineFun
hashCode() - Method in class wycs.solver.smt.Stmt.DefineSort
hashCode() - Method in class wycs.solver.smt.Stmt.Exit
 
hashCode() - Method in class wyfs.util.Trie
 
hashCode() - Method in class wyil.lang.Code.AbstractBinaryOp
 
hashCode() - Method in class wyil.lang.Code.AbstractNaryAssignable
 
hashCode() - Method in class wyil.lang.Code.AbstractUnaryOp
 
hashCode() - Method in class wyil.lang.CodeBlock.Index
 
hashCode() - Method in class wyil.lang.Codes.Assert
 
hashCode() - Method in class wyil.lang.Codes.Assume
 
hashCode() - Method in class wyil.lang.Codes.BinaryOperator
 
hashCode() - Method in class wyil.lang.Codes.Const
 
hashCode() - Method in class wyil.lang.Codes.Convert
 
hashCode() - Method in class wyil.lang.Codes.FieldLoad
 
hashCode() - Method in class wyil.lang.Codes.Goto
 
hashCode() - Method in class wyil.lang.Codes.If
 
hashCode() - Method in class wyil.lang.Codes.IfIs
 
hashCode() - Method in class wyil.lang.Codes.Invariant
 
hashCode() - Method in class wyil.lang.Codes.Invoke
 
hashCode() - Method in class wyil.lang.Codes.Label
 
hashCode() - Method in class wyil.lang.Codes.Lambda
 
hashCode() - Method in class wyil.lang.Codes.Loop
 
hashCode() - Method in class wyil.lang.Codes.Not
 
hashCode() - Method in class wyil.lang.Codes.Quantify
 
hashCode() - Method in class wyil.lang.Codes.Switch
 
hashCode() - Method in class wyil.lang.Codes.UnaryOperator
 
hashCode() - Method in class wyil.lang.Constant.Bool
 
hashCode() - Method in class wyil.lang.Constant.Byte
 
hashCode() - Method in class wyil.lang.Constant.Decimal
 
hashCode() - Method in class wyil.lang.Constant.Integer
 
hashCode() - Method in class wyil.lang.Constant.Lambda
 
hashCode() - Method in class wyil.lang.Constant.List
 
hashCode() - Method in class wyil.lang.Constant.Null
 
hashCode() - Method in class wyil.lang.Constant.Rational
 
hashCode() - Method in class wyil.lang.Constant.Record
 
hashCode() - Method in class wyil.lang.Constant.Tuple
 
hashCode() - Method in class wyil.lang.Constant.Type
 
hashCode() - Method in class wyil.lang.Type.Any
 
hashCode() - Method in class wyil.lang.Type.Bool
 
hashCode() - Method in class wyil.lang.Type.Byte
 
hashCode() - Method in class wyil.lang.Type.Compound
 
hashCode() - Method in class wyil.lang.Type.Int
 
hashCode() - Method in class wyil.lang.Type.Meta
 
hashCode() - Method in class wyil.lang.Type.Nominal
 
hashCode() - Method in class wyil.lang.Type.Null
 
hashCode() - Method in class wyil.lang.Type.Real
 
hashCode() - Method in class wyil.lang.Type.Void
 
hashCode() - Method in class wyjc.runtime.WyBool
 
hashCode() - Method in class wyjc.runtime.WyByte
 
hashCode() - Method in class wyjc.runtime.WyRat
 
hasModifier(NameID, WhileyFile.Context, Modifier) - Method in class wyc.builder.FlowTypeChecker
Determine whether a named item has a modifier matching one of a given list.
hasModifier(Modifier) - Method in class wyc.lang.WhileyFile.NamedDeclaration
 
hasModifier(Modifier) - Method in class wyil.lang.WyilFile.Declaration
 
hasName(String) - Method in class wyc.lang.WhileyFile
 
hasName(String) - Method in class wyil.lang.WyilFile
Determines whether a declaration exists with the given name.
havoc(int) - Method in class wyil.builders.VcBranch
Terminate the current flow for a given register and begin a new one.
havocVariables(int[], VcBranch) - Method in class wyil.builders.VcGenerator
Send a given set of variables to havoc.

I

id() - Method in class wycs.core.WycsFile
 
id() - Method in class wycs.syntax.WyalFile
 
id() - Method in interface wyfs.lang.Path.Item
Return the identify of this item.
id - Variable in class wyfs.util.AbstractEntry
 
id() - Method in class wyfs.util.AbstractEntry
 
id - Variable in class wyfs.util.AbstractFolder
 
id() - Method in class wyfs.util.AbstractFolder
 
id() - Method in class wyil.lang.WyilFile
Returns the fully qualified name of this WyilFile, including both the package and module name.
Identifier(String, int) - Constructor for class wycc.io.Token.Identifier
 
IdentifierRule() - Constructor for class wycc.io.AbstractLexer.IdentifierRule
 
If(Type, int, int, Codes.Comparator, String) - Static method in class wyil.lang.Codes
 
IfElse(Expr, List<Stmt>, List<Stmt>, Attribute...) - Constructor for class wyc.lang.Stmt.IfElse
Construct an if-else statement from a condition, true branch and optional false branch.
IfElse(Expr, List<Stmt>, List<Stmt>, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.IfElse
Construct an if-else statement from a condition, true branch and optional false branch.
IfIs(Type, int, Type, String) - Static method in class wyil.lang.Codes
 
il2str(WyList) - Static method in class wyjc.runtime.Util
 
Impl() - Constructor for class wycc.lang.SyntacticElement.Impl
 
Impl(Attribute) - Constructor for class wycc.lang.SyntacticElement.Impl
 
Impl(Collection<Attribute>) - Constructor for class wycc.lang.SyntacticElement.Impl
 
Impl(Attribute[]) - Constructor for class wycc.lang.SyntacticElement.Impl
 
ImplicitCoercionOperator - Class in wyil.util.type
The implicit coercion operator extends the basic subtype operator to consider implicit coercions in the subtype computation.
ImplicitCoercionOperator(Automaton, Automaton) - Constructor for class wyil.util.type.ImplicitCoercionOperator
 
implies(Code, Code) - Static method in class wycs.builders.CodeGeneration
 
Implies(Automaton, int, int) - Static method in class wycs.solver.SolverUtil
Construct an automaton node representing the logical implication between two nodes
Import(Trie, String, Attribute...) - Constructor for class wyc.lang.WhileyFile.Import
 
Import(Trie, String, Attribute...) - Constructor for class wycs.syntax.WyalFile.Import
 
importCache - Variable in class wycs.builders.Wyal2WycsBuilder
The import cache caches specific import queries to their result sets.
imports(Trie) - Method in class wyc.builder.WhileyBuilder
This method takes a given import declaration, and expands it to find all matching modules.
imports() - Method in interface wyc.lang.WhileyFile.Context
 
imports(Trie) - Method in class wycs.builders.Wyal2WycsBuilder
This method takes a given import declaration, and expands it to find all matching modules.
imports() - Method in class wycs.syntax.WyalFile.AbstractContext
Construct an appropriate list of import statements for a declaration in a given file.
imports() - Method in interface wycs.syntax.WyalFile.Context
 
INCOMPARABLE_OPERANDS - Static variable in class wyil.util.ErrorMessages
 
indent(int) - Method in class wyc.io.WhileyFilePrinter
 
INDENT - Static variable in class wycs.io.WyalFilePrinter
 
index - Variable in class wyc.lang.Expr.IndexOf
 
index - Variable in class wycs.core.Code.Load
 
index - Variable in class wycs.core.Code.Variable
 
index - Variable in class wycs.syntax.Expr.IndexOf
 
Index(CodeBlock.Index) - Constructor for class wyil.lang.CodeBlock.Index
Construct an index which is nested within the parent index, and whose initial value at the innermost level is 0.
Index(CodeBlock.Index, int) - Constructor for class wyil.lang.CodeBlock.Index
Construct an index which is nested within the parent index, and whose initial value at the innermost level is determined by a given parameter.
index - Variable in class wyil.lang.Codes.TupleLoad
 
IndexOf(Expr, Expr, Attribute...) - Constructor for class wyc.lang.Expr.IndexOf
 
IndexOf(Expr, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Expr.IndexOf
 
IndexOf(SemanticType.Array, Code<?>, Code<?>, Attribute...) - Static method in class wycs.core.Code
 
IndexOf(SemanticType.Array, Code<?>, Code<?>, Collection<Attribute>) - Static method in class wycs.core.Code
 
IndexOf(Automaton, int...) - Static method in class wycs.solver.Solver
 
IndexOf(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
IndexOf(Expr, Expr, Attribute...) - Constructor for class wycs.syntax.Expr.IndexOf
 
IndexOf(Expr, Expr, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.IndexOf
 
IndexOf(Type.EffectiveArray, int, int, int) - Static method in class wyil.lang.Codes
Construct a listload bytecode which reads a value from a given index in a given list.
indexOperand - Variable in class wyil.lang.Codes.ListLVal
 
indexOperand - Variable in class wyil.lang.Codes.Quantify
 
indexOutOfBoundsChecks(Codes.IndexOf, VcBranch) - Method in class wyil.builders.VcGenerator
Generate preconditions necessary to protect against an out-of-bounds access.
indices() - Method in class wyil.util.AttributedCodeBlock
Return the list of all valid bytecode indexes in this block in order of appearance.
IndirectFunctionCall(Expr, Collection<Expr>, Attribute...) - Constructor for class wyc.lang.Expr.IndirectFunctionCall
 
IndirectFunctionCall(Expr, Collection<Expr>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.IndirectFunctionCall
 
IndirectInvoke(Expr, List<SyntacticType>, Expr, Attribute...) - Constructor for class wycs.syntax.Expr.IndirectInvoke
 
IndirectInvoke(Expr, List<SyntacticType>, Expr, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.IndirectInvoke
 
IndirectInvoke(Type.FunctionOrMethod, int, int, Collection<Integer>) - Static method in class wyil.lang.Codes
 
IndirectInvoke(Type.FunctionOrMethod, int, int, int[]) - Static method in class wyil.lang.Codes
 
IndirectMethodCall(Expr, Collection<Expr>, Attribute...) - Constructor for class wyc.lang.Expr.IndirectMethodCall
 
IndirectMethodCall(Expr, Collection<Expr>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.IndirectMethodCall
 
Inequality(Automaton, int...) - Static method in class wycs.solver.Solver
 
Inequality(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
infer(CodeBlock.Index, Codes.AssertOrAssume, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.BinaryOperator, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.Convert, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.Const, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.Debug, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.Fail, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.FieldLoad, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.TupleLoad, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.IndirectInvoke, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.Invoke, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.Lambda, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.LengthOf, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.IndexOf, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.Assign, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.Update, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.NewRecord, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.NewList, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.NewTuple, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.Return, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.Invert, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.UnaryOperator, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.NewObject, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(CodeBlock.Index, Codes.Dereference, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
infer(WyilFile.Type) - Method in class wyil.transforms.LoopVariants
 
infer(WyilFile.FunctionOrMethod) - Method in class wyil.transforms.LoopVariants
 
infer(CodeBlock) - Method in class wyil.transforms.LoopVariants
Determine the modified variables for a given block of Wyil bytecodes.
inferences - Static variable in class wycs.core.Types
 
inferences - Static variable in class wycs.solver.Solver
 
Inhabited(Automaton, int) - Static method in class wycs.solver.Solver
 
initialisePipeline() - Method in class wyc.util.WycBuildTask
Initialise the Wyil pipeline to be used for compiling Whiley files.
initialisePipeline() - Method in class wycs.util.WycsBuildTask
Initialise the Wyil pipeline to be used for compiling Whiley files.
initialiseProject() - Method in class wyc.util.WycBuildTask
 
initialiseProject() - Method in class wycs.util.WycsBuildTask
 
initialStore() - Method in class wyil.checks.DefiniteAssignmentCheck
 
initialStore() - Method in class wyil.transforms.ConstantPropagation
 
initialStore() - Method in class wyil.util.dfa.ForwardFlowAnalysis
Determine the initial store for the current method case.
innerLinkedList(int) - Static method in class wyil.lang.Type
 
inplaceAppend(Automaton, Automaton.State) - Static method in class wyautl_old.lang.Automata
Append all given states in place onto the given automaton.
inplaceAppendAll(Automaton, Automaton.State...) - Static method in class wyautl_old.lang.Automata
Append all given states in place onto the given automaton.
inplaceRemap(Automaton, int[]) - Static method in class wyautl_old.lang.Automata
The remap method takes an automaton, and a mapping from vertices in the old space to the those in the new space.
inplaceReorder(Automaton, int[]) - Static method in class wyautl_old.lang.Automata
The reorder method takes an automaton, and a mapping from vertices in the old space to the those in the new space.
input - Variable in class wyfs.io.BinaryInputStream
 
inputStream() - Method in interface wyfs.lang.Path.Entry
Open a generic input stream to the entry.
inputStream() - Method in class wyfs.util.DirectoryRoot.Entry
 
inputStream() - Method in class wyfs.util.VirtualRoot.Entry
 
insert(Path.Item) - Method in class wyfs.util.AbstractFolder
Insert a newly created item into this folder.
insert(CodeBlock.Index, T) - Method in interface wyil.lang.Attribute.Map
Insert meta-data associated with a given bytecode a given location.
insert(CodeBlock.Index, T) - Method in class wyil.util.AbstractAttributeMap
Insert meta-data associated with a given bytecode a given location.
instanceOf(Object, WyType) - Static method in class wyjc.runtime.Util
The instanceOf method implements a runtime type test.
instanceOf(WyList, WyType) - Static method in class wyjc.runtime.Util
This method gets called when we're testing a list object against some type.
instanceOf(WyRecord, WyType) - Static method in class wyjc.runtime.Util
This method gets called when we're testing a record object against some type.
instanceOf(WyTuple, WyType) - Static method in class wyjc.runtime.Util
This method gets called when we're testing a tuple object against some type.
instantiate(Builder) - Method in class wycc.lang.Pipeline
The following instantiates a compiler pipeline starting from the default pipeline and applying those modifiers requested.
instantiate(Builder) - Method in class wycc.lang.Pipeline.Template
Construct an instance of a given compiler stage, using the given argument list.
instantiate(Map<String, SemanticType>) - Method in class wycs.core.Code
Instantiate generic variables with concrete types in bytecodes as determined by a given map.
instantiate(Map<String, SemanticType>) - Method in class wycs.core.Code.Quantifier
 
instantiate(Automaton, Automaton.List) - Static method in class wycs.solver.Solver$native
Attempt to bind a quantified expression with a concrete expression, producing one or more candidate bindings over one or more quantified variables.
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.Binary
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.Cast
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.Constant
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.ConstantAccess
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.FieldAccess
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.IndexOf
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.IndirectInvoke
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.Invoke
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.Is
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.Nary
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.Quantifier
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.Record
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.Unary
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.Expr.Variable
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.SyntacticType.Function
 
instantiate(Map<String, SyntacticType>) - Method in interface wycs.syntax.SyntacticType
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.SyntacticType.Intersection
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.SyntacticType.List
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.SyntacticType.Negation
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.SyntacticType.Nominal
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.SyntacticType.Primitive
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.SyntacticType.Record
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.SyntacticType.Reference
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.SyntacticType.Tuple
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.SyntacticType.Union
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.SyntacticType.Variable
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.TypePattern
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.TypePattern.Intersection
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.TypePattern.Leaf
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.TypePattern.Rational
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.TypePattern.Record
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.TypePattern.Tuple
 
instantiate(Map<String, SyntacticType>) - Method in class wycs.syntax.TypePattern.Union
 
instantiateAxioms(Code, int) - Method in class wycs.transforms.VerificationCheck
Blindly instantiate all axioms.
Int(Attribute...) - Constructor for class wyc.lang.SyntacticType.Int
 
INT - Static variable in class wycc.util.OptArg
 
Int - Static variable in class wycs.core.SemanticType
 
INT - Static variable in class wycs.solver.smt.Sort
The singleton integer sort.
Int(Attribute...) - Constructor for class wycs.syntax.SyntacticType.Int
 
Int(Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Int
 
INT - Static variable in class wyjc.runtime.WyType
 
intDivide(WyRat) - Method in class wyjc.runtime.WyRat
 
Integer(BigInteger) - Static method in class wycs.core.Value
 
internal_add(WyList, Object) - Static method in class wyjc.runtime.WyList
This method is not intended for public consumption.
internal_add(WyTuple, Object) - Static method in class wyjc.runtime.WyTuple
This method is not intended for public consumption.
INTERNAL_FAILURE - Static variable in class wyc.WycMain
 
INTERNAL_FAILURE - Static variable in class wycs.WycsMain
 
internal_get(WyList, BigInteger) - Static method in class wyjc.runtime.WyList
This method is not intended for public consumption.
internal_get(WyRecord, String) - Static method in class wyjc.runtime.WyRecord
 
internalFailure(String, WhileyFile.Context, SyntacticElement) - Static method in class wyc.lang.WhileyFile
 
internalFailure(String, WhileyFile.Context, SyntacticElement, Throwable) - Static method in class wyc.lang.WhileyFile
 
internalFailure(String, String, SyntacticElement) - Static method in exception wycc.lang.SyntaxError
 
internalFailure(String, String, SyntacticElement, Throwable) - Static method in exception wycc.lang.SyntaxError
 
InternalFailure(String, String, int, int) - Constructor for exception wycc.lang.SyntaxError.InternalFailure
 
InternalFailure(String, String, int, int, Throwable) - Constructor for exception wycc.lang.SyntaxError.InternalFailure
 
internalFailure(String, String, Attribute...) - Static method in class wyil.util.ErrorMessages
Helper function for emitting a internal failure with appropriate source information.
internalFailure(String, String, Collection<Attribute>) - Static method in class wyil.util.ErrorMessages
Helper function for emitting a internal failure with appropriate source information.
internalFailure(String, String, Throwable, Attribute...) - Static method in class wyil.util.ErrorMessages
Helper function for emitting a internal failure with appropriate source information.
internalFailure(String, String, Throwable, Collection<Attribute>) - Static method in class wyil.util.ErrorMessages
Helper function for emitting a internal failure with appropriate source information.
Interpretation<T> - Interface in wyautl_old.lang
An interpretation is used to define the meaning of states in an Automata.
Interpreter - Class in wyil.util
A simple interpreter for WyIL bytecodes.
Interpreter(Build.Project, PrintStream) - Constructor for class wyil.util.Interpreter
 
Interpreter.Context - Class in wyil.util
A class for grouping two related items together.
intersect(Nominal, Nominal) - Static method in class wyc.lang.Nominal
 
intersect(Value.Array) - Method in class wycs.core.Value.Array
 
intersect(Type, Type) - Static method in class wyil.lang.Type
Compute the intersection of two types.
intersect(Type, Type) - Static method in class wyil.util.type.TypeAlgorithms
Compute the intersection of two types.
Intersection(Collection<SyntacticType>, Attribute...) - Constructor for class wyc.lang.SyntacticType.Intersection
 
Intersection(ArrayList<SyntacticType>, Collection<Attribute>) - Constructor for class wyc.lang.SyntacticType.Intersection
 
Intersection(List<TypePattern>, Attribute...) - Constructor for class wyc.lang.TypePattern.Intersection
 
Intersection(List<TypePattern>, List<Attribute>) - Constructor for class wyc.lang.TypePattern.Intersection
 
Intersection(Collection<SyntacticType>, Attribute...) - Constructor for class wycs.syntax.SyntacticType.Intersection
 
Intersection(Collection<SyntacticType>, Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Intersection
 
Intersection(List<TypePattern>, Attribute...) - Constructor for class wycs.syntax.TypePattern.Intersection
 
Intersection(List<TypePattern>, Collection<Attribute>) - Constructor for class wycs.syntax.TypePattern.Intersection
 
intersectRecords(int, boolean, int, boolean) - Method in class wyil.util.type.ExplicitCoercionOperator
Check for intersection between two states with kind K_RECORD.
intersectRecords(int, boolean, int, boolean) - Method in class wyil.util.type.SubtypeOperator
Check for intersection between two states with kind K_RECORD.
IntOrReal - Static variable in class wycs.core.SemanticType
 
intRemainder(WyRat) - Method in class wyjc.runtime.WyRat
 
IntT - Static variable in class wycs.core.Types
 
IntT - Static variable in class wycs.solver.Solver
 
intValue() - Method in class wyjc.runtime.WyRat
Get an integer representation of this rational.
INVALID_ARRAY_EXPRESSION - Static variable in class wyil.util.ErrorMessages
 
INVALID_BINARY_EXPRESSION - Static variable in class wyil.util.ErrorMessages
 
INVALID_BOOLEAN_EXPRESSION - Static variable in class wyil.util.ErrorMessages
 
INVALID_CONSTANT_EXPRESSION - Static variable in class wyil.util.ErrorMessages
 
INVALID_FILE_ACCESS - Static variable in class wyil.util.ErrorMessages
 
INVALID_LVAL_EXPRESSION - Static variable in class wyil.util.ErrorMessages
 
INVALID_NUMERIC_EXPRESSION - Static variable in class wyil.util.ErrorMessages
 
INVALID_PACKAGE_ACCESS - Static variable in class wyil.util.ErrorMessages
 
INVALID_TUPLE_LVAL - Static variable in class wyil.util.ErrorMessages
 
INVALID_UNARY_EXPRESSION - Static variable in class wyil.util.ErrorMessages
 
invalidate(int, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
Invalidate the record for a given register in the environment.
invariant - Variable in class wyc.lang.WhileyFile.Type
 
invariant - Variable in class wycs.core.WycsFile.Type
 
invariant - Variable in class wycs.syntax.WyalFile.Type
 
Invariant(Collection<Code>) - Static method in class wyil.lang.Codes
Construct an invariant bytecode which represents a user-defined loop invariant.
invariant() - Method in class wyil.lang.WyilFile.Type
 
invariants - Variable in class wyc.lang.Stmt.DoWhile
 
invariants - Variable in class wyc.lang.Stmt.While
 
Invert(Type, int, int) - Static method in class wyil.lang.Codes
 
invert(Codes.Comparator) - Static method in class wyil.lang.CodeUtils
Determine the inverse comparator, or null if no inverse exists.
Invoke(String, Path.ID, List<SyntacticType>, Expr, Attribute...) - Constructor for class wycs.syntax.Expr.Invoke
 
Invoke(String, Path.ID, List<SyntacticType>, Expr, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.Invoke
 
Invoke(Type.FunctionOrMethod, int, Collection<Integer>, NameID) - Static method in class wyil.lang.Codes
 
Invoke(Type.FunctionOrMethod, int, int[], NameID) - Static method in class wyil.lang.Codes
 
invokeInternal(Path.ID, String, Code, WyalFile.Context) - Method in class wycs.builders.CodeGeneration
 
Is(SemanticType, Code<?>, SemanticType, Attribute...) - Static method in class wycs.core.Code
 
Is(SemanticType, Code<?>, SemanticType, Collection<Attribute>) - Static method in class wycs.core.Code
 
Is(Automaton, int...) - Static method in class wycs.solver.Solver
 
Is(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
Is(Expr, SyntacticType, Attribute...) - Constructor for class wycs.syntax.Expr.Is
 
Is(Expr, SyntacticType, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.Is
 
isConcrete(Automaton) - Static method in class wyautl_old.lang.Automata
Check whether or not an automaton is "concrete".
isConcrete() - Method in class wyfs.util.Trie
 
isContractive(Type) - Static method in class wyil.lang.Type
Contractive types are types which cannot accept value because they have an unterminated cycle.
isContractive(Automaton) - Static method in class wyil.util.type.TypeAlgorithms
Contractive types are types which cannot accept value because they have an unterminated cycle.
isContractive(Automaton) - Static method in class wyil.util.type.TypeGenerator
 
isExplicitCoerciveSubtype(Type, Type) - Static method in class wyil.lang.Type
Determine whether type t2 is an explicit coercive subtype of type t1.
isFunction() - Method in class wyil.lang.WyilFile.FunctionOrMethod
 
isInteger() - Method in class wyjc.runtime.WyRat
 
isIntersection(int, boolean, int, boolean) - Method in class wyil.util.type.SubtypeOperator
Determine whether there is a non-empty intersection between the state rooted at fromIndex and that rooted at toIndex.
isIntersectionInner(int, boolean, int, boolean) - Method in class wyil.util.type.ExplicitCoercionOperator
 
isIntersectionInner(int, boolean, int, boolean) - Method in class wyil.util.type.ImplicitCoercionOperator
 
isIntersectionInner(int, boolean, int, boolean) - Method in class wyil.util.type.SubtypeOperator
 
isMemberOfType(Constant, Type, Interpreter.Context) - Method in class wyil.util.Interpreter
Determine whether a given value is a member of a given type.
isMethod() - Method in class wyil.lang.WyilFile.FunctionOrMethod
 
isModelEmpty(Automaton, ArrayList<DefaultInterpretation.Term>) - Static method in class wyil.util.type.TypeTester
 
isModelSubtype(Automaton, Automaton, ArrayList<DefaultInterpretation.Term>) - Static method in class wyil.util.type.TypeTester
 
isModified() - Method in interface wyfs.lang.Path.Entry
Check whether this file has been modified or not.
isModified() - Method in class wyfs.util.AbstractEntry
 
isName(NameID) - Method in class wyc.builder.WhileyBuilder
Determine whether a given name exists or not.
isNameVisible(NameID, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
Determine whether a name is visible in a given context.
isOpen - Variable in class wyc.lang.SyntacticType.Record
 
isOpen - Variable in class wyc.lang.TypePattern.Record
 
isOpen - Variable in class wycs.syntax.SyntacticType.Record
 
isOpen - Variable in class wycs.syntax.TypePattern.Record
 
isOpen(NameID, Type) - Static method in class wyil.lang.Type
This is a utility helper for constructing types.
isOpen(Set<NameID>, Type) - Static method in class wyil.lang.Type
This is a utility helper for constructing types.
isOpen() - Method in class wyil.lang.Type.Record
 
isOpen - Variable in class wyil.lang.Type.Record.State
 
isOpen - Variable in class wyjc.runtime.WyType.Record
 
isOperatorStart(char) - Method in class wyc.io.WhileyFileLexer
 
isOperatorStart(char) - Method in class wycs.io.WyalFileLexer
 
isPure(Expr, WhileyFile.Context) - Static method in class wyc.lang.Exprs
Determine whether this expression is "pure" or not.
isRealConstant(Constant) - Static method in class wyil.transforms.ConstantPropagation
 
isRelated(int, int) - Method in class wyautl_old.lang.DefaultSubsumption
 
isRelated(int, int) - Method in interface wyautl_old.lang.Relation
Check whether a node in the from automaton, and a node in the to automaton are related or not.
isSubsumed(Automaton, Automaton) - Static method in class wyautl_old.util.Tester
 
isSubtype(SemanticType, SemanticType) - Static method in class wycs.core.SemanticType
Check that t1 :> t2 or, equivalently, that t2 is a subtype of t1.
isSubtype(Type, Type) - Static method in class wyil.lang.Type
Determine whether type t2 is a subtype of type t1 (written t1 :> t2).
isSubtype(int, int) - Method in class wyil.util.type.SubtypeOperator
Test whether from :> to
isSupertype(int, int) - Method in class wyil.util.type.SubtypeOperator
Test whether from <: to
isTypeVisible(NameID, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
Determine whether a named type is fully visible in a given context.
isValidIdentifier(String) - Static method in class wycs.syntax.Expr
 
isValidIdentifierPart(char) - Static method in class wycs.syntax.Expr
 
isValidIdentifierStart(char) - Static method in class wycs.syntax.Expr
 
isWithin(CodeBlock.Index) - Method in class wyil.lang.CodeBlock.Index
Check whether this index is contained within a given parent index.
iterator() - Method in class wyfs.util.Trie
 
iterator() - Method in class wyil.lang.CodeBlock
 
iterator() - Method in class wyil.lang.Codes.Update
 
iterator(WyList) - Static method in class wyjc.runtime.WyList
 
iterator(WyTuple) - Static method in class wyjc.runtime.WyTuple
 

J

JarFileRoot - Class in wyfs.util
Provides an implementation of Path.Root for representing the contents of a jar file.
JarFileRoot(String, Content.Registry) - Constructor for class wyfs.util.JarFileRoot
 
JarFileRoot(File, Content.Registry) - Constructor for class wyfs.util.JarFileRoot
 
JarFileRoot.Folder - Class in wyfs.util
Represents a directory on a physical file system.
join(VcBranch...) - Method in class wyil.builders.VcBranch
Join two (or more) branches together to form a single active branch with two (or more) parents.
join(HashSet<Integer>, HashSet<Integer>) - Method in class wyil.checks.DefiniteAssignmentCheck
 
join(ConstantPropagation.Env, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
join(T, T) - Method in class wyil.util.dfa.ForwardFlowAnalysis
Join two abstract stores together producing a new abstract store.

K

K_And - Static variable in class wycs.solver.Solver
 
K_AndT - Static variable in class wycs.core.Types
 
K_AndT - Static variable in class wycs.solver.Solver
 
K_ANY - Static variable in class wyil.lang.Type
 
K_AnyT - Static variable in class wycs.core.Types
 
K_AnyT - Static variable in class wycs.solver.Solver
 
K_Array - Static variable in class wycs.solver.Solver
 
K_ArrayT - Static variable in class wycs.core.Types
 
K_ArrayT - Static variable in class wycs.solver.Solver
 
K_BOOL - Static variable in class wyil.lang.Type
 
K_BoolT - Static variable in class wycs.core.Types
 
K_BoolT - Static variable in class wycs.solver.Solver
 
K_BYTE - Static variable in class wyil.lang.Type
 
K_CHAR - Static variable in class wyil.lang.Type
 
K_Div - Static variable in class wycs.solver.Solver
 
K_Equals - Static variable in class wycs.solver.Solver
 
K_Equation - Static variable in class wycs.solver.Solver
 
K_Exists - Static variable in class wycs.solver.Solver
 
K_False - Static variable in class wycs.solver.Solver
 
K_Fn - Static variable in class wycs.solver.Solver
 
K_ForAll - Static variable in class wycs.solver.Solver
 
K_FUNCTION - Static variable in class wyil.lang.Type
 
K_FunctionT - Static variable in class wycs.core.Types
 
K_FunctionT - Static variable in class wycs.solver.Solver
 
K_IndexOf - Static variable in class wycs.solver.Solver
 
K_Inequality - Static variable in class wycs.solver.Solver
 
K_Inhabited - Static variable in class wycs.solver.Solver
 
K_INT - Static variable in class wyil.lang.Type
 
K_IntT - Static variable in class wycs.core.Types
 
K_IntT - Static variable in class wycs.solver.Solver
 
K_Is - Static variable in class wycs.solver.Solver
 
K_LengthOf - Static variable in class wycs.solver.Solver
 
K_LIST - Static variable in class wyil.lang.Type
 
K_Load - Static variable in class wycs.solver.Solver
 
K_MAP - Static variable in class wyil.lang.Type
 
K_META - Static variable in class wyil.lang.Type
 
K_METHOD - Static variable in class wyil.lang.Type
 
K_Mul - Static variable in class wycs.solver.Solver
 
K_NEGATION - Static variable in class wyil.lang.Type
 
K_NOMINAL - Static variable in class wyil.lang.Type
 
K_NominalT - Static variable in class wycs.core.Types
 
K_NominalT - Static variable in class wycs.solver.Solver
 
K_Not - Static variable in class wycs.solver.Solver
 
K_NotT - Static variable in class wycs.core.Types
 
K_NotT - Static variable in class wycs.solver.Solver
 
K_Null - Static variable in class wycs.solver.Solver
 
K_NULL - Static variable in class wyil.lang.Type
 
K_NullT - Static variable in class wycs.core.Types
 
K_NullT - Static variable in class wycs.solver.Solver
 
K_Num - Static variable in class wycs.solver.Solver
 
K_Or - Static variable in class wycs.solver.Solver
 
K_OrT - Static variable in class wycs.core.Types
 
K_OrT - Static variable in class wycs.solver.Solver
 
K_RATIONAL - Static variable in class wyil.lang.Type
 
K_RealT - Static variable in class wycs.core.Types
 
K_RealT - Static variable in class wycs.solver.Solver
 
K_RECORD - Static variable in class wyil.lang.Type
 
K_REFERENCE - Static variable in class wyil.lang.Type
 
K_SET - Static variable in class wyil.lang.Type
 
K_String - Static variable in class wycs.solver.Solver
 
K_STRING - Static variable in class wyil.lang.Type
 
K_StringT - Static variable in class wycs.core.Types
 
K_StringT - Static variable in class wycs.solver.Solver
 
K_Sum - Static variable in class wycs.solver.Solver
 
K_True - Static variable in class wycs.solver.Solver
 
K_Tuple - Static variable in class wycs.solver.Solver
 
K_TUPLE - Static variable in class wyil.lang.Type
 
K_TupleT - Static variable in class wycs.core.Types
 
K_TupleT - Static variable in class wycs.solver.Solver
 
K_UNION - Static variable in class wyil.lang.Type
 
K_Var - Static variable in class wycs.solver.Solver
 
K_VarT - Static variable in class wycs.core.Types
 
K_VarT - Static variable in class wycs.solver.Solver
 
K_VOID - Static variable in class wyil.lang.Type
 
K_VoidT - Static variable in class wycs.core.Types
 
K_VoidT - Static variable in class wycs.solver.Solver
 
key() - Method in class wyc.lang.Nominal.List
 
key(int) - Method in class wyil.lang.Codes.Update
Get the given key register (in order of appearance from the left) used in a map or list update.
key() - Method in class wyil.lang.Type.Array
 
key() - Method in class wyil.lang.Type.UnionOfArrays
 
key - Variable in class wyjc.runtime.WyType.Dictionary
 
keys() - Method in class wyil.lang.Codes.Update
Return the registers used to hold key values for map or list updates.
keys() - Method in class wyil.lang.Type.Record
Extract just the key set for this field.
Keyword(String, int) - Constructor for class wycc.io.Token.Keyword
 
KeywordRule(String[]) - Constructor for class wycc.io.AbstractLexer.KeywordRule
 
keywords - Static variable in class wyc.io.WhileyFileLexer
A map from identifier strings to the corresponding token kind.
keywords - Static variable in class wycs.io.WyalFileLexer
A map from identifier strings to the corresponding token kind.
kind - Variable in class wyautl_old.lang.Automaton.State
 
kind - Variable in class wyautl_old.lang.DefaultInterpretation.Term
 
Kind(boolean, int, int, Generator.Data) - Constructor for class wyautl_old.util.Generator.Kind
 
kind - Variable in class wyc.io.WhileyFileLexer.Token
 
kind - Variable in class wycs.io.WyalFileLexer.Token
 
kind - Variable in class wyil.lang.Codes.BinaryOperator
 
kind - Variable in class wyil.lang.Codes.UnaryOperator
 
kind - Variable in class wyjc.runtime.WyType
 
KINDS - Variable in class wyautl_old.util.Generator.Config
Provide details of kinds used.

L

Label(String) - Static method in class wyil.lang.Codes
 
label - Variable in class wyil.lang.Codes.Label
 
Label(int) - Constructor for class wyjc.runtime.WyType.Label
 
label - Variable in class wyjc.runtime.WyType.Label
 
label - Variable in class wyjc.Wyil2JavaBuilder
 
Lambda(Collection<WhileyFile.Parameter>, Expr, Attribute...) - Constructor for class wyc.lang.Expr.Lambda
 
Lambda(Collection<WhileyFile.Parameter>, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Expr.Lambda
 
Lambda(Type.FunctionOrMethod, int, Collection<Integer>, NameID) - Static method in class wyil.lang.Codes
 
Lambda(Type.FunctionOrMethod, int, int[], NameID) - Static method in class wyil.lang.Codes
 
lambdas - Variable in class wyjc.Wyil2JavaBuilder
List of temporary classes created to implement lambda expressions
last() - Method in interface wyfs.lang.Path.ID
A convenience function that gets the last component of this path.
last() - Method in class wyfs.util.Trie
 
lastModified() - Method in interface wyfs.lang.Path.Entry
Get the last modification time for this file.
lastModified() - Method in class wyfs.util.DirectoryRoot.Entry
 
lastModified() - Method in class wyfs.util.VirtualRoot.Entry
 
lastStore() - Method in class wyil.transforms.LiveVariablesAnalysis
Last store for the live variables analysis is empty, because all variables are considered to be dead at the end of a method/function.
lastStore() - Method in class wyil.util.dfa.BackwardFlowAnalysis
Generate the store which holds true immediately after the last statement of the method-case body.
Leaf(SyntacticType, Expr.LocalVariable, Attribute...) - Constructor for class wyc.lang.TypePattern.Leaf
 
Leaf(SyntacticType, Expr.LocalVariable, List<Attribute>) - Constructor for class wyc.lang.TypePattern.Leaf
 
Leaf(SyntacticType, Expr.Variable, Attribute...) - Constructor for class wycs.syntax.TypePattern.Leaf
 
Leaf(SyntacticType, Expr.Variable, Collection<Attribute>) - Constructor for class wycs.syntax.TypePattern.Leaf
 
Leaf() - Constructor for class wyil.lang.Type.Leaf
 
leafData(Type.Leaf) - Static method in class wyil.lang.Type
Determine the node data of a Type.Leaf.
leafKind(Type.Leaf) - Static method in class wyil.lang.Type
Determine the node kind of a Type.Leafs
leftOperand - Variable in class wycs.syntax.Expr.Binary
 
leftOperand - Variable in class wycs.syntax.Expr.Is
 
leftOperand - Variable in class wyil.lang.Code.AbstractBinaryOp
 
leftShift(BigInteger) - Method in class wyjc.runtime.WyByte
 
length() - Method in class wyjc.runtime.WyList
 
length(WyTuple) - Static method in class wyjc.runtime.WyTuple
 
LengthOf(Expr, Attribute...) - Constructor for class wyc.lang.Expr.LengthOf
 
LengthOf(Expr, Collection<Attribute>) - Constructor for class wyc.lang.Expr.LengthOf
 
LengthOf(Automaton, int) - Static method in class wycs.solver.Solver
 
LengthOf(Type.EffectiveArray, int, int) - Static method in class wyil.lang.Codes
 
LessThan(Automaton, int, int, int) - Static method in class wycs.solver.SolverUtil
Construct an automaton node representing an inequality comparing two arithmetic expressions.
LessThanEq(Automaton, int, int, int) - Static method in class wycs.solver.SolverUtil
Construct an automaton node representing the addition of two arithmetic expressions.
level() - Method in class wyil.lang.Codes.Update
 
lhs - Variable in class wyc.lang.Expr.BinOp
 
lhs - Variable in class wyc.lang.Stmt.Assign
 
line - Variable in class wycc.lang.Attribute.Origin
 
line - Variable in class wycc.lang.Attribute.Source
 
LineComment(String, int) - Constructor for class wycc.io.Token.LineComment
 
LineCommentRule(String) - Constructor for class wycc.io.AbstractLexer.LineCommentRule
 
lineNumbers - Variable in class wyjc.Wyil2JavaBuilder
List of line number entries for current function / method being compiled.
linkedList(int) - Static method in class wyil.lang.Type
 
List(Nominal, boolean) - Static method in class wyc.lang.Nominal
 
List(SyntacticType, Attribute...) - Constructor for class wycs.syntax.SyntacticType.List
 
List(SyntacticType, Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.List
 
List(WyType, boolean) - Constructor for class wyjc.runtime.WyType.List
 
ListGenerator(Type.Array, int, int, int) - Static method in class wyil.lang.Codes
Construct a listgen bytecode which constructs a new list initialised to a given length, with each element containing a given item.
listGeneratorChecks(Codes.ListGenerator, VcBranch) - Method in class wyil.builders.VcGenerator
Generate preconditions necessary to protect against a negative array size.
ListLVal(Type.EffectiveArray, int) - Constructor for class wyil.lang.Codes.ListLVal
 
LiveVariablesAnalysis - Class in wyil.transforms
Implements a classic live variables analysis to enable efficient reference counting.
LiveVariablesAnalysis(Builder) - Constructor for class wyil.transforms.LiveVariablesAnalysis
 
LiveVariablesAnalysis.Env - Class in wyil.transforms
 
Load(SemanticType.Tuple, Code<?>, int, Attribute...) - Static method in class wycs.core.Code
 
Load(SemanticType.Tuple, Code<?>, int, Collection<Attribute>) - Static method in class wycs.core.Code
 
Load(Automaton, int...) - Static method in class wycs.solver.Solver
 
Load(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
LocalVariable(String, Attribute...) - Constructor for class wyc.lang.Expr.LocalVariable
 
LocalVariable(String, Collection<Attribute>) - Constructor for class wyc.lang.Expr.LocalVariable
 
location() - Method in interface wyfs.lang.Path.Entry
Return a string indicating the true location of this entry.
location() - Method in class wyfs.util.DirectoryRoot.Entry
 
location() - Method in class wyfs.util.DirectoryRoot
 
location() - Method in class wyfs.util.VirtualRoot.Entry
 
Logger - Interface in wycc.util
Provides a standard interface for logging messages generated by builders.
logger - Variable in class wycs.builders.Wyal2WycsBuilder
 
logger - Variable in class wycs.builders.Wycs2WyalBuilder
 
logger - Variable in class wyil.builders.Wyil2WyalBuilder
For logging information.
Logger.Default - Class in wycc.util
A simple implementation of Logger which writes to a given PrintStream.
Logic - Enum in wycs.solver.smt
Roughly speaking, a logic is a collection of theorems that are required to run the Smt2File.
logout - Variable in class wyc.util.WycBuildTask
For logging information.
logout - Variable in class wycs.util.WycsBuildTask
For logging information.
logTimedMessage(String, long, long) - Method in class wycc.util.Logger.Default
This method is just a helper to format the output
logTimedMessage(String, long, long) - Method in interface wycc.util.Logger
Log a message, along with a time.
logTimedMessage(String, long, long) - Method in class wycs.builders.Wyal2WycsBuilder
 
logTotalTime(String, long, long) - Method in class wycc.util.Logger.Default
 
longValue() - Method in class wyjc.runtime.WyRat
Get a long representation of this rational.
lookahead() - Method in class wycc.io.AbstractLexer.BlockCommentRule
 
lookahead() - Method in class wycc.io.AbstractLexer.CharRule
 
lookahead() - Method in class wycc.io.AbstractLexer.DecimalRule
 
lookahead() - Method in class wycc.io.AbstractLexer.IdentifierRule
 
lookahead() - Method in class wycc.io.AbstractLexer.KeywordRule
 
lookahead() - Method in class wycc.io.AbstractLexer.LineCommentRule
 
lookahead() - Method in class wycc.io.AbstractLexer.OperatorRule
 
lookahead() - Method in class wycc.io.AbstractLexer.Rule
Determines the maximum amount of lookahead required by this rule.
lookahead() - Method in class wycc.io.AbstractLexer.StringRule
 
lookahead() - Method in class wycc.io.AbstractLexer.WhitespaceRule
 
lookupTransform(String) - Static method in class wycc.lang.Pipeline
Lookup a transform in the list of registered transforms.
Loop(int[], Collection<Code>) - Static method in class wyil.lang.Codes
 
Loop(int[], Code...) - Static method in class wyil.lang.Codes
 
LoopVariants - Class in wyil.transforms
Responsible for determining what the modified variables (a.k.a variants) in a loop are.
LoopVariants(Builder) - Constructor for class wyil.transforms.LoopVariants
 
LVal(T) - Constructor for class wyil.lang.Codes.LVal
 

M

Macro(String, SemanticType.Function, Code<?>, Attribute...) - Constructor for class wycs.core.WycsFile.Macro
 
Macro(String, List<String>, TypePattern, Expr, Attribute...) - Constructor for class wycs.syntax.WyalFile.Macro
 
MacroExpansion - Class in wycs.transforms
Responsible for inlining macros (i.e.
MacroExpansion(Builder) - Constructor for class wycs.transforms.MacroExpansion
 
main(String[]) - Static method in class wyautl_old.lang.Automata
 
main(String[]) - Static method in class wyautl_old.util.Filter
 
main(String[]) - Static method in class wyautl_old.util.Generator
 
main(String[]) - Static method in class wyautl_old.util.Tester
 
main(String[]) - Static method in class wyc.WycMain
 
main(String[]) - Static method in class wycs.core.Types
 
main(String[]) - Static method in class wycs.solver.Solver
 
main(String[]) - Static method in class wycs.WycsMain
 
main(String[]) - Static method in class wyfs.io.BinaryOutputStream
 
main(String[]) - Static method in class wyfs.util.Trie
 
main(String[]) - Static method in class wyil.lang.Type
 
Main - Class in wyil
 
Main() - Constructor for class wyil.Main
 
main(String[]) - Static method in class wyil.Main
 
main(String[]) - Static method in class wyil.util.type.TypeGenerator
 
main(String[]) - Static method in class wyil.util.type.TypeTester
 
main(String[]) - Static method in class wyjc.WyjcMain
 
Main.Registry - Class in wyil
Default implementation of a content registry.
MAJOR_VERSION - Static variable in class wyc.WycMain
 
MAJOR_VERSION - Static variable in class wycs.WycsMain
 
match(Content.Filter<T>) - Method in interface wybs.lang.Build.Project
Identify all entries matching a given content filter stored in this root.
match(Content.Filter<T>) - Method in class wybs.util.StdProject
Identify all entries matching a given content filter stored in this root.
match(StringBuffer, int) - Method in class wycc.io.AbstractLexer.BlockCommentRule
 
match(StringBuffer, int) - Method in class wycc.io.AbstractLexer.CharRule
 
match(StringBuffer, int) - Method in class wycc.io.AbstractLexer.DecimalRule
 
match(StringBuffer, int) - Method in class wycc.io.AbstractLexer.IdentifierRule
 
match(StringBuffer, int) - Method in class wycc.io.AbstractLexer.KeywordRule
 
match(StringBuffer, int) - Method in class wycc.io.AbstractLexer.LineCommentRule
 
match(StringBuffer, int) - Method in class wycc.io.AbstractLexer.OperatorRule
 
match(StringBuffer, int) - Method in class wycc.io.AbstractLexer.Rule
Attempt to match this rule at a given position in the input stream.
match(StringBuffer, int) - Method in class wycc.io.AbstractLexer.StringRule
 
match(StringBuffer, int) - Method in class wycc.io.AbstractLexer.WhitespaceRule
 
match(Content.Filter<T>) - Method in interface wyfs.lang.Path.Root
Identify all entries matching a given content filter stored in this root.
match(Content.Filter<T>) - Method in class wyfs.util.AbstractRoot
 
matches(Path.ID, Content.Type<T>) - Method in interface wyfs.lang.Content.Filter
Check whether a given entry is matched by this filter.
matches(Path.ID) - Method in interface wyfs.lang.Path.Filter
Check whether a given entry is matched by this filter.
matches(Path.ID) - Method in class wyfs.util.Trie
 
matchesSubpath(Path.ID) - Method in interface wyfs.lang.Content.Filter
Check whether a given subpath is matched by this filter.
matchesSubpath(Path.ID) - Method in interface wyfs.lang.Path.Filter
Check whether a given subpath is matched by this filter.
matchesSubpath(Path.ID) - Method in class wyfs.util.Trie
 
max(Automaton, int) - Static method in class wycs.solver.Solver$native
Determine the maximum element from a bag of elements according to an internal ordering defined here.
MAX_CHILDREN - Variable in class wyautl_old.util.Generator.Kind
Determine maximum number of children this kind can have.
maxMultiplicand(Automaton, int) - Static method in class wycs.solver.Solver$native
 
message - Variable in class wycs.core.WycsFile.Assert
 
message - Variable in class wycs.syntax.WyalFile.Assert
 
META - Static variable in class wyjc.runtime.WyType
 
Method(Type.Method, Type.Method) - Constructor for class wyc.lang.Nominal.Method
 
Method(SyntacticType, SyntacticType, Collection<SyntacticType>, Attribute...) - Constructor for class wyc.lang.SyntacticType.Method
 
Method(SyntacticType, SyntacticType, Collection<SyntacticType>, Collection<Attribute>) - Constructor for class wyc.lang.SyntacticType.Method
 
Method(List<Modifier>, String, TypePattern, List<WhileyFile.Parameter>, List<Expr>, List<Expr>, SyntacticType, List<Stmt>, Attribute...) - Constructor for class wyc.lang.WhileyFile.Method
 
Method(Type, Type, Collection<Type>) - Static method in class wyil.lang.Type
Construct a method type using the given receiver, return and parameter types.
Method(Type, Type, Type...) - Static method in class wyil.lang.Type
Construct a function type using the given return and parameter types.
method - Variable in class wyil.util.dfa.BackwardFlowAnalysis
The function or method currently being propagated through.
method - Variable in class wyil.util.dfa.ForwardFlowAnalysis
The function or method currently being propagated through.
MethodCall(NameID, Path.ID, Collection<Expr>, Attribute...) - Constructor for class wyc.lang.Expr.MethodCall
 
MethodCall(NameID, Path.ID, Collection<Expr>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.MethodCall
 
METHODCALL_NOT_PERMITTED_IN_FUNCTION - Static variable in class wyil.util.ErrorMessages
 
methodType - Variable in class wyc.lang.Expr.IndirectMethodCall
 
methodType - Variable in class wyc.lang.Expr.MethodCall
 
mhs - Variable in class wyc.lang.Expr.UnOp
 
min(Automaton, int) - Static method in class wycs.solver.Solver$native
Determine the minimum element from a bag of elements according to an internal ordering defined here.
MIN_CHILDREN - Variable in class wyautl_old.util.Generator.Kind
Determine minimum number of children this kind can have.
minimise(Automaton) - Static method in class wyautl_old.lang.Automata
This method minimises an automaton by removing equivalent states.
minimiseTest(Interpretation, ArrayList<DefaultInterpretation.Term>, ArrayList<Automaton>, boolean) - Static method in class wyautl_old.util.Tester
The purpose of this test is to check that minimised automata accept the same set of values as non-minimised ones.
MINOR_REVISION - Static variable in class wyc.WycMain
 
MINOR_REVISION - Static variable in class wycs.WycsMain
 
MINOR_VERSION - Static variable in class wyc.WycMain
 
MINOR_VERSION - Static variable in class wycs.WycsMain
 
MISSING_RETURN_VALUE - Static variable in class wyil.util.ErrorMessages
 
modified - Variable in class wyfs.util.AbstractEntry
 
modifiedOperands - Variable in class wyil.lang.Codes.Loop
 
Modifier(Pipeline.POP, String, Map<String, Object>) - Constructor for class wycc.lang.Pipeline.Modifier
 
Modifier - Interface in wyil.lang
Represents a protection modifier on a module item.
Modifier.Export - Class in wyil.lang
 
Modifier.Native - Class in wyil.lang
 
Modifier.Private - Class in wyil.lang
 
Modifier.Public - Class in wyil.lang
 
MODIFIER_Export - Static variable in class wyil.io.WyilFileWriter
 
MODIFIER_MANGLE_MASK - Static variable in class wyil.io.WyilFileWriter
 
MODIFIER_Native - Static variable in class wyil.io.WyilFileWriter
 
MODIFIER_Private - Static variable in class wyil.io.WyilFileWriter
 
MODIFIER_PROTECTION_MASK - Static variable in class wyil.io.WyilFileWriter
 
MODIFIER_Public - Static variable in class wyil.io.WyilFileWriter
 
modifiers() - Method in class wyc.lang.WhileyFile.NamedDeclaration
 
modifiers() - Method in class wyil.lang.WyilFile.Declaration
 
module - Variable in class wyc.lang.WhileyFile
 
module() - Method in class wycc.lang.NameID
 
ModuleCheck - Class in wyil.checks
Performs a number of simplistic checks that a module is syntactically correct.
ModuleCheck(Builder) - Constructor for class wyil.checks.ModuleCheck
 
ModuleReader - Interface in wyil.io
A module reader is responsible for physically reading information about a given module.
MONE - Static variable in class wyjc.runtime.WyRat
 
Move(Type, int, int) - Static method in class wyil.lang.Codes
 
msg() - Method in exception wycc.lang.SyntaxError
Error message
Mul(Automaton, int...) - Static method in class wycs.solver.Solver
 
Mul(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
Mul(Automaton, int, int) - Static method in class wycs.solver.SolverUtil
Construct an automaton node representing the multiplication of two arithmetic expressions.
multiply(Value.Decimal) - Method in class wycs.core.Value.Decimal
 
multiply(Value.Integer) - Method in class wycs.core.Value.Integer
 
multiply(Constant.Decimal) - Method in class wyil.lang.Constant.Decimal
 
multiply(Constant.Integer) - Method in class wyil.lang.Constant.Integer
 
multiply(Constant.Rational) - Method in class wyil.lang.Constant.Rational
 
multiply(int) - Method in class wyjc.runtime.WyRat
 
multiply(long) - Method in class wyjc.runtime.WyRat
 
multiply(BigInteger) - Method in class wyjc.runtime.WyRat
 
multiply(WyRat) - Method in class wyjc.runtime.WyRat
 
mustParseAsMixedType() - Method in class wyc.io.WhileyFileParser
 
mustParseAsMixedType() - Method in class wycs.io.WyalFileParser
 

N

name - Variable in class wyc.lang.Expr.AbstractFunctionOrMethod
 
name - Variable in class wyc.lang.Expr.AbstractInvoke
 
name - Variable in class wyc.lang.Expr.ConstantAccess
 
name - Variable in class wyc.lang.Expr.FieldAccess
 
name - Variable in class wyc.lang.WhileyFile.Import
 
name() - Method in class wyc.lang.WhileyFile.NamedDeclaration
 
name - Variable in class wyc.lang.WhileyFile.Parameter
 
name() - Method in class wyc.lang.WhileyFile.Parameter
 
name() - Method in class wycc.lang.NameID
 
name - Variable in class wycc.lang.Pipeline.Modifier
 
name(String) - Static method in class wycs.builders.Wyal2WycsBuilder
 
name() - Method in class wycs.core.SemanticType.Nominal
 
name() - Method in class wycs.core.SemanticType.Var
 
name() - Method in class wycs.core.WycsFile.Assert
 
name() - Method in interface wycs.core.WycsFile.Declaration
 
name - Variable in class wycs.core.WycsFile.Function
 
name() - Method in class wycs.core.WycsFile.Function
 
name - Variable in class wycs.core.WycsFile.Macro
 
name() - Method in class wycs.core.WycsFile.Macro
 
name - Variable in class wycs.core.WycsFile.Type
 
name() - Method in class wycs.core.WycsFile.Type
 
name - Variable in class wycs.syntax.Expr.ConstantAccess
 
name - Variable in class wycs.syntax.Expr.FieldAccess
 
name - Variable in class wycs.syntax.Expr.Invoke
 
name - Variable in class wycs.syntax.Expr.Variable
 
name() - Method in class wycs.syntax.WyalFile.Assert
 
name - Variable in class wycs.syntax.WyalFile.Assume
 
name() - Method in class wycs.syntax.WyalFile.Assume
 
name() - Method in interface wycs.syntax.WyalFile.Declaration
 
name - Variable in class wycs.syntax.WyalFile.Function
 
name() - Method in class wycs.syntax.WyalFile.Function
 
name - Variable in class wycs.syntax.WyalFile.Import
 
name() - Method in class wycs.syntax.WyalFile.Import
 
name - Variable in class wycs.syntax.WyalFile.Macro
 
name() - Method in class wycs.syntax.WyalFile.Macro
 
name - Variable in class wycs.syntax.WyalFile.Type
 
name() - Method in class wycs.syntax.WyalFile.Type
 
name() - Method in class wyil.attributes.VariableDeclarations.Declaration
 
name - Variable in class wyil.lang.Codes.Invoke
 
name - Variable in class wyil.lang.Codes.Lambda
 
name - Variable in class wyil.lang.Constant.Lambda
 
name() - Method in class wyil.lang.Type.Nominal
 
name() - Method in class wyil.lang.WyilFile.Declaration
 
NamedDeclaration(String, Collection<Modifier>, Attribute...) - Constructor for class wyc.lang.WhileyFile.NamedDeclaration
 
NameID - Class in wycc.lang
A Name Identifier consists of a module, and a name within that module.
NameID(Path.ID, String) - Constructor for class wycc.lang.NameID
 
names - Variable in class wyc.lang.SyntacticType.Nominal
 
names - Variable in class wycs.syntax.SyntacticType.Nominal
 
names - Variable in class wyjc.runtime.WyType.Record
 
Nary(SemanticType, Code.Op, Code<?>[], Attribute...) - Static method in class wycs.core.Code
 
Nary(SemanticType, Code.Op, Code<?>[], Collection<Attribute>) - Static method in class wycs.core.Code
 
Nary(Expr.Nary.Op, List<Expr>, Attribute...) - Constructor for class wycs.syntax.Expr.Nary
 
Nary(Expr.Nary.Op, List<Expr>, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.Nary
 
Nary(Expr.Nary.Op, Expr[], Attribute...) - Constructor for class wycs.syntax.Expr.Nary
 
Nary(Expr.Nary.Op, Expr[], Collection<Attribute>) - Constructor for class wycs.syntax.Expr.Nary
 
NATIVE - Static variable in interface wyil.lang.Modifier
 
Neg(Automaton, int) - Static method in class wycs.solver.SolverUtil
Construct an automaton node representing the negation of an arithmetic expression.
negate() - Method in class wyil.lang.Constant.Decimal
 
negate() - Method in class wyil.lang.Constant.Integer
 
negate() - Method in class wyil.lang.Constant.Rational
 
negate() - Method in class wyjc.runtime.WyRat
 
Negation(Nominal) - Static method in class wyc.lang.Nominal
 
Negation(SyntacticType, Attribute...) - Constructor for class wyc.lang.SyntacticType.Negation
 
Negation(SyntacticType, Attribute...) - Constructor for class wycs.syntax.SyntacticType.Negation
 
Negation(SyntacticType, Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Negation
 
Negation(Type) - Static method in class wyil.lang.Type
Construct a difference of two types.
Negation(WyType) - Constructor for class wyjc.runtime.WyType.Negation
 
negationNormalForm(Code) - Static method in class wycs.core.NormalForms
Convert a given expression into negation normal form, where all logical negations are pushed inwards as far as possible.
nestedWithin(int) - Method in class wyil.lang.CodeBlock.Index
Return the first index nested within this index.
New(Expr, Attribute...) - Constructor for class wyc.lang.Expr.New
 
NewLine(String, int) - Constructor for class wycc.io.Token.NewLine
 
NewList(Type.Array, int, Collection<Integer>) - Static method in class wyil.lang.Codes
Construct a newlist bytecode which constructs a new list and puts it on the stack.
NewList(Type.Array, int, int[]) - Static method in class wyil.lang.Codes
 
NewObject(Type.Reference, int, int) - Static method in class wyil.lang.Codes
 
NewRecord(Type.Record, int, Collection<Integer>) - Static method in class wyil.lang.Codes
Construct a newrecord bytecode which constructs a new record and puts it on the stack.
NewRecord(Type.Record, int, int[]) - Static method in class wyil.lang.Codes
 
NewTuple(Type.Tuple, int, Collection<Integer>) - Static method in class wyil.lang.Codes
Construct a newtuple bytecode which constructs a new tuple and puts it on the stack.
NewTuple(Type.Tuple, int, int[]) - Static method in class wyil.lang.Codes
 
next() - Method in class wyil.lang.CodeBlock.Index
Return the next index in sequence.
next(int) - Method in class wyil.lang.CodeBlock.Index
Return the next index in sequence.
nid - Variable in class wyc.lang.Expr.FunctionCall
 
nid() - Method in class wyc.lang.Expr.FunctionCall
 
nid - Variable in class wyc.lang.Expr.FunctionOrMethod
 
nid - Variable in class wyc.lang.Expr.MethodCall
 
nid() - Method in class wyc.lang.Expr.MethodCall
 
nid - Variable in class wycs.core.Code.FunCall
 
NOCHILDREN - Static variable in class wyautl_old.lang.Automaton
The following constant is used simply to prevent unnecessary memory allocations.
Nominal - Class in wyc.lang
A type pair is used to simplify the problem of dealing with nominal and raw types.
Nominal() - Constructor for class wyc.lang.Nominal
 
nominal() - Method in class wyc.lang.Nominal.Base
 
nominal() - Method in class wyc.lang.Nominal.Function
 
nominal() - Method in class wyc.lang.Nominal.FunctionOrMethod
 
nominal() - Method in class wyc.lang.Nominal.List
 
nominal() - Method in class wyc.lang.Nominal.Method
 
nominal() - Method in class wyc.lang.Nominal
 
nominal() - Method in class wyc.lang.Nominal.Record
 
nominal() - Method in class wyc.lang.Nominal.Reference
 
nominal() - Method in class wyc.lang.Nominal.Tuple
 
Nominal(Collection<String>, Attribute...) - Constructor for class wyc.lang.SyntacticType.Nominal
 
Nominal(NameID) - Static method in class wycs.core.SemanticType
 
Nominal(NameID) - Constructor for class wycs.core.SemanticType.Nominal
 
Nominal(Collection<String>, Attribute...) - Constructor for class wycs.syntax.SyntacticType.Nominal
 
Nominal(Collection<String>, Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Nominal
 
Nominal(NameID) - Static method in class wyil.lang.Type
 
Nominal.Base - Class in wyc.lang
 
Nominal.Function - Class in wyc.lang
 
Nominal.FunctionOrMethod - Class in wyc.lang
 
Nominal.List - Class in wyc.lang
 
Nominal.Method - Class in wyc.lang
 
Nominal.Record - Class in wyc.lang
 
Nominal.Reference - Class in wyc.lang
 
Nominal.Tuple - Class in wyc.lang
 
NominalT(Automaton, String) - Static method in class wycs.core.Types
 
NominalT(Automaton, String) - Static method in class wycs.solver.Solver
 
nonAccepting(Automaton) - Static method in class wyautl_old.util.Tester
 
nonEmpty() - Method in class wyil.lang.Type.Array
 
nonEmpty - Variable in class wyjc.runtime.WyType.List
 
nonEmpty - Variable in class wyjc.runtime.WyType.Set
 
Nop - Static variable in class wyil.lang.Codes
 
NormalForms - Class in wycs.core
Provides a number of encodings for many of the standard data types found in a typical programming language (especially, of course, those found in Whiley).
NormalForms() - Constructor for class wycs.core.NormalForms
 
Not(SemanticType) - Static method in class wycs.core.SemanticType
 
Not(SemanticType) - Constructor for class wycs.core.SemanticType.Not
 
Not(Automaton, int) - Static method in class wycs.solver.Solver
 
Not(int, int) - Static method in class wyil.lang.Codes
 
NotT(Automaton, int) - Static method in class wycs.core.Types
 
NotT(Automaton, int) - Static method in class wycs.solver.Solver
 
Null(Attribute...) - Constructor for class wyc.lang.SyntacticType.Null
 
NULL - Static variable in interface wycc.util.Logger
The NULL logger simply drops all logged messages.
Null - Static variable in class wycs.core.SemanticType
 
Null - Static variable in class wycs.core.Value
 
Null - Static variable in class wycs.solver.Solver
 
Null(Attribute...) - Constructor for class wycs.syntax.SyntacticType.Null
 
Null(Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Null
 
Null() - Constructor for class wyil.lang.Constant.Null
 
NULL - Static variable in class wyjc.runtime.WyType
 
NULL_FILTER - Static variable in class wyfs.util.DirectoryRoot
 
NULL_REG - Static variable in class wyil.lang.Codes
Provided to aid readability of client code.
NullT - Static variable in class wycs.core.Types
 
NullT - Static variable in class wycs.solver.Solver
 
Num(Automaton, long) - Static method in class wycs.solver.Solver
 
Num(Automaton, BigRational) - Static method in class wycs.solver.Solver
 
Number(int, BigInteger, BigInteger, String, int) - Constructor for class wycc.io.Token.Number
Construct a token representing a decimal number represented in a given base.
numberOfSteps - Variable in class wycs.transforms.VerificationCheck.RESULT
 
numerator - Variable in class wyc.lang.Expr.RationalLVal
 
numerator - Variable in class wyc.lang.TypePattern.Rational
 
numerator - Variable in class wycs.syntax.TypePattern.Rational
 
numerator() - Method in class wyjc.runtime.WyRat
 
numSlots() - Method in class wyil.builders.VcBranch
 
numSlots() - Method in class wyil.lang.CodeBlock
Determine the number of slots used in this block.

O

offset - Variable in enum wycs.core.Code.Op
 
offset - Variable in enum wycs.syntax.Expr.Binary.Op
 
offset - Variable in enum wycs.syntax.Expr.Nary.Op
 
offset - Variable in enum wycs.syntax.Expr.Unary.Op
 
offset - Variable in enum wyil.lang.Codes.BinaryOperatorKind
 
offset - Variable in enum wyil.lang.Codes.Comparator
 
offset - Variable in enum wyil.lang.Codes.UnaryOperatorKind
 
ONE - Static variable in class wyjc.runtime.WyRat
 
op - Variable in class wyc.lang.Expr.BinOp
 
op - Variable in class wyc.lang.Expr.UnOp
 
op - Variable in class wycc.lang.Pipeline.Modifier
 
op - Variable in class wycs.syntax.Expr.Binary
 
op - Variable in class wycs.syntax.Expr.Nary
 
op - Variable in class wycs.syntax.Expr.Unary
 
op - Variable in class wyil.lang.Codes.If
 
opcode - Variable in class wycs.core.Code
The opcode which defines what this bytecode does.
opcode() - Method in interface wyil.lang.Code
Return the opcode value of this bytecode.
opcode() - Method in class wyil.lang.Codes.Assert
 
opcode() - Method in class wyil.lang.Codes.Assign
 
opcode() - Method in class wyil.lang.Codes.Assume
 
opcode() - Method in class wyil.lang.Codes.BinaryOperator
 
opcode() - Method in class wyil.lang.Codes.Const
 
opcode() - Method in class wyil.lang.Codes.Convert
 
opcode() - Method in class wyil.lang.Codes.Debug
 
opcode() - Method in class wyil.lang.Codes.Dereference
 
opcode() - Method in class wyil.lang.Codes.Fail
 
opcode() - Method in class wyil.lang.Codes.FieldLoad
 
opcode() - Method in class wyil.lang.Codes.Goto
 
opcode() - Method in class wyil.lang.Codes.If
 
opcode() - Method in class wyil.lang.Codes.IfIs
 
opcode() - Method in class wyil.lang.Codes.IndexOf
 
opcode() - Method in class wyil.lang.Codes.IndirectInvoke
 
opcode() - Method in class wyil.lang.Codes.Invariant
 
opcode() - Method in class wyil.lang.Codes.Invert
 
opcode() - Method in class wyil.lang.Codes.Invoke
 
opcode() - Method in class wyil.lang.Codes.Label
 
opcode() - Method in class wyil.lang.Codes.Lambda
 
opcode() - Method in class wyil.lang.Codes.LengthOf
 
opcode() - Method in class wyil.lang.Codes.ListGenerator
 
opcode() - Method in class wyil.lang.Codes.Loop
 
opcode() - Method in class wyil.lang.Codes.Move
 
opcode() - Method in class wyil.lang.Codes.NewList
 
opcode() - Method in class wyil.lang.Codes.NewObject
 
opcode() - Method in class wyil.lang.Codes.NewRecord
 
opcode() - Method in class wyil.lang.Codes.NewTuple
 
opcode() - Method in class wyil.lang.Codes.Nop
 
opcode() - Method in class wyil.lang.Codes.Not
 
opcode() - Method in class wyil.lang.Codes.Quantify
 
opcode() - Method in class wyil.lang.Codes.Return
 
opcode() - Method in class wyil.lang.Codes.Switch
 
opcode() - Method in class wyil.lang.Codes.TupleLoad
 
opcode() - Method in class wyil.lang.Codes.UnaryOperator
 
opcode() - Method in class wyil.lang.Codes.Update
 
opcode() - Method in class wyil.lang.Codes.Void
 
OPCODE_add - Static variable in interface wyil.lang.Code
 
OPCODE_assertblock - Static variable in interface wyil.lang.Code
 
OPCODE_assign - Static variable in interface wyil.lang.Code
 
OPCODE_assumeblock - Static variable in interface wyil.lang.Code
 
OPCODE_bitwiseand - Static variable in interface wyil.lang.Code
 
OPCODE_bitwiseor - Static variable in interface wyil.lang.Code
 
OPCODE_bitwisexor - Static variable in interface wyil.lang.Code
 
OPCODE_const - Static variable in interface wyil.lang.Code
 
OPCODE_convert - Static variable in interface wyil.lang.Code
 
OPCODE_debug - Static variable in interface wyil.lang.Code
 
OPCODE_denominator - Static variable in interface wyil.lang.Code
 
OPCODE_dereference - Static variable in interface wyil.lang.Code
 
OPCODE_div - Static variable in interface wyil.lang.Code
 
OPCODE_fail - Static variable in interface wyil.lang.Code
 
OPCODE_fieldload - Static variable in interface wyil.lang.Code
 
OPCODE_goto - Static variable in interface wyil.lang.Code
 
OPCODE_ifel - Static variable in interface wyil.lang.Code
 
OPCODE_ifeq - Static variable in interface wyil.lang.Code
 
OPCODE_ifge - Static variable in interface wyil.lang.Code
 
OPCODE_ifgt - Static variable in interface wyil.lang.Code
 
OPCODE_ifis - Static variable in interface wyil.lang.Code
 
OPCODE_ifle - Static variable in interface wyil.lang.Code
 
OPCODE_iflt - Static variable in interface wyil.lang.Code
 
OPCODE_ifne - Static variable in interface wyil.lang.Code
 
OPCODE_ifse - Static variable in interface wyil.lang.Code
 
OPCODE_ifss - Static variable in interface wyil.lang.Code
 
OPCODE_indexof - Static variable in interface wyil.lang.Code
 
OPCODE_indirectinvokefn - Static variable in interface wyil.lang.Code
 
OPCODE_indirectinvokefnv - Static variable in interface wyil.lang.Code
 
OPCODE_indirectinvokemd - Static variable in interface wyil.lang.Code
 
OPCODE_indirectinvokemdv - Static variable in interface wyil.lang.Code
 
OPCODE_invariantblock - Static variable in interface wyil.lang.Code
 
OPCODE_invert - Static variable in interface wyil.lang.Code
 
OPCODE_invokefn - Static variable in interface wyil.lang.Code
 
OPCODE_invokefnv - Static variable in interface wyil.lang.Code
 
OPCODE_invokemd - Static variable in interface wyil.lang.Code
 
OPCODE_invokemdv - Static variable in interface wyil.lang.Code
 
OPCODE_lambdafn - Static variable in interface wyil.lang.Code
 
OPCODE_lambdamd - Static variable in interface wyil.lang.Code
 
OPCODE_lengthof - Static variable in interface wyil.lang.Code
 
OPCODE_listgen - Static variable in interface wyil.lang.Code
 
OPCODE_loop - Static variable in interface wyil.lang.Code
 
OPCODE_lshr - Static variable in interface wyil.lang.Code
 
OPCODE_move - Static variable in interface wyil.lang.Code
 
OPCODE_mul - Static variable in interface wyil.lang.Code
 
OPCODE_neg - Static variable in interface wyil.lang.Code
 
OPCODE_newlist - Static variable in interface wyil.lang.Code
 
OPCODE_newobject - Static variable in interface wyil.lang.Code
 
OPCODE_newrecord - Static variable in interface wyil.lang.Code
 
OPCODE_newtuple - Static variable in interface wyil.lang.Code
 
OPCODE_nop - Static variable in interface wyil.lang.Code
 
OPCODE_not - Static variable in interface wyil.lang.Code
 
OPCODE_numerator - Static variable in interface wyil.lang.Code
 
OPCODE_quantify - Static variable in interface wyil.lang.Code
 
OPCODE_rem - Static variable in interface wyil.lang.Code
 
OPCODE_return - Static variable in interface wyil.lang.Code
 
OPCODE_returnv - Static variable in interface wyil.lang.Code
 
OPCODE_rshr - Static variable in interface wyil.lang.Code
 
OPCODE_sub - Static variable in interface wyil.lang.Code
 
OPCODE_switch - Static variable in interface wyil.lang.Code
 
OPCODE_throw - Static variable in interface wyil.lang.Code
 
OPCODE_trycatch - Static variable in interface wyil.lang.Code
 
OPCODE_tupleload - Static variable in interface wyil.lang.Code
 
OPCODE_update - Static variable in interface wyil.lang.Code
 
OPCODE_void - Static variable in interface wyil.lang.Code
 
OPCODE_wide - Static variable in interface wyil.lang.Code
 
OPCODE_widerest - Static variable in interface wyil.lang.Code
 
OPCODE_widewide - Static variable in interface wyil.lang.Code
 
operand - Variable in class wycs.syntax.Expr.Cast
 
operand - Variable in class wycs.syntax.Expr.FieldAccess
 
operand - Variable in class wycs.syntax.Expr.IndexOf
 
operand - Variable in class wycs.syntax.Expr.IndirectInvoke
 
operand - Variable in class wycs.syntax.Expr.Invoke
 
operand - Variable in class wycs.syntax.Expr.Quantifier
 
operand - Variable in class wycs.syntax.Expr.Unary
 
operand(int) - Method in class wyil.lang.Code.AbstractNaryAssignable
Return the ith operand read by this bytecode.
operand - Variable in class wyil.lang.Code.AbstractUnaryOp
 
operands - Variable in class wycs.core.Code
An array of zero of more code operands.
operands - Variable in class wycs.syntax.Expr.Nary
 
operands - Variable in class wycs.syntax.Expr.Record
 
operands() - Method in class wyil.lang.Code.AbstractNaryAssignable
 
Operator(String, int) - Constructor for class wycc.io.Token.Operator
 
OperatorRule(String[]) - Constructor for class wycc.io.AbstractLexer.OperatorRule
 
OptArg - Class in wycc.util
A small utility for parsing command-line options.
OptArg(String, String) - Constructor for class wycc.util.OptArg
Construct an option object which does not accept an argument.
OptArg(String, String, String) - Constructor for class wycc.util.OptArg
Construct an option object with a short form which does not accept an argument.
OptArg(String, OptArg.Kind, String) - Constructor for class wycc.util.OptArg
Construct an option object which accepts an argument.
OptArg(String, String, OptArg.Kind, String) - Constructor for class wycc.util.OptArg
Construct an option object with a short form which accepts an argument.
OptArg(String, OptArg.Kind, String, Object) - Constructor for class wycc.util.OptArg
Construct an option object which accepts an argument and has a default value.
OptArg(String, String, OptArg.Kind, String, Object) - Constructor for class wycc.util.OptArg
Construct an option object with a short form which accepts an argument and has a default value.
option - Variable in class wycc.util.OptArg
The long form of the option.
Option - Class in wycs.solver.smt
A utility class for some options provided by some of the solvers specified in wycs.solver.smt.Solver.
options - Variable in class wyc.WycMain
The command-line options accepted by the main method.
options - Variable in class wycc.lang.Pipeline.Modifier
 
options - Variable in class wycc.lang.Pipeline.Template
 
options - Variable in class wycs.WycsMain
The command-line options accepted by the main method.
Or(SemanticType...) - Static method in class wycs.core.SemanticType
 
Or(Collection<SemanticType>) - Static method in class wycs.core.SemanticType
 
Or(Automaton, int...) - Static method in class wycs.solver.Solver
 
Or(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
or(Content.Filter<T>, Content.Filter<T>) - Static method in class wyfs.lang.Content
Combine two filters together produce one filter whose items must be matched by at least one of the original filters.
or(WyByte) - Method in class wyjc.runtime.WyByte
 
Origin(String, int, int, int) - Constructor for class wycc.lang.Attribute.Origin
 
original() - Method in exception wycs.transforms.VerificationCheck.AssertionFailure
 
OrT(Automaton, int...) - Static method in class wycs.core.Types
 
OrT(Automaton, List<Integer>) - Static method in class wycs.core.Types
 
OrT(Automaton, int...) - Static method in class wycs.solver.Solver
 
OrT(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
output - Variable in class wyfs.io.BinaryOutputStream
 
outputSourceError(PrintStream) - Method in exception wycc.lang.SyntaxError
Output the syntax error to a given output stream in full form.
outputSourceError(PrintStream, boolean) - Method in exception wycc.lang.SyntaxError
Output the syntax error to a given output stream in either full or brief form.
outputStream() - Method in interface wyfs.lang.Path.Entry
Open a generic output stream to the entry.
outputStream() - Method in class wyfs.util.DirectoryRoot.Entry
 
outputStream() - Method in class wyfs.util.VirtualRoot.Entry
 
owner - Variable in class wyjc.Wyil2JavaBuilder
Type of enclosing class being generated

P

pad_u8() - Method in class wyfs.io.BinaryInputStream
 
pad_u8() - Method in class wyfs.io.BinaryOutputStream
Pad out stream to nearest byte boundary
Pair<FIRST,SECOND> - Class in wycc.util
This class represents a pair of items
Pair(FIRST, SECOND) - Constructor for class wycc.util.Pair
 
param(int) - Method in class wyc.lang.Nominal.Function
 
param(int) - Method in class wyc.lang.Nominal.FunctionOrMethod
 
param(int) - Method in class wyc.lang.Nominal.Method
 
Parameter(SyntacticType, String, Attribute...) - Constructor for class wyc.lang.WhileyFile.Parameter
 
Parameter(SyntacticType, String, Collection<Attribute>) - Constructor for class wyc.lang.WhileyFile.Parameter
 
parameter(int) - Method in class wyil.lang.Codes.IndirectInvoke
Return register holding the ith parameter for the invoked function.
parameters - Variable in class wyc.lang.Expr.Lambda
 
parameters - Variable in class wyc.lang.WhileyFile.FunctionOrMethod
 
parameters() - Method in class wyil.lang.Codes.IndirectInvoke
Return registers holding parameters for the invoked function.
params() - Method in class wyc.lang.Nominal.Function
 
params() - Method in class wyc.lang.Nominal.FunctionOrMethod
 
params() - Method in class wyc.lang.Nominal.Method
 
params() - Method in class wyil.lang.Type.FunctionOrMethod
Get the parameter types of this function or method type.
paramTypes - Variable in class wyc.lang.Expr.AbstractFunctionOrMethod
 
paramTypes - Variable in class wyc.lang.SyntacticType.FunctionOrMethod
 
paramTypes - Variable in class wycs.syntax.SyntacticType.Function
 
parent() - Method in interface wyfs.lang.Path.ID
Get the parent of this path.
parent() - Method in class wyfs.util.Trie
 
parent(int) - Method in class wyfs.util.Trie
 
parent() - Method in class wyil.lang.CodeBlock.Index
 
parents() - Method in class wyil.builders.VcBranch
Return the parents for this node.
parse() - Method in class wyil.util.type.TypeParser
 
parse(HashSet<String>) - Method in class wyil.util.type.TypeParser
 
parseArrayTypePattern(HashSet<String>, boolean) - Method in class wyc.io.WhileyFileParser
 
parseAssertDeclaration(WyalFile) - Method in class wycs.io.WyalFileParser
Parse an assert declaration in a WyAL source file.
parseAssumeDeclaration(WyalFile) - Method in class wycs.io.WyalFileParser
Parse an assume declaration in a WyAL source file.
parseBraceTerm(HashSet<String>) - Method in class wyil.util.type.TypeParser
 
parseDefiniteType() - Method in class wyc.io.WhileyFileParser
Attempt to parse something which maybe a type, or an expression.
parseDefiniteType(HashSet<String>) - Method in class wycs.io.WyalFileParser
Attempt to parse something which maybe a type, or an expression.
parseFunctionTerm(HashSet<String>) - Method in class wyil.util.type.TypeParser
 
parseGenericSignature(boolean, List<String>) - Method in class wycs.io.WyalFileParser
 
parseIntersectionTypePattern(HashSet<String>, boolean) - Method in class wyc.io.WhileyFileParser
Parse an intersection type pattern, which has the form:
parseIntersectionTypePattern(HashSet<String>, HashSet<String>, boolean) - Method in class wycs.io.WyalFileParser
Parse an intersection type pattern, which has the form:
parseNotTerm(HashSet<String>) - Method in class wyil.util.type.TypeParser
 
parseOptions(List<String>, OptArg...) - Static method in class wycc.util.OptArg
Parse options from the list of arguments, removing those which are recognised.
parsePossibleTypePattern(HashSet<String>, boolean) - Method in class wyc.io.WhileyFileParser
Attempt to parse something which maybe a type pattern, or an expression.
parsePossibleTypePattern(HashSet<String>, HashSet<String>, boolean) - Method in class wycs.io.WyalFileParser
Attempt to parse something which maybe a type pattern, or an expression.
parseRationalTypePattern(HashSet<String>, boolean) - Method in class wyc.io.WhileyFileParser
Parse a rational type pattern, which has the form:
parseRationalTypePattern(HashSet<String>, HashSet<String>, boolean) - Method in class wycs.io.WyalFileParser
Parse a rational type pattern, which has the form:
parseString(String) - Method in class wyc.io.WhileyFileParser
Parse a string constant whilst interpreting all escape characters.
parseString(String) - Method in class wycs.io.WyalFileParser
Parse a string whilst interpreting all escape characters.
parseTerm(HashSet<String>) - Method in class wyil.util.type.TypeParser
 
parseTypeDeclaration(WhileyFile, List<Modifier>) - Method in class wyc.io.WhileyFileParser
Parse a type declaration in a Whiley source file, which has the form:
parseTypeDeclaration(WyalFile) - Method in class wycs.io.WyalFileParser
Parse a type declaration in a Wyal source file, which has the form:
parseTypePatternTerm(HashSet<String>, boolean) - Method in class wyc.io.WhileyFileParser
Parse a type pattern leaf, which has the form:
parseTypePatternTerm(HashSet<String>, HashSet<String>, boolean) - Method in class wycs.io.WyalFileParser
Parse a type pattern leaf, which has the form:
parseTypePatternVar(boolean) - Method in class wyc.io.WhileyFileParser
 
parseTypePatternVar(boolean) - Method in class wycs.io.WyalFileParser
 
parseUnionTypePattern(HashSet<String>, boolean) - Method in class wyc.io.WhileyFileParser
Parse a uniontype pattern "compound", which has the form:
parseUnionTypePattern(HashSet<String>, HashSet<String>, boolean) - Method in class wycs.io.WyalFileParser
Parse a uniontype pattern "compound", which has the form:
Path - Class in wyfs.lang
 
Path() - Constructor for class wyfs.lang.Path
 
Path.Entry<T> - Interface in wyfs.lang
Represents a physical item of some sort which is reachable from a Root.
Path.Filter - Interface in wyfs.lang
A generic mechanism for selecting one or more paths.
Path.Folder - Interface in wyfs.lang
An folder represents a special kind of entry which contains entries (and other folders).
Path.ID - Interface in wyfs.lang
Represents a sequence of zero or more names which describe a path through the namespace for a given project.
Path.Item - Interface in wyfs.lang
Represents an abstract or physical item of some sort which is reachable from a Root.
Path.Root - Interface in wyfs.lang
Represents the root of a hierarchy of named entries.
pattern - Variable in class wyc.lang.Stmt.VariableDeclaration
 
pattern - Variable in class wyc.lang.WhileyFile.Type
 
pattern - Variable in class wycs.syntax.Expr.Quantifier
 
pc() - Method in class wyil.builders.VcBranch
Return the current Program Counter (PC) value for this branch.
pc - Variable in class wyil.util.Interpreter.Context
 
permutations(int[]) - Static method in class wyautl_old.lang.Automata
The following method produces every possible permutation of the give array.
Pipeline<T extends CompilationUnit> - Class in wycc.lang
A Pipeline consists of a number of stages which are applied to the intermediate language (wyil).
Pipeline(List<Pipeline.Template<T>>) - Constructor for class wycc.lang.Pipeline
 
pipeline - Variable in class wycs.builders.Wyal2WycsBuilder
The list of stages which must be applied to a Wycs file.
Pipeline.Modifier - Class in wycc.lang
The pipeline modifier captures a requested adjustment to the compilation pipeline.
Pipeline.POP - Enum in wycc.lang
 
Pipeline.Template<T extends CompilationUnit> - Class in wycc.lang
A template is an uninstantiated pipeline stage.
PIPELINEAPPEND - Static variable in class wycc.util.OptArg
 
PIPELINECONFIGURE - Static variable in class wycc.util.OptArg
 
pipelineModifiers - Variable in class wyc.util.WycBuildTask
The pipeline modifiers which will be applied to the default pipeline.
pipelineModifiers - Variable in class wycs.util.WycsBuildTask
The pipeline modifiers which will be applied to the default pipeline.
PIPELINEREMOVE - Static variable in class wycc.util.OptArg
 
Pop(int) - Constructor for class wycs.solver.smt.Stmt.Pop
 
postcondition() - Method in class wyil.lang.WyilFile.FunctionOrMethod
 
precondition() - Method in class wyil.lang.WyilFile.FunctionOrMethod
 
preconditionCheck(Codes.Invoke, VcBranch, Type[], AttributedCodeBlock) - Method in class wyil.builders.VcGenerator
Generate preconditions necessary to ensure the preconditions for a method or method invocation are met.
prefixes() - Method in class wyil.builders.VcBranch
Get the static list of prefixes
prefixNormalForm(Code) - Static method in class wycs.core.NormalForms
Convert a given expression into Prefix Normal Form, where there at most one quantifier which universally quantifies the entire expression.
prepend(CodeBlock.Index) - Method in class wyil.lang.CodeBlock.Index
Prepend a given index onto the front of this index;
Primitive(Attribute...) - Constructor for class wycs.syntax.SyntacticType.Primitive
 
Primitive(Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Primitive
 
print(WhileyFile) - Method in class wyc.io.WhileyFilePrinter
 
print(WhileyFile.Declaration) - Method in class wyc.io.WhileyFilePrinter
 
print(WhileyFile.FunctionOrMethod) - Method in class wyc.io.WhileyFilePrinter
 
print(WhileyFile.Import) - Method in class wyc.io.WhileyFilePrinter
 
print(WhileyFile.Constant) - Method in class wyc.io.WhileyFilePrinter
 
print(WhileyFile.Type) - Method in class wyc.io.WhileyFilePrinter
 
print(List<Stmt>, int) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt, int) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.Assert) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.Assume) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.Debug) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.Break) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.Continue) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.Skip) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.Return) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.Assign) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.IfElse, int) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.DoWhile, int) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.While, int) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.Switch, int) - Method in class wyc.io.WhileyFilePrinter
 
print(Stmt.VariableDeclaration, int) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.Constant) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.AbstractVariable) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.ConstantAccess) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.ArrayInitialiser) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.BinOp) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.LengthOf) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.Dereference) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.Cast) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.IndexOf) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.UnOp) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.AbstractInvoke) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.IndirectFunctionCall) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.IndirectMethodCall) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.Quantifier) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.FieldAccess) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.Record) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.Tuple) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.AbstractFunctionOrMethod) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.Lambda) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.New) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.TypeVal) - Method in class wyc.io.WhileyFilePrinter
 
print(Expr.RationalLVal) - Method in class wyc.io.WhileyFilePrinter
 
print(List<Modifier>) - Method in class wyc.io.WhileyFilePrinter
 
print(TypePattern) - Method in class wyc.io.WhileyFilePrinter
 
print(SyntacticType) - Method in class wyc.io.WhileyFilePrinter
 
print() - Method in class wyil.util.AbstractAttributeMap
 
print(AbstractAttributeMap.Block<?>) - Static method in class wyil.util.AbstractAttributeMap
 
print(String, AbstractAttributeMap.Block<?>) - Static method in class wyil.util.AbstractAttributeMap
 
print(WyList) - Static method in class wyjc.runtime.Util
 
PRINT_SUCCESS - Static variable in class wycs.solver.smt.Option
Boolean.
printAccepts(BitSet, ArrayList<DefaultInterpretation.Term>) - Static method in class wyautl_old.util.Tester
 
println(WyList) - Static method in class wyjc.runtime.Util
 
printStackTrace(PrintStream, Throwable) - Static method in class wyc.WycMain
Print a complete stack trace.
printWithBrackets(Expr, Class<? extends Expr>...) - Method in class wyc.io.WhileyFilePrinter
 
PRIVATE - Static variable in interface wyil.lang.Modifier
 
process(WycsFile, Transform<WycsFile>) - Method in class wycs.builders.Wyal2WycsBuilder
 
project() - Method in interface wybs.lang.Builder
Get the project this builder is operating on.
project() - Method in class wyc.builder.WhileyBuilder
 
project - Variable in class wycs.builders.Wyal2WycsBuilder
The master project for identifying all resources available to the builder.
project() - Method in class wycs.builders.Wyal2WycsBuilder
 
project - Variable in class wycs.builders.Wycs2WyalBuilder
The master namespace for identifying all resources available to the builder.
project() - Method in class wycs.builders.Wycs2WyalBuilder
 
project - Variable in class wyil.builders.Wyil2WyalBuilder
The master namespace for identifying all resources available to the builder.
project() - Method in class wyil.builders.Wyil2WyalBuilder
 
project - Variable in class wyjc.Wyil2JavaBuilder
The master project for identifying all resources available to the builder.
project() - Method in class wyjc.Wyil2JavaBuilder
 
propagate(List<WhileyFile>) - Method in class wyc.builder.FlowTypeChecker
 
propagate(WhileyFile) - Method in class wyc.builder.FlowTypeChecker
 
propagate(WhileyFile.Type) - Method in class wyc.builder.FlowTypeChecker
Resolve types for a given type declaration.
propagate(WhileyFile.Constant) - Method in class wyc.builder.FlowTypeChecker
Propagate and check types for a given constant declaration.
propagate(WhileyFile.FunctionOrMethod) - Method in class wyc.builder.FlowTypeChecker
Propagate and check types for a given function or method declaration.
propagate(Expr, FlowTypeChecker.Environment, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
Propagate types through a given expression, whilst checking that it is well typed.
propagate(CodeBlock.Index, Code, HashSet<Integer>) - Method in class wyil.checks.DefiniteAssignmentCheck
 
propagate(CodeBlock.Index, Codes.If, HashSet<Integer>) - Method in class wyil.checks.DefiniteAssignmentCheck
 
propagate(CodeBlock.Index, Codes.IfIs, HashSet<Integer>) - Method in class wyil.checks.DefiniteAssignmentCheck
 
propagate(CodeBlock.Index, Codes.Switch, HashSet<Integer>) - Method in class wyil.checks.DefiniteAssignmentCheck
 
propagate(CodeBlock.Index, Codes.Loop, HashSet<Integer>) - Method in class wyil.checks.DefiniteAssignmentCheck
 
propagate(WyilFile.Type) - Method in class wyil.transforms.ConstantPropagation
 
propagate(WyilFile.FunctionOrMethod) - Method in class wyil.transforms.ConstantPropagation
 
propagate(AttributedCodeBlock) - Method in class wyil.transforms.ConstantPropagation
 
propagate(CodeBlock.Index, Code, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
propagate(CodeBlock.Index, Codes.If, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
propagate(CodeBlock.Index, Codes.IfIs, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
propagate(CodeBlock.Index, Codes.Switch, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
propagate(CodeBlock.Index, Codes.Loop, ConstantPropagation.Env) - Method in class wyil.transforms.ConstantPropagation
 
propagate(WyilFile.Type) - Method in class wyil.transforms.LiveVariablesAnalysis
 
propagate(WyilFile.FunctionOrMethod) - Method in class wyil.transforms.LiveVariablesAnalysis
 
propagate(AttributedCodeBlock) - Method in class wyil.transforms.LiveVariablesAnalysis
 
propagate(CodeBlock.Index, Code, LiveVariablesAnalysis.Env) - Method in class wyil.transforms.LiveVariablesAnalysis
 
propagate(CodeBlock.Index, Codes.If, LiveVariablesAnalysis.Env, LiveVariablesAnalysis.Env) - Method in class wyil.transforms.LiveVariablesAnalysis
 
propagate(Type, LiveVariablesAnalysis.Env, LiveVariablesAnalysis.Env) - Method in class wyil.transforms.LiveVariablesAnalysis
 
propagate(CodeBlock.Index, Codes.IfIs, LiveVariablesAnalysis.Env, LiveVariablesAnalysis.Env) - Method in class wyil.transforms.LiveVariablesAnalysis
 
propagate(CodeBlock.Index, Codes.Switch, List<LiveVariablesAnalysis.Env>, LiveVariablesAnalysis.Env) - Method in class wyil.transforms.LiveVariablesAnalysis
 
propagate(CodeBlock.Index, Codes.Loop, LiveVariablesAnalysis.Env, List<Pair<Type, String>>) - Method in class wyil.transforms.LiveVariablesAnalysis
 
propagate(WyilFile.Constant) - Method in class wyil.util.dfa.BackwardFlowAnalysis
 
propagate(WyilFile.Type) - Method in class wyil.util.dfa.BackwardFlowAnalysis
 
propagate(WyilFile.FunctionOrMethod) - Method in class wyil.util.dfa.BackwardFlowAnalysis
 
propagate(CodeBlock.Index, CodeBlock, T, List<Pair<Type, String>>) - Method in class wyil.util.dfa.BackwardFlowAnalysis
Propagate a given store backwards through this bytecode block.
propagate(CodeBlock.Index, Codes.If, T, T) - Method in class wyil.util.dfa.BackwardFlowAnalysis
Propagate back from a conditional branch.
propagate(CodeBlock.Index, Codes.IfIs, T, T) - Method in class wyil.util.dfa.BackwardFlowAnalysis
Propagate back from a type test.
propagate(CodeBlock.Index, Codes.Switch, List<T>, T) - Method in class wyil.util.dfa.BackwardFlowAnalysis
Propagate back from a multi-way branch.
propagate(CodeBlock.Index, Codes.Loop, T, List<Pair<Type, String>>) - Method in class wyil.util.dfa.BackwardFlowAnalysis
Propagate back from a loop statement, producing a store which holds true immediately before the statement
propagate(CodeBlock.Index, Code, T) - Method in class wyil.util.dfa.BackwardFlowAnalysis
Propagate back from a sequential statement, producing a store which holds true immediately after the statement
propagate(Type, T, T) - Method in class wyil.util.dfa.BackwardFlowAnalysis
Propagate from an exception handler.
propagate(WyilFile.Constant) - Method in class wyil.util.dfa.ForwardFlowAnalysis
 
propagate(WyilFile.Type) - Method in class wyil.util.dfa.ForwardFlowAnalysis
 
propagate(WyilFile.FunctionOrMethod) - Method in class wyil.util.dfa.ForwardFlowAnalysis
 
propagate(CodeBlock.Index, CodeBlock, T) - Method in class wyil.util.dfa.ForwardFlowAnalysis
Propagate a given store forwards through this bytecode block.
propagate(CodeBlock.Index, Codes.If, T) - Method in class wyil.util.dfa.ForwardFlowAnalysis
Propagate through a conditional branch.
propagate(CodeBlock.Index, Codes.IfIs, T) - Method in class wyil.util.dfa.ForwardFlowAnalysis
Propagate through a type test.
propagate(CodeBlock.Index, Codes.Switch, T) - Method in class wyil.util.dfa.ForwardFlowAnalysis
Propagate through a multi-way branch.
propagate(CodeBlock.Index, Codes.Loop, T) - Method in class wyil.util.dfa.ForwardFlowAnalysis
Propagate through a loop statement, producing a store which holds true immediately after the statement
propagate(CodeBlock.Index, Code, T) - Method in class wyil.util.dfa.ForwardFlowAnalysis
Propagate through a sequential statement, producing a store which holds true immediately after the statement
propagateCondition(Expr, boolean, FlowTypeChecker.Environment, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
Propagate type information through an expression being used as a condition, whilst checking it is well-typed at the same time.
PUBLIC - Static variable in interface wyil.lang.Modifier
 
Push(int) - Constructor for class wycs.solver.smt.Stmt.Push
 
put(int, String) - Method in class wyc.builder.CodeGenerator.Environment
 
put(CodeBlock.Index, SourceLocation) - Method in class wyil.attributes.SourceLocationMap
 
put(CodeBlock.Index, T) - Method in interface wyil.lang.Attribute.Map
Assign or update the meta-data associated with a given bytecode location.
put(CodeBlock.Index, T) - Method in class wyil.util.AbstractAttributeMap
Associate an attribute with a given bytecode location.
put(WyRecord, String, Object) - Static method in class wyjc.runtime.WyRecord
 

Q

qualification - Variable in class wyc.lang.Expr.AbstractInvoke
 
qualification - Variable in class wyc.lang.Expr.ConstantAccess
 
qualification - Variable in class wycs.syntax.Expr.ConstantAccess
 
qualification - Variable in class wycs.syntax.Expr.Invoke
 
Quantifier(Expr.QOp, Collection<Triple<String, Expr, Expr>>, Expr, Attribute...) - Constructor for class wyc.lang.Expr.Quantifier
 
Quantifier(SemanticType, Code.Op, Code<?>, Pair<SemanticType, Integer>[], Attribute...) - Static method in class wycs.core.Code
 
Quantifier(SemanticType, Code.Op, Code<?>, Pair<SemanticType, Integer>[], Collection<Attribute>) - Static method in class wycs.core.Code
 
Quantifier(TypePattern, Expr, Attribute...) - Constructor for class wycs.syntax.Expr.Quantifier
 
Quantifier(TypePattern, Expr, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.Quantifier
 
Quantify(int, int, int, int[], Collection<Code>) - Static method in class wyil.lang.Codes
 
Quantify(int, int, int, int[], Code...) - Static method in class wyil.lang.Codes
 

R

range(BigInteger, BigInteger) - Static method in class wyjc.runtime.WyList
Return a list constructed from the range of two integers.
Rational(TypePattern, TypePattern, Attribute...) - Constructor for class wyc.lang.TypePattern.Rational
 
Rational(TypePattern, TypePattern, List<Attribute>) - Constructor for class wyc.lang.TypePattern.Rational
 
Rational(TypePattern, TypePattern, Attribute...) - Constructor for class wycs.syntax.TypePattern.Rational
 
Rational(TypePattern, TypePattern, Collection<Attribute>) - Constructor for class wycs.syntax.TypePattern.Rational
 
RationalLVal(Expr.LVal, Expr.LVal, Attribute...) - Constructor for class wyc.lang.Expr.RationalLVal
 
raw() - Method in class wyc.lang.Nominal.Base
 
raw() - Method in class wyc.lang.Nominal.Function
 
raw() - Method in class wyc.lang.Nominal.FunctionOrMethod
 
raw() - Method in class wyc.lang.Nominal.List
 
raw() - Method in class wyc.lang.Nominal.Method
 
raw() - Method in class wyc.lang.Nominal
 
raw() - Method in class wyc.lang.Nominal.Record
 
raw() - Method in class wyc.lang.Nominal.Reference
 
raw() - Method in class wyc.lang.Nominal.Tuple
 
rawType() - Method in class wyil.lang.Codes.LVal
 
read() - Method in class wyautl_old.io.BinaryAutomataReader
 
read() - Method in interface wyautl_old.io.GenericReader
 
read() - Method in class wyc.io.WhileyFileParser
Read a WhileyFile from the token stream.
read() - Method in class wycs.io.WyalFileParser
Read a WyalFile from the token stream.
read() - Method in class wycs.io.WyalFileReader
 
read() - Method in class wycs.io.WycsFileReader
 
read() - Method in class wyfs.io.BinaryInputStream
 
read(byte[]) - Method in class wyfs.io.BinaryInputStream
 
read(byte[], int, int) - Method in class wyfs.io.BinaryInputStream
 
read(Path.Entry<T>, InputStream) - Method in interface wyfs.lang.Content.Type
Physically read the raw bytes from a given input stream and convert into the format described by this content type.
read() - Method in interface wyfs.lang.Path.Entry
Read contents of file.
read() - Method in class wyfs.util.AbstractEntry
 
read(int) - Method in class wyil.builders.VcBranch
Get the constraint variable which corresponds to the given Wyil bytecode register at this point on this branch.
read(Path.ID, InputStream) - Method in interface wyil.io.ModuleReader
Read a given given module from an input stream.
read() - Method in class wyil.io.WyilFileReader
 
read_bit() - Method in class wyfs.io.BinaryInputStream
 
read_u16() - Method in class wyfs.io.BinaryInputStream
 
read_u32() - Method in class wyfs.io.BinaryInputStream
 
read_u8() - Method in class wyfs.io.BinaryInputStream
 
read_un(int) - Method in class wyfs.io.BinaryInputStream
 
read_uv() - Method in class wyfs.io.BinaryInputStream
 
readAutomatas(GenericReader<Automaton>, boolean) - Static method in class wyautl_old.util.Tester
 
readCodeBlock(int, int, HashMap<Integer, Codes.Label>) - Method in class wyil.io.WyilFileReader
Read all bytecodes between two given offsets.
reader - Variable in class wyautl_old.io.BinaryAutomataReader
 
readModel(GenericReader<Automaton>, boolean) - Static method in class wyautl_old.util.Tester
 
readState() - Method in class wyautl_old.io.BinaryAutomataReader
 
readState() - Method in class wyil.lang.Type.BinaryReader
 
readType() - Method in class wyil.lang.Type.BinaryReader
 
Real(Attribute...) - Constructor for class wyc.lang.SyntacticType.Real
 
Real(List<Attribute>) - Constructor for class wyc.lang.SyntacticType.Real
 
Real - Static variable in class wycs.core.SemanticType
 
REAL - Static variable in class wycs.solver.smt.Sort
The singleton real sort.
Real(Attribute...) - Constructor for class wycs.syntax.SyntacticType.Real
 
Real(Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Real
 
Real(List<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Real
 
REAL - Static variable in class wyjc.runtime.WyType
 
RealT - Static variable in class wycs.core.Types
 
RealT - Static variable in class wycs.solver.Solver
 
rebind(Map<Integer, Integer>) - Method in class wycs.core.Code.Quantifier
 
rebind(Map<Integer, Integer>) - Method in class wycs.core.Code
Rebind variables within the given expression.
rebind(Map<Integer, Integer>) - Method in class wycs.core.Code.Variable
 
Record(Map<String, Expr>, Attribute...) - Constructor for class wyc.lang.Expr.Record
 
Record(boolean, Map<String, Nominal>) - Static method in class wyc.lang.Nominal
 
Record(boolean, Map<String, SyntacticType>, Attribute...) - Constructor for class wyc.lang.SyntacticType.Record
 
Record(boolean, Map<String, SyntacticType>, List<Attribute>) - Constructor for class wyc.lang.SyntacticType.Record
 
Record(SyntacticType.Record, Attribute...) - Constructor for class wyc.lang.TypePattern.Record
 
Record(List<TypePattern.Leaf>, boolean, Attribute...) - Constructor for class wyc.lang.TypePattern.Record
 
Record(List<TypePattern.Leaf>, boolean, List<Attribute>) - Constructor for class wyc.lang.TypePattern.Record
 
Record(List<Pair<String, Expr>>, Attribute...) - Constructor for class wycs.syntax.Expr.Record
 
Record(List<Pair<String, Expr>>, Collection<Attribute>) - Constructor for class wycs.syntax.Expr.Record
 
Record(boolean, Collection<Pair<SyntacticType, Expr.Variable>>, Attribute...) - Constructor for class wycs.syntax.SyntacticType.Record
 
Record(boolean, Collection<Pair<SyntacticType, Expr.Variable>>, Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Record
 
Record(SyntacticType.Record, Attribute...) - Constructor for class wycs.syntax.TypePattern.Record
 
Record(List<TypePattern.Leaf>, boolean, Attribute...) - Constructor for class wycs.syntax.TypePattern.Record
 
Record(List<TypePattern.Leaf>, boolean, Collection<Attribute>) - Constructor for class wycs.syntax.TypePattern.Record
 
Record(boolean, Map<String, Type>) - Static method in class wyil.lang.Type
Construct a record type using the given fields.
Record(String[], WyType[], boolean) - Constructor for class wyjc.runtime.WyType.Record
 
RECORD_MISSING_FIELD - Static variable in class wyil.util.ErrorMessages
 
RECORD_TYPE_REQUIRED - Static variable in class wyil.util.ErrorMessages
 
RecordLVal(Type.EffectiveRecord, String) - Constructor for class wyil.lang.Codes.RecordLVal
 
RECURSIVE - Variable in class wyautl_old.util.Generator.Config
Allow recursive links or not.
Recursive(NameID, Type) - Static method in class wyil.lang.Type
Close a recursive type using a given label (i.e.
reduction() - Method in exception wycs.transforms.VerificationCheck.AssertionFailure
 
reductions - Static variable in class wycs.core.Types
 
reductions - Static variable in class wycs.solver.Solver
 
Reference(Nominal) - Static method in class wyc.lang.Nominal
 
Reference(SyntacticType, Attribute...) - Constructor for class wyc.lang.SyntacticType.Reference
 
Reference(SyntacticType, Attribute...) - Constructor for class wycs.syntax.SyntacticType.Reference
 
Reference(SyntacticType, Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Reference
 
reference() - Method in class wyil.lang.Codes.IndirectInvoke
Return register holding the indirect function/method reference.
Reference(Type) - Static method in class wyil.lang.Type
Construct a reference type using the given element type.
Reference(WyType) - Constructor for class wyjc.runtime.WyType.Reference
 
REFERENCE_ACCESS_NOT_PERMITTED_IN_FUNCTION - Static variable in class wyil.util.ErrorMessages
 
REFERENCE_NOT_PERMITTED_IN_FUNCTION - Static variable in class wyil.util.ErrorMessages
 
ReferenceLVal(Type.Reference) - Constructor for class wyil.lang.Codes.ReferenceLVal
 
refresh() - Method in class wybs.util.StdProject
Force root to refresh entries from permanent storage (where appropriate).
refresh() - Method in interface wyfs.lang.Path.Item
Force item to refresh contents from permanent storage (where appropriate).
refresh() - Method in interface wyfs.lang.Path.Root
Force root to refresh entries from permanent storage (where appropriate).
refresh() - Method in class wyfs.util.AbstractEntry
 
refresh() - Method in class wyfs.util.AbstractFolder
 
refresh() - Method in class wyfs.util.AbstractRoot
 
refresh() - Method in class wyfs.util.JarFileRoot
 
REG_0 - Static variable in class wyil.lang.Codes
Provided to aid readability of client code.
REG_1 - Static variable in class wyil.lang.Codes
Provided to aid readability of client code.
REG_2 - Static variable in class wyil.lang.Codes
Provided to aid readability of client code.
REG_3 - Static variable in class wyil.lang.Codes
Provided to aid readability of client code.
REG_4 - Static variable in class wyil.lang.Codes
Provided to aid readability of client code.
REG_5 - Static variable in class wyil.lang.Codes
Provided to aid readability of client code.
REG_6 - Static variable in class wyil.lang.Codes
Provided to aid readability of client code.
REG_7 - Static variable in class wyil.lang.Codes
Provided to aid readability of client code.
REG_8 - Static variable in class wyil.lang.Codes
Provided to aid readability of client code.
REG_9 - Static variable in class wyil.lang.Codes
Provided to aid readability of client code.
register(Class<? extends Transform<S>>) - Static method in class wycc.lang.Pipeline
Register a transform with the system, in order that it can be used in a given Pipeline.
registers(Set<Integer>) - Method in class wyil.lang.Code.AbstractBinaryOp
 
registers(Set<Integer>) - Method in class wyil.lang.Code.AbstractNaryAssignable
 
registers(Set<Integer>) - Method in class wyil.lang.Code.AbstractUnaryOp
 
registers(Set<Integer>) - Method in class wyil.lang.Code.Compound
 
registers(Set<Integer>) - Method in interface wyil.lang.Code
Determine which registers are used in this bytecode.
registers(Set<Integer>) - Method in class wyil.lang.Code.Unit
 
registers(Set<Integer>) - Method in class wyil.lang.Codes.Const
 
registers(Set<Integer>) - Method in class wyil.lang.Codes.Quantify
 
registry - Variable in class wyc.util.WycBuildTask
The master project content type registry.
Registry() - Constructor for class wyc.util.WycBuildTask.Registry
 
registry - Variable in class wycs.util.WycsBuildTask
The master project content type registry.
Registry() - Constructor for class wycs.util.WycsBuildTask.Registry
 
Registry() - Constructor for class wyil.Main.Registry
 
Registry() - Constructor for class wyjc.util.WyjcBuildTask.Registry
 
relabel(Map<String, String>) - Method in class wyil.lang.Codes.Goto
 
relabel(Map<String, String>) - Method in class wyil.lang.Codes.If
 
relabel(Map<String, String>) - Method in class wyil.lang.Codes.IfIs
 
relabel(Map<String, String>) - Method in class wyil.lang.Codes.Label
 
relabel(Map<String, String>) - Method in class wyil.lang.Codes.Switch
 
Relation - Interface in wyautl_old.lang
A relation is used to determining whether a relationship exists between two automata.
remainder(Value.Integer) - Method in class wycs.core.Value.Integer
 
remainder(Constant.Integer) - Method in class wyil.lang.Constant.Integer
 
remap(Automaton, int[]) - Static method in class wyautl_old.lang.Automata
The remap method takes an automaton, and a mapping from vertices in the old space to the those in the new space.
remap(Automaton.State, int[]) - Static method in class wyautl_old.lang.Automata
The remap method takes a node, and mapping from vertices in the old space to the those in the new space.
remap(Map<Integer, Integer>) - Method in class wyil.lang.Code.AbstractBinaryOp
 
remap(Map<Integer, Integer>) - Method in class wyil.lang.Code.AbstractNaryAssignable
 
remap(Map<Integer, Integer>) - Method in class wyil.lang.Code.AbstractUnaryOp
 
remap(Map<Integer, Integer>) - Method in class wyil.lang.Code.Compound
 
remap(Map<Integer, Integer>) - Method in interface wyil.lang.Code
Remaps all registers according to a given binding.
remap(Map<Integer, Integer>) - Method in class wyil.lang.Code.Unit
 
remap(Map<Integer, Integer>) - Method in class wyil.lang.Codes.Const
 
remap(Map<Integer, Integer>) - Method in class wyil.lang.Codes.Loop
 
remap(Map<Integer, Integer>) - Method in class wyil.lang.Codes.Quantify
 
remapOperands(Map<Integer, Integer>, int[]) - Static method in class wyil.lang.CodeUtils
 
remove(Value) - Method in class wycs.core.Value.Array
 
remove(int) - Method in class wyil.lang.CodeBlock
Remove the bytecode at a given position in this block with another.
renameVariables(Code) - Static method in class wycs.core.NormalForms
Traverse the expression rename bound variables to ensure there is no potential for variable capture during the conversion to PNF.
renameVariables(Code, int) - Static method in class wycs.core.NormalForms
Traverse the expression rename bound variables to ensure there is no potential for variable capture during the conversion to PNF.
reorder(Automaton, int[]) - Static method in class wyautl_old.lang.Automata
The reorder method takes an automaton, and a mapping from vertices in the old space to the those in the new space.
replace(WyilFile.Block, WyilFile.Block) - Method in class wyil.lang.WyilFile
 
requires - Variable in class wyc.lang.WhileyFile.FunctionOrMethod
 
RESOLUTION_ERROR - Static variable in class wyil.util.ErrorMessages
 
resolveAsConstant(NameID) - Method in class wyc.builder.FlowTypeChecker
Resolve a given name as a constant value.
resolveAsConstant(Expr, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
Resolve a given constant expression as a constant value.
resolveAsFunctionOrMethod(NameID, List<Nominal>, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
Responsible for determining the true type of a method or function being invoked.
resolveAsFunctionOrMethod(String, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
Responsible for determining the true type of a method or function being invoked.
resolveAsFunctionOrMethod(String, List<Nominal>, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
Responsible for determining the true type of a method or function being invoked.
resolveAsFunctionType(String, SemanticType, List<SemanticType>, WyalFile.Context) - Method in class wycs.builders.Wyal2WycsBuilder
This function must be called after stubs are created.
resolveAsFunctionType(NameID, SemanticType, List<SemanticType>, WyalFile.Context) - Method in class wycs.builders.Wyal2WycsBuilder
This function must be called after stubs are created.
resolveAsModule(String, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
This method attempts to resolve a name as a module in a given name context.
resolveAsModule(String, WyalFile.Context) - Method in class wycs.builders.Wyal2WycsBuilder
 
resolveAsName(String, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
Responsible for resolve names, types, constants and functions / methods at the global level.
resolveAsName(List<String>, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
This methods attempts to resolve the given list of names into a single named item (e.g.
resolveAsName(String, WyalFile.Context) - Method in class wycs.builders.Wyal2WycsBuilder
Resolve a name found at a given context in a source file to determine its fully qualified name.
resolveAsType(SyntacticType.Function, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
 
resolveAsType(SyntacticType.Method, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
 
resolveAsType(SyntacticType, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
Resolve a type in a given context by identifying all unknown names and replacing them with nominal types.
resolveAsUnconstrainedType(SyntacticType, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker
Resolve a type in a given context by identifying all unknown names and replacing them with nominal types.
resolvedType - Variable in class wyc.lang.WhileyFile.Function
 
resolvedType() - Method in class wyc.lang.WhileyFile.Function
 
resolvedType() - Method in class wyc.lang.WhileyFile.FunctionOrMethod
 
resolvedType - Variable in class wyc.lang.WhileyFile.Method
 
resolvedType() - Method in class wyc.lang.WhileyFile.Method
 
resolvedType - Variable in class wyc.lang.WhileyFile.Type
 
resolvedValue - Variable in class wyc.lang.WhileyFile.Constant
 
ResolveError - Exception in wycc.util
A resolve error is thrown by the ModuleLoader, when it was unable to resolve a given class or package.
ResolveError(String) - Constructor for exception wycc.util.ResolveError
 
ResolveError(String, Throwable) - Constructor for exception wycc.util.ResolveError
 
Response - Class in wycs.solver.smt
Utility class for constants representing the response of a SMT solver.
result() - Method in class wyc.lang.Expr.AbstractFunctionOrMethod
 
result() - Method in class wyc.lang.Expr.AbstractIndirectInvoke
 
result() - Method in class wyc.lang.Expr.AbstractInvoke
 
result() - Method in class wyc.lang.Expr.AbstractVariable
 
result() - Method in class wyc.lang.Expr.ArrayGenerator
 
result() - Method in class wyc.lang.Expr.ArrayInitialiser
 
result() - Method in class wyc.lang.Expr.BinOp
 
result() - Method in class wyc.lang.Expr.Cast
 
result() - Method in class wyc.lang.Expr.Constant
 
result() - Method in class wyc.lang.Expr.ConstantAccess
 
result() - Method in class wyc.lang.Expr.Dereference
 
result() - Method in class wyc.lang.Expr.FieldAccess
 
result() - Method in class wyc.lang.Expr.FunctionCall
 
result() - Method in class wyc.lang.Expr.IndexOf
 
result() - Method in class wyc.lang.Expr.IndirectFunctionCall
 
result() - Method in class wyc.lang.Expr.IndirectMethodCall
 
result() - Method in class wyc.lang.Expr.Lambda
 
result() - Method in class wyc.lang.Expr.LengthOf
 
result() - Method in class wyc.lang.Expr.LocalVariable
 
result() - Method in class wyc.lang.Expr.MethodCall
 
result() - Method in class wyc.lang.Expr.New
 
result() - Method in class wyc.lang.Expr.Quantifier
 
result() - Method in class wyc.lang.Expr.RationalLVal
 
result() - Method in class wyc.lang.Expr.Record
 
result() - Method in interface wyc.lang.Expr
Get the type that this expression will evaluate to.
result() - Method in class wyc.lang.Expr.Tuple
 
result() - Method in class wyc.lang.Expr.TypeVal
 
result() - Method in class wyc.lang.Expr.UnOp
 
RESULT(int) - Constructor for class wycs.transforms.VerificationCheck.RESULT
 
result - Variable in class wyil.lang.Codes.Convert
 
result() - Method in class wyil.lang.Codes.Update
Returns register from which assigned value is read.
ret() - Method in class wyc.lang.Nominal.Function
 
ret() - Method in class wyc.lang.Nominal.FunctionOrMethod
 
ret() - Method in class wyc.lang.Nominal.Method
 
ret - Variable in class wyc.lang.SyntacticType.FunctionOrMethod
 
ret - Variable in class wyc.lang.WhileyFile.FunctionOrMethod
 
ret - Variable in class wycs.syntax.SyntacticType.Function
 
ret() - Method in class wyil.lang.Type.FunctionOrMethod
Get the return type of this function or method type.
Return(Expr, Attribute...) - Constructor for class wyc.lang.Stmt.Return
Create a given return statement with an optional return value.
Return(Expr, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Return
Create a given return statement with an optional return value.
Return() - Static method in class wyil.lang.Codes
Construct a return bytecode which does return a value and, hence, its type automatically defaults to void.
Return(Type, int) - Static method in class wyil.lang.Codes
Construct a return bytecode which reads a value from the operand register and returns it.
RETURN_FROM_VOID - Static variable in class wyil.util.ErrorMessages
 
returnType() - Method in class wycs.core.Code.Binary
 
returnType() - Method in class wycs.core.Code.Cast
 
returnType() - Method in class wycs.core.Code.Constant
 
returnType() - Method in class wycs.core.Code.FunCall
 
returnType() - Method in class wycs.core.Code.IndexOf
 
returnType() - Method in class wycs.core.Code.Is
 
returnType() - Method in class wycs.core.Code.Load
 
returnType() - Method in class wycs.core.Code.Nary
 
returnType() - Method in class wycs.core.Code.Quantifier
 
returnType() - Method in class wycs.core.Code
Determine the most precise type capturing any value that this bytecode could evaluate to.
returnType() - Method in class wycs.core.Code.Unary
 
returnType() - Method in class wycs.core.Code.Variable
 
returnType(Expr) - Static method in class wycs.transforms.TypePropagation
Calculate the most precise type that captures those possible values a given expression can evaluate to.
retypeExpression(Expr, SemanticType, HashMap<String, SemanticType>, WyalFile.Context) - Method in class wycs.transforms.TypePropagation
Apply constraints imposed by fixing a given expression to be a given type.
rewriter() - Method in exception wycs.transforms.VerificationCheck.AssertionFailure
 
rhs - Variable in class wyc.lang.Expr.BinOp
 
rhs - Variable in class wyc.lang.Stmt.Assign
 
rhs() - Method in class wyil.lang.Codes.Update
Extract the type for the right-hand side of this assignment.
rightOperand - Variable in class wycs.syntax.Expr.Binary
 
rightOperand - Variable in class wycs.syntax.Expr.Is
 
rightOperand - Variable in class wyil.lang.Code.AbstractBinaryOp
 
rightOperand - Variable in class wyil.lang.Codes.IfIs
 
rightShift(BigInteger) - Method in class wyjc.runtime.WyByte
 
root - Variable in class wyfs.util.AbstractRoot
 
root() - Method in class wyfs.util.AbstractRoot
Get the root folder for this abstract root.
root() - Method in class wyfs.util.DirectoryRoot
 
root() - Method in class wyfs.util.JarFileRoot
 
ROOT - Static variable in class wyfs.util.Trie
 
root() - Method in class wyfs.util.VirtualRoot
 
ROOT - Static variable in class wyil.lang.CodeBlock.Index
 
rootBlock - Variable in class wyil.util.dfa.BackwardFlowAnalysis
The root block currently being propagated through.
rootBlock - Variable in class wyil.util.dfa.ForwardFlowAnalysis
The root block currently being propagated through.
rootBlock - Variable in class wyjc.Wyil2JavaBuilder
Root of block being translated
roots - Variable in class wybs.util.StdProject
The roots of all entries known to the system which form the global namespace used by the builder(s).
roots() - Method in class wybs.util.StdProject
Get the roots associated with this project.
round(int) - Method in class wyjc.runtime.WyRat
 
Rule() - Constructor for class wycc.io.AbstractLexer.Rule
 
rules - Variable in class wybs.util.StdProject
The rules associated with this project for transforming content.
rules() - Method in class wybs.util.StdProject
Get the build rules associated with this project.
run(String[]) - Method in class wyc.WycMain
 
run(String[]) - Method in class wycs.WycsMain
 

S

SAT - Static variable in class wycs.solver.smt.Response
Result is satisfiable; there is one or more models that make the assertions true.
SAT(int) - Constructor for class wycs.transforms.VerificationCheck.RESULT.SAT
 
scan() - Method in class wyc.io.WhileyFileLexer
Scan all characters from the input stream and generate a corresponding list of tokens, whilst discarding all whitespace and comments.
scan() - Method in class wycc.io.AbstractLexer
Scan the given input stream and produce a list of tokens, or an error.
scan() - Method in class wycs.io.WyalFileLexer
Scan all characters from the input stream and generate a corresponding list of tokens, whilst discarding all whitespace and comments.
scanBlockComment() - Method in class wyc.io.WhileyFileLexer
 
scanBlockComment() - Method in class wycs.io.WyalFileLexer
 
scanCharacterConstant() - Method in class wyc.io.WhileyFileLexer
Scan a character constant, such as e.g.
scanCharacterConstant() - Method in class wycs.io.WyalFileLexer
Scan a character constant, such as e.g.
scanIdentifier() - Method in class wyc.io.WhileyFileLexer
 
scanIdentifier() - Method in class wycs.io.WyalFileLexer
 
scanIndent() - Method in class wyc.io.WhileyFileLexer
Scan one or more spaces or tab characters, combining them to form an "indent".
scanIndent() - Method in class wycs.io.WyalFileLexer
Scan one or more spaces or tab characters, combining them to form an "indent".
scanLineComment() - Method in class wyc.io.WhileyFileLexer
 
scanLineComment() - Method in class wycs.io.WyalFileLexer
 
scanNumericConstant() - Method in class wyc.io.WhileyFileLexer
Scan a numeric constant.
scanNumericConstant() - Method in class wycs.io.WyalFileLexer
Scan a numeric constant.
scanOperator() - Method in class wyc.io.WhileyFileLexer
 
scanOperator() - Method in class wycs.io.WyalFileLexer
 
scanStringConstant() - Method in class wyc.io.WhileyFileLexer
 
scanStringConstant() - Method in class wycs.io.WyalFileLexer
 
scanWhiteSpace(List<WhileyFileLexer.Token>) - Method in class wyc.io.WhileyFileLexer
 
scanWhiteSpace(List<WyalFileLexer.Token>) - Method in class wycs.io.WyalFileLexer
 
SCHEMA - Static variable in class wycs.core.Types
 
SCHEMA - Static variable in class wycs.solver.Solver
 
second - Variable in class wycc.util.Pair
 
second() - Method in class wycc.util.Pair
 
selectCandidateFunctionOrMacro(NameID, SemanticType, List<SemanticType>, List<SemanticType.Function>, WyalFile.Context) - Method in class wycs.builders.Wyal2WycsBuilder
 
SemanticType - Class in wycs.core
 
SemanticType.And - Class in wycs.core
 
SemanticType.Any - Class in wycs.core
 
SemanticType.Array - Class in wycs.core
 
SemanticType.Atom - Class in wycs.core
 
SemanticType.Bool - Class in wycs.core
 
SemanticType.EffectiveTuple - Interface in wycs.core
An effective tuple is either a tuple, or a union of tuples.
SemanticType.Function - Class in wycs.core
 
SemanticType.Int - Class in wycs.core
 
SemanticType.Nary - Class in wycs.core
 
SemanticType.Nominal - Class in wycs.core
 
SemanticType.Not - Class in wycs.core
 
SemanticType.Null - Class in wycs.core
 
SemanticType.Or - Class in wycs.core
 
SemanticType.OrTuple - Class in wycs.core
 
SemanticType.Real - Class in wycs.core
 
SemanticType.String - Class in wycs.core
 
SemanticType.Tuple - Class in wycs.core
 
SemanticType.Var - Class in wycs.core
 
SemanticType.Void - Class in wycs.core
 
serialVersionUID - Static variable in exception wycc.lang.SyntaxError
 
set(int, int, boolean) - Method in class wyautl_old.util.BinaryMatrix
 
Set(String) - Constructor for class wycs.solver.smt.Sort.Set
 
set(int, VariableDeclarations.Declaration) - Method in class wyil.attributes.VariableDeclarations
 
set(int, Code) - Method in class wyil.lang.CodeBlock
Replace the bytecode at a given position in this block with another.
set(int, Code, Attribute...) - Method in class wyil.util.AttributedCodeBlock
Replace the bytecode at a given position in this block with another.
set(int, Code, Collection<Attribute>) - Method in class wyil.util.AttributedCodeBlock
Replace the bytecode at a given position in this block with another.
set(WyList, BigInteger, Object) - Static method in class wyjc.runtime.WyList
 
Set(WyType, boolean) - Constructor for class wyjc.runtime.WyType.Set
 
setAttributes(boolean) - Method in class wyil.io.WyilFilePrinter
 
setBootPath(Path) - Method in class wyc.util.WycAntTask
 
setBootPath(List<File>) - Method in class wyc.util.WycBuildTask
 
setBootPath(Path) - Method in class wycs.util.WycsAntTask
 
setBootPath(List<File>) - Method in class wycs.util.WycsBuildTask
 
setClassdir(File) - Method in class wyjc.util.WyjcAntTask
 
setClassDir(File) - Method in class wyjc.util.WyjcBuildTask
 
setDebug(boolean) - Method in class wycs.builders.Wyal2WycsBuilder
 
setDebug(boolean) - Method in class wycs.builders.Wycs2WyalBuilder
 
setDebug(boolean) - Method in class wycs.transforms.SmtVerificationCheck
Sets the value of the debug option.
setDebug(boolean) - Method in class wycs.transforms.VerificationCheck
 
setDebug(boolean) - Method in class wycs.util.WycsBuildTask
 
setDecompile(boolean) - Method in class wycs.util.WycsBuildTask
 
setEnable(boolean) - Method in class wycs.transforms.MacroExpansion
 
setEnable(boolean) - Method in class wycs.transforms.SmtVerificationCheck
Sets the value of the enable option.
setEnable(boolean) - Method in class wycs.transforms.TypePropagation
 
setEnable(boolean) - Method in class wycs.transforms.VerificationCheck
 
setEnable(boolean) - Method in class wyil.checks.DefiniteAssignmentCheck
 
setEnable(boolean) - Method in class wyil.transforms.ConstantPropagation
 
setEnable(boolean) - Method in class wyil.transforms.DeadCodeElimination
 
setEnable(boolean) - Method in class wyil.transforms.LiveVariablesAnalysis
 
setEnable(boolean) - Method in class wyil.transforms.LoopVariants
 
setEnd(int) - Method in class wyil.attributes.SourceLocation
 
setExcludes(String) - Method in class wyc.util.WycAntTask
 
setExcludes(String) - Method in class wyc.util.WycBuildTask
 
setExcludes(String) - Method in class wycs.util.WycsAntTask
 
setExcludes(String) - Method in class wycs.util.WycsBuildTask
 
setIncludes(String) - Method in class wyc.util.WycAntTask
 
setIncludes(String) - Method in class wyc.util.WycBuildTask
 
setIncludes(String) - Method in class wycs.util.WycsAntTask
 
setIncludes(String) - Method in class wycs.util.WycsBuildTask
 
setLabels(boolean) - Method in class wyil.io.WyilFilePrinter
 
setLogger(Logger) - Method in class wyc.builder.WhileyBuilder
 
setLogger(Logger) - Method in class wycs.builders.Wyal2WycsBuilder
 
setLogger(Logger) - Method in class wycs.builders.Wycs2WyalBuilder
 
setLogger(Logger) - Method in class wyil.builders.Wyil2WyalBuilder
 
setLogger(Logger) - Method in class wyjc.Wyil2JavaBuilder
 
SetLogic(Logic) - Constructor for class wycs.solver.smt.Stmt.SetLogic
 
setLogOut(PrintStream) - Method in class wyc.util.WycBuildTask
 
setLogOut(PrintStream) - Method in class wycs.util.WycsBuildTask
 
setMaxInferences(int) - Method in class wycs.transforms.VerificationCheck
 
setNops(boolean) - Method in class wyil.transforms.LiveVariablesAnalysis
 
setOption(Class<? extends Transform>, String, Object) - Method in class wycc.lang.Pipeline
Set a specific option on a given pipeline stage.
SetOption(String, String) - Constructor for class wycs.solver.smt.Stmt.SetOption
 
setPipelineModifiers(List<Pipeline.Modifier>) - Method in class wyc.util.WycBuildTask
 
setPipelineModifiers(List<Pipeline.Modifier>) - Method in class wycs.util.WycsBuildTask
 
setRwmode(String) - Method in class wycs.transforms.VerificationCheck
 
setSlots(boolean) - Method in class wyil.io.WyilFilePrinter
 
setSmtVerification(boolean) - Method in class wyc.util.WycBuildTask
 
setSolver(String) - Method in class wycs.transforms.SmtVerificationCheck
Sets the value of the solver option.
setSourceFile(String) - Method in class wyil.attributes.SourceFile
 
setSourceFile(int) - Method in class wyil.attributes.SourceLocation
 
setStart(int) - Method in class wyil.attributes.SourceLocation
 
setState(VcBranch.State) - Method in class wyil.builders.VcBranch
Update the state of this branch.
setState(Object) - Method in class wyjc.runtime.WyObject
 
setVerbose(boolean) - Method in class wyc.util.WycAntTask
 
setVerbose(boolean) - Method in class wyc.util.WycBuildTask
 
setVerbose(boolean) - Method in class wycs.util.WycsAntTask
 
setVerbose(boolean) - Method in class wycs.util.WycsBuildTask
 
setVerification(boolean) - Method in class wyc.util.WycAntTask
 
setVerification(boolean) - Method in class wyc.util.WycBuildTask
 
setVerificationConditions(boolean) - Method in class wyc.util.WycAntTask
 
setVerificationConditions(boolean) - Method in class wyc.util.WycBuildTask
 
setWhileydir(File) - Method in class wyc.util.WycAntTask
 
setWhileyDir(File) - Method in class wyc.util.WycBuildTask
 
setWhileyDir(File) - Method in class wyjc.util.WyjcBuildTask
 
setWhileyPath(Path) - Method in class wyc.util.WycAntTask
 
setWhileyPath(List<File>) - Method in class wyc.util.WycBuildTask
 
setWyaldir(File) - Method in class wyc.util.WycAntTask
 
setWyalDir(File) - Method in class wyc.util.WycBuildTask
 
setWyaldir(File) - Method in class wycs.util.WycsAntTask
 
setWyalDir(File) - Method in class wycs.util.WycsBuildTask
 
setWycsdir(File) - Method in class wyc.util.WycAntTask
 
setWycsDir(File) - Method in class wyc.util.WycBuildTask
 
setWycsdir(File) - Method in class wycs.util.WycsAntTask
 
setWycsDir(File) - Method in class wycs.util.WycsBuildTask
 
setWycsPath(Path) - Method in class wycs.util.WycsAntTask
 
setWycsPath(List<File>) - Method in class wycs.util.WycsBuildTask
 
setWyildir(File) - Method in class wyc.util.WycAntTask
 
setWyilDir(File) - Method in class wyc.util.WycBuildTask
 
setWyilDir(File) - Method in class wyjc.util.WyjcBuildTask
 
shortForm - Variable in class wycc.util.OptArg
The short form of the option.
simplify(Automaton) - Static method in class wyil.util.type.TypeAlgorithms
This simplification rule removes spurious components by repeated application of various rewrite rules.
size() - Method in class wyautl_old.lang.Automaton
 
SIZE - Variable in class wyautl_old.util.Generator.Config
Determine size of automata to generate.
size() - Method in class wyc.builder.CodeGenerator.Environment
 
size() - Method in interface wycs.core.SemanticType.EffectiveTuple
Returns the number of direct addressable elements.
size() - Method in class wycs.core.SemanticType.OrTuple
 
size() - Method in class wycs.core.SemanticType.Tuple
 
size() - Method in interface wyfs.lang.Path.ID
Get the number of components that make up this ID.
size() - Method in class wyfs.util.Trie
 
size() - Method in class wyil.attributes.VariableDeclarations
 
size() - Method in class wyil.lang.CodeBlock.Index
 
size() - Method in class wyil.lang.CodeBlock
 
size() - Method in class wyil.lang.Type.Tuple
 
size() - Method in class wyil.lang.Type.UnionOfTuples
 
size(WyList) - Static method in class wyjc.runtime.WyList
 
size(WyTuple) - Static method in class wyjc.runtime.WyTuple
 
sizeof(Code) - Static method in class wyil.io.WyilFileReader
Return the "size" of this bytecode.
Skip(Attribute...) - Constructor for class wyc.lang.Stmt.Skip
 
Skip(Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Skip
 
skipWhitespace(List<WhileyFileLexer.Token>) - Method in class wyc.io.WhileyFileLexer
Skip over any whitespace at the current index position in the input string.
skipWhitespace(List<WyalFileLexer.Token>) - Method in class wycs.io.WyalFileLexer
Skip over any whitespace at the current index position in the input string.
skolemiseExistentials(Code) - Static method in class wycs.core.NormalForms
 
slots() - Method in class wyil.lang.CodeBlock
Determine the exact slots used in this block.
Smt2File - Class in wycs.solver.smt
Represents a SMT file.
Smt2File() - Constructor for class wycs.solver.smt.Smt2File
 
smtVerification - Variable in class wyc.util.WycBuildTask
Indicates whether or not the compiler should enable detailed verification checking of pre- and post-conditions using an external SMT solver.
SmtVerificationCheck - Class in wycs.transforms
A SMT verification checker.
SmtVerificationCheck(Builder) - Constructor for class wycs.transforms.SmtVerificationCheck
Creates a new SmtVerificationCheck with the given project builder.
SmtVerificationCheck.AssertionFailure - Exception in wycs.transforms
Represents a failure that occurred in an assertion, i.e., an assertion was found to be either "unsat" or "unknown".
SmtVerificationCheck.SolverFailure - Error in wycs.transforms
Represents a failure that occurred in the SMT solver.
Solver - Class in wycs.solver
 
Solver() - Constructor for class wycs.solver.Solver
 
Solver$native - Class in wycs.solver
Implements a lexiographic ordering of variable expressions.
Solver$native() - Constructor for class wycs.solver.Solver$native
 
SolverFailure(String) - Constructor for error wycs.transforms.SmtVerificationCheck.SolverFailure
Creates a new SolverFailure with the given error message.
SolverUtil - Class in wycs.solver
Provides a bunch of utility methods to simplify interfacing with the Solver directly.
SolverUtil() - Constructor for class wycs.solver.SolverUtil
 
Sort - Class in wycs.solver.smt
A sort is the term for a type in the SMT domain.
Sort.Any - Class in wycs.solver.smt
TODO: Documentation.
Sort.Array - Class in wycs.solver.smt
TODO: Documentation.
Sort.Bool - Class in wycs.solver.smt
TODO: Documentation.
Sort.Int - Class in wycs.solver.smt
TODO: Documentation.
Sort.Real - Class in wycs.solver.smt
TODO: Documentation.
Sort.Set - Class in wycs.solver.smt
TODO: Documentation.
Sort.Tuple - Class in wycs.solver.smt
TODO: Documentation.
Source(int, int, int) - Constructor for class wycc.lang.Attribute.Source
 
source - Variable in class wycs.syntax.Expr.IndirectInvoke
 
SourceFile - Class in wyil.attributes
Provides identifying information for a source file which contributed to the generation of a given WyIL file.
SourceFile(String) - Constructor for class wyil.attributes.SourceFile
 
sourceFile() - Method in class wyil.attributes.SourceFile
 
sourceFile() - Method in class wyil.attributes.SourceLocation
 
SourceLocation - Class in wyil.attributes
 
SourceLocation(int, int, int) - Constructor for class wyil.attributes.SourceLocation
 
SourceLocationMap - Class in wyil.attributes
The source location map is used to map individual bytecodes to their positions within their originating source file(s).
SourceLocationMap() - Constructor for class wyil.attributes.SourceLocationMap
 
sources - Variable in class wyc.lang.Expr.Quantifier
 
Spaces(String, int) - Constructor for class wycc.io.Token.Spaces
 
src - Variable in class wyc.lang.Expr.AbstractIndirectInvoke
 
src - Variable in class wyc.lang.Expr.Dereference
 
src - Variable in class wyc.lang.Expr.FieldAccess
 
src - Variable in class wyc.lang.Expr.IndexOf
 
src - Variable in class wyc.lang.Expr.LengthOf
 
srcFiles - Variable in class wycs.builders.Wyal2WycsBuilder
A map of the source files currently being compiled.
srcType - Variable in class wyc.lang.Expr.BinOp
 
srcType() - Method in class wyc.lang.Expr.BinOp
 
srcType - Variable in class wyc.lang.Expr.Dereference
 
srcType - Variable in class wyc.lang.Expr.FieldAccess
 
srcType - Variable in class wyc.lang.Expr.IndexOf
 
srcType - Variable in class wyc.lang.Expr.LengthOf
 
start - Variable in class wyc.io.WhileyFileLexer.Token
 
start - Variable in class wycc.io.Token
 
start - Variable in class wycc.lang.Attribute.Origin
 
start - Variable in class wycc.lang.Attribute.Source
 
start() - Method in exception wycc.lang.SyntaxError
Get index of first character of offending location.
start - Variable in class wycs.io.WyalFileLexer.Token
 
start() - Method in class wyil.attributes.SourceLocation
 
startOperand - Variable in class wyil.lang.Codes.Quantify
 
State(int) - Constructor for class wyautl_old.lang.Automaton.State
Construct a deterministic state with no children and no supplementary data.
State(int, int...) - Constructor for class wyautl_old.lang.Automaton.State
Construct a deterministic state with no supplementary data.
State(int, boolean, int...) - Constructor for class wyautl_old.lang.Automaton.State
Construct a state with no supplementary data.
State(int, Object, boolean, int...) - Constructor for class wyautl_old.lang.Automaton.State
Construct a state with children and supplementary data.
State(Automaton.State) - Constructor for class wyautl_old.lang.Automaton.State
 
state() - Method in class wyil.builders.VcBranch
Determine the current state of this branch.
State(boolean) - Constructor for class wyil.lang.Type.Record.State
 
State(boolean, Collection<String>) - Constructor for class wyil.lang.Type.Record.State
 
state() - Method in class wyjc.runtime.WyObject
 
statements - Variable in class wyc.lang.WhileyFile.FunctionOrMethod
 
states - Variable in class wyautl_old.lang.Automaton
 
StdBuildRule - Class in wybs.util
Provides a straightforward, yet flexible build rule implementation.
StdBuildRule(Builder, Path.Root, Content.Filter<?>, Content.Filter<?>, Path.Root) - Constructor for class wybs.util.StdBuildRule
Construct a standard build rule.
stderr - Variable in class wyc.WycMain
Stream to which error messages are written
stdout - Variable in class wyc.WycMain
Stream to which non-error messages are written
StdProject - Class in wybs.util
Provides a straightforward implementation of Build.Project and a basic build system supporting an arbitrary number of build rules.
StdProject(Collection<Path.Root>) - Constructor for class wybs.util.StdProject
 
StdProject(Collection<Path.Root>...) - Constructor for class wybs.util.StdProject
 
Stmt - Interface in wyc.lang
Provides classes for representing statements in Whiley's source language.
Stmt - Class in wycs.solver.smt
A statement in the SMT-LIB v2 language specification.
Stmt.Assert - Class in wyc.lang
Represents a assert statement of the form assert e, where e is a boolean expression.
Stmt.Assert - Class in wycs.solver.smt
An assertion statement.
Stmt.Assign - Class in wyc.lang
Represents an assignment statement of the form lhs = rhs.
Stmt.Assume - Class in wyc.lang
Represents an assume statement of the form assume e, where e is a boolean expression.
Stmt.Break - Class in wyc.lang
 
Stmt.Case - Class in wyc.lang
 
Stmt.CheckSat - Class in wycs.solver.smt
A check satisfiable statement.
Stmt.Continue - Class in wyc.lang
 
Stmt.Debug - Class in wyc.lang
 
Stmt.DeclareFun - Class in wycs.solver.smt
TODO: Documentation.
Stmt.DeclareSort - Class in wycs.solver.smt
TODO: Documentation.
Stmt.DefineFun - Class in wycs.solver.smt
TODO: Documentation.
Stmt.DefineSort - Class in wycs.solver.smt
TODO: Documentation.
Stmt.DoWhile - Class in wyc.lang
Represents a do-while statement whose body is made up from a block of statements separated by indentation.
Stmt.Exit - Class in wycs.solver.smt
TODO: Documentation.
Stmt.IfElse - Class in wyc.lang
Represents a classical if-else statement, which is has the form:
Stmt.Pop - Class in wycs.solver.smt
TODO: Documentation.
Stmt.Push - Class in wycs.solver.smt
TODO: Documentation.
Stmt.Return - Class in wyc.lang
Represents a return statement, which has the form:
Stmt.SetLogic - Class in wycs.solver.smt
TODO: Documentation.
Stmt.SetOption - Class in wycs.solver.smt
TODO: Documentation.
Stmt.Skip - Class in wyc.lang
 
Stmt.Switch - Class in wyc.lang
 
Stmt.VariableDeclaration - Class in wyc.lang
Represents a variable declaration which has the form:
Stmt.While - Class in wyc.lang
Represents a while statement, which has the form:
stmts - Variable in class wyc.lang.Stmt.Case
 
stores - Variable in class wyil.util.dfa.BackwardFlowAnalysis
The temporary abstract stores being generated during propagation.
stores - Variable in class wyil.util.dfa.ForwardFlowAnalysis
The temporary abstract stores being generated during propagation.
str2il(String) - Static method in class wyjc.runtime.Util
Coerce a string into a Whiley int list.
String(String, int) - Constructor for class wycc.io.Token.String
 
STRING - Static variable in class wycc.util.OptArg
 
String - Static variable in class wycs.core.SemanticType
 
String(String) - Static method in class wycs.core.Value
 
String(Automaton, String) - Static method in class wycs.solver.Solver
 
STRING - Static variable in class wyjc.runtime.WyType
 
StringRule() - Constructor for class wycc.io.AbstractLexer.StringRule
 
StringT - Static variable in class wycs.core.Types
 
StringT - Static variable in class wycs.solver.Solver
 
Strung(Attribute...) - Constructor for class wycs.syntax.SyntacticType.Strung
 
Strung(Collection<Attribute>) - Constructor for class wycs.syntax.SyntacticType.Strung
 
Sub(Automaton, int, int) - Static method in class wycs.solver.SolverUtil
Construct an automaton node representing the subtraction of two arithmetic expressions.
subpath(int, int) - Method in interface wyfs.lang.Path.ID
Get a sub ID from this id, which consists of those components between start and end (exclusive).
subpath(int, int) - Method in class wyfs.util.Trie
 
substitute(Map<Integer, Code>) - Method in class wycs.core.Code.Quantifier
 
substitute(Map<Integer, Code>) - Method in class wycs.core.Code
Substitute variables for bytecodes throughout this bytecode as determined by a given map.
substitute(Map<Integer, Code>) - Method in class wycs.core.Code.Variable
 
substitute(Map<String, SemanticType>) - Method in class wycs.core.SemanticType.Atom
 
substitute(Map<String, SemanticType>) - Method in class wycs.core.SemanticType
Substitute type variables for concrete types according to a given binding.
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.Binary
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.Cast
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.Constant
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.ConstantAccess
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.FieldAccess
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.IndexOf
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.IndirectInvoke
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.Invoke
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.Is
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.Nary
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.Quantifier
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.Record
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.Unary
 
substitute(Map<String, Expr>) - Method in class wycs.syntax.Expr.Variable
 
subtract(Value.Decimal) - Method in class wycs.core.Value.Decimal
 
subtract(Value.Integer) - Method in class wycs.core.Value.Integer
 
subtract(Constant.Decimal) - Method in class wyil.lang.Constant.Decimal
 
subtract(Constant.Integer) - Method in class wyil.lang.Constant.Integer
 
subtract(Constant.Rational) - Method in class wyil.lang.Constant.Rational
 
subtract(int) - Method in class wyjc.runtime.WyRat
 
subtract(long) - Method in class wyjc.runtime.WyRat
 
subtract(BigInteger) - Method in class wyjc.runtime.WyRat
 
subtract(WyRat) - Method in class wyjc.runtime.WyRat
 
SUBTYPE_ERROR - Static variable in class wyil.util.ErrorMessages
 
SubtypeOperator - Class in wyil.util.type
The subtype operator implements the algorithm for determining whether or not one type is a subtype of another.
SubtypeOperator(Automaton, Automaton) - Constructor for class wyil.util.type.SubtypeOperator
 
sUC_ELEMENTOF - Static variable in class wycc.io.Token
 
sUC_EMPTYSET - Static variable in class wycc.io.Token
 
sUC_EXISTS - Static variable in class wycc.io.Token
 
sUC_FORALL - Static variable in class wycc.io.Token
 
sUC_GREATEREQUALS - Static variable in class wycc.io.Token
 
sUC_LESSEQUALS - Static variable in class wycc.io.Token
 
sUC_LOGICALAND - Static variable in class wycc.io.Token
 
sUC_LOGICALOR - Static variable in class wycc.io.Token
 
sUC_SETINTERSECTION - Static variable in class wycc.io.Token
 
sUC_SETUNION - Static variable in class wycc.io.Token
 
sUC_SUBSET - Static variable in class wycc.io.Token
 
sUC_SUBSETEQ - Static variable in class wycc.io.Token
 
sUC_SUPSET - Static variable in class wycc.io.Token
 
sUC_SUPSETEQ - Static variable in class wycc.io.Token
 
SUCCESS - Static variable in class wyc.WycMain
 
SUCCESS - Static variable in class wycs.WycsMain
 
suffix(Content.Type<?>) - Method in class wyc.util.WycBuildTask.Registry
 
suffix(Content.Type<?>) - Method in class wycs.util.WycsBuildTask.Registry
 
suffix(Content.Type<?>) - Method in interface wyfs.lang.Content.Registry
Determine an appropriate suffix for a given content type.
suffix() - Method in interface wyfs.lang.Path.Entry
Return the suffix of the item in question.
suffix() - Method in class wyfs.util.DirectoryRoot.Entry
 
suffix() - Method in class wyfs.util.VirtualRoot.Entry
 
suffix(Content.Type<?>) - Method in class wyil.Main.Registry
 
suffix(Content.Type<?>) - Method in class wyjc.util.WyjcBuildTask.Registry
 
Sum(Automaton, int...) - Static method in class wycs.solver.Solver
 
Sum(Automaton, List<Integer>) - Static method in class wycs.solver.Solver
 
Switch(Expr, List<Stmt.Case>, Attribute...) - Constructor for class wyc.lang.Stmt.Switch
 
Switch(Expr, List<Stmt.Case>, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Switch
 
Switch(Type, int, String, Collection<Pair<Constant, String>>) - Static method in class wyil.lang.Codes
Construct a switch bytecode which pops a value off the stack, and switches to a given label based on it.
SyntacticElement - Interface in wycc.lang
A Syntactic Element represents any part of a source file which is relevant to the syntactic structure of the file, and in particular parts we may wish to add information too (e.g.
SyntacticElement.Impl - Class in wycc.lang
 
SyntacticType - Interface in wyc.lang
Provides classes for representing types in Whiley's source language.
SyntacticType - Interface in wycs.syntax
 
SyntacticType.Any - Class in wyc.lang
The type any represents the type whose variables may hold any possible value.
SyntacticType.Any - Class in wycs.syntax
The type any represents the type whose variables may hold any possible value.
SyntacticType.Array - Class in wyc.lang
Represents a list type, which is of the form:
SyntacticType.Bool - Class in wyc.lang
Represents the set of boolean values (i.e.
SyntacticType.Bool - Class in wycs.syntax
Represents the set of boolean values (i.e.
SyntacticType.Byte - Class in wyc.lang
Represents a sequence of 8 bits.
SyntacticType.Byte - Class in wycs.syntax
Represents a sequence of 8 bits.
SyntacticType.Char - Class in wycs.syntax
Represents a unicode character.
SyntacticType.Function - Class in wyc.lang
 
SyntacticType.Function - Class in wycs.syntax
 
SyntacticType.FunctionOrMethod - Class in wyc.lang
 
SyntacticType.Int - Class in wyc.lang
Represents the set of (unbound) integer values.
SyntacticType.Int - Class in wycs.syntax
Represents the set of (unbound) integer values.
SyntacticType.Intersection - Class in wyc.lang
Represents an intersection type, which is of the form:
SyntacticType.Intersection - Class in wycs.syntax
Represents an intersection type, which is of the form:
SyntacticType.List - Class in wycs.syntax
Represents a list type, which is of the form:
SyntacticType.Method - Class in wyc.lang
 
SyntacticType.Negation - Class in wyc.lang
Parse a negation type, which is of the form:
SyntacticType.Negation - Class in wycs.syntax
Parse a negation type, which is of the form:
SyntacticType.Nominal - Class in wyc.lang
Represents a nominal type, which is of the form:
SyntacticType.Nominal - Class in wycs.syntax
Parse a nominal type, which is of the form:
SyntacticType.NonUnion - Interface in wyc.lang
A non-union type represents a type which is not an instance of Union.
SyntacticType.Null - Class in wyc.lang
The null type is a special type which should be used to show the absence of something.
SyntacticType.Null - Class in wycs.syntax
The null type is a special type which should be used to show the absence of something.
SyntacticType.Primitive - Interface in wyc.lang
 
SyntacticType.Primitive - Class in wycs.syntax
 
SyntacticType.Real - Class in wyc.lang
The type real represents the set of (unbound) rational numbers.
SyntacticType.Real - Class in wycs.syntax
The type real represents the set of (unbound) rational numbers.
SyntacticType.Record - Class in wyc.lang
Represents record type, which is of the form:
SyntacticType.Record - Class in wycs.syntax
Represents record type, which is of the form:
SyntacticType.Reference - Class in wyc.lang
Parse a reference type, which is of the form:
SyntacticType.Reference - Class in wycs.syntax
Parse a reference type, which is of the form:
SyntacticType.Strung - Class in wycs.syntax
The type string represents a string of characters
SyntacticType.Tuple - Class in wyc.lang
Parse a tuple type, which is of the form:
SyntacticType.Tuple - Class in wycs.syntax
Parse a tuple type, which is of the form:
SyntacticType.Union - Class in wyc.lang
Represents a union type, which is of the form:
SyntacticType.Union - Class in wycs.syntax
Represents a union type, which is of the form:
SyntacticType.Util - Class in wycs.syntax
 
SyntacticType.Variable - Class in wycs.syntax
 
SyntacticType.Void - Class in wyc.lang
A void type represents the type whose variables cannot exist! That is, they cannot hold any possible value.
SyntacticType.Void - Class in wycs.syntax
A void type represents the type whose variables cannot exist! That is, they cannot hold any possible value.
SYNTAX_ERROR - Static variable in class wyc.WycMain
 
SYNTAX_ERROR - Static variable in class wycs.WycsMain
 
syntaxError(String, WhileyFile.Context, SyntacticElement) - Static method in class wyc.lang.WhileyFile
 
syntaxError(String, WhileyFile.Context, SyntacticElement, Throwable) - Static method in class wyc.lang.WhileyFile
 
SyntaxError - Exception in wycc.lang
This exception is thrown when a syntax error occurs in the parser.
SyntaxError(String, String, int, int, Attribute.Origin...) - Constructor for exception wycc.lang.SyntaxError
Identify a syntax error at a particular point in a file.
SyntaxError(String, String, int, int, Throwable, Attribute.Origin...) - Constructor for exception wycc.lang.SyntaxError
Identify a syntax error at a particular point in a file.
syntaxError(String, String, SyntacticElement) - Static method in exception wycc.lang.SyntaxError
 
syntaxError(String, String, SyntacticElement, Throwable) - Static method in exception wycc.lang.SyntaxError
 
syntaxError(String, String, Attribute...) - Static method in class wyil.util.ErrorMessages
Helper function for emitting a syntax error with appropriate source information.
syntaxError(String, String, Collection<Attribute>) - Static method in class wyil.util.ErrorMessages
Helper function for emitting a syntax error with appropriate source information.
syntaxError(String, String, Throwable, Attribute...) - Static method in class wyil.util.ErrorMessages
Helper function for emitting a syntax error with appropriate source information.
SyntaxError.InternalFailure - Exception in wycc.lang
An internal failure is a special form of syntax error which indicates something went wrong whilst processing some piece of syntax.
systemConsole(String[]) - Static method in class wyjc.runtime.Util
 

T

T_ANY - Static variable in class wyc.lang.Nominal
 
T_ANY - Static variable in class wyil.lang.Type
 
T_ARRAY_ANY - Static variable in class wyil.lang.Type
The type representing all possible list types.
T_BOOL - Static variable in class wyc.lang.Nominal
 
T_BOOL - Static variable in class wyil.lang.Type
 
T_BYTE - Static variable in class wyc.lang.Nominal
 
T_BYTE - Static variable in class wyil.lang.Type
 
T_INT - Static variable in class wyc.lang.Nominal
 
T_INT - Static variable in class wyil.lang.Type
 
T_LIST_ANY - Static variable in class wyc.lang.Nominal
 
T_META - Static variable in class wyc.lang.Nominal
 
T_META - Static variable in class wyil.lang.Type
 
T_NOTNULL - Static variable in class wyc.lang.Nominal
 
T_NULL - Static variable in class wyc.lang.Nominal
 
T_NULL - Static variable in class wyil.lang.Type
 
T_REAL - Static variable in class wyc.lang.Nominal
 
T_REAL - Static variable in class wyil.lang.Type
 
T_REF_ANY - Static variable in class wyil.lang.Type
 
T_VOID - Static variable in class wyc.lang.Nominal
 
T_VOID - Static variable in class wyil.lang.Type
 
Tabs(String, int) - Constructor for class wycc.io.Token.Tabs
 
target - Variable in class wycs.core.Code.Cast
 
target() - Method in class wyil.lang.Code.AbstractAssignable
Return the target register assigned by this bytecode.
target - Variable in class wyil.lang.Codes.Goto
 
target - Variable in class wyil.lang.Codes.If
 
target - Variable in class wyil.lang.Codes.IfIs
 
Template(Class<? extends Transform<T>>, Map<String, Object>) - Constructor for class wycc.lang.Pipeline.Template
 
Term(int, Object, DefaultInterpretation.Term...) - Constructor for class wyautl_old.lang.DefaultInterpretation.Term
 
test - Variable in class wycs.core.Code.Is
 
Tester - Class in wyautl_old.util
 
Tester() - Constructor for class wyautl_old.util.Tester
 
text - Variable in class wyc.io.WhileyFileLexer.Token
 
text - Variable in class wycc.io.Token
 
text - Variable in class wycs.io.WyalFileLexer.Token
 
TextAutomataWriter - Class in wyautl_old.io
Responsible for writing an automaton in a textual format to an output stream.
TextAutomataWriter(PrintStream) - Constructor for class wyautl_old.io.TextAutomataWriter
 
TextAutomataWriter(OutputStream) - Constructor for class wyautl_old.io.TextAutomataWriter
 
TextTypeWriter(PrintStream) - Constructor for class wyil.util.type.TypeGenerator.TextTypeWriter
 
third - Variable in class wycc.util.Triple
 
third() - Method in class wycc.util.Triple
 
throwsClause() - Method in class wyil.lang.Type.FunctionOrMethod
Get the throws clause of this function or method type.
throwType - Variable in class wyc.lang.SyntacticType.FunctionOrMethod
 
throwType - Variable in class wyc.lang.WhileyFile.FunctionOrMethod
 
throwType - Variable in class wycs.syntax.SyntacticType.Function
 
TIMEOUT(int) - Constructor for class wycs.transforms.VerificationCheck.RESULT.TIMEOUT
 
to() - Method in class wyautl_old.lang.DefaultSubsumption
 
to() - Method in interface wyautl_old.lang.Relation
Get the automaton in the "to" position.
to() - Method in class wycs.core.SemanticType.Function
 
to - Variable in class wycs.syntax.WyalFile.Function
 
to - Variable in class wyil.util.type.SubtypeOperator
 
toArray() - Method in class wyil.lang.CodeBlock.Index
 
toArray(BitSet) - Method in class wyil.transforms.LoopVariants
 
toIntArray(Collection<Integer>) - Static method in class wyil.lang.CodeUtils
 
Token(WhileyFileLexer.Token.Kind, String, int) - Constructor for class wyc.io.WhileyFileLexer.Token
 
Token - Class in wycc.io
An abstract notion representing a single token in the token stream produced by lexing a given input stream.
Token(String, int) - Constructor for class wycc.io.Token
 
Token(WyalFileLexer.Token.Kind, String, int) - Constructor for class wycs.io.WyalFileLexer.Token
 
Token.BlockComment - Class in wycc.io
A block comment represents a comment which potentially spans several lines of the source file.
Token.Char - Class in wycc.io
Represents a single character which begins and ends with single quotes.
Token.Comment - Class in wycc.io
A comment represents a section of the source file which should be effectively ignored (at least, from the perspective of semantics).
Token.Identifier - Class in wycc.io
An identifier is a token representing a sequence of (typically) alpha-numeric characters, which starts with an alphabetic character.
Token.Keyword - Class in wycc.io
A keyword is similar to an identifier which has been marked out as having special significance.
Token.LineComment - Class in wycc.io
A line comment represents a comment which spans to the end of the current line.
Token.NewLine - Class in wycc.io
Denotes a new line in the source file.
Token.Number - Class in wycc.io
A number which consists of an integer of unbounded size, followed by an (optional) second integer of unbounded size separated by a decimal point.
Token.Operator - Class in wycc.io
Represents an operator symbol, which may consist of 1 or more characters.
Token.Spaces - Class in wycc.io
Denotes a sequence of one or more space characters
Token.String - Class in wycc.io
Represents a string which begins and ends with double quotes.
Token.Tabs - Class in wycc.io
Denotes a sequence of one or more tab characters
Token.Whitespace - Class in wycc.io
Whitespace represents denotes the unused portions of the source file which lie between the significant tokens.
toNativeString() - Method in class wyfs.util.Trie
 
toString() - Method in class wyautl_old.lang.Automaton
 
toString() - Method in class wyautl_old.lang.DefaultInterpretation.Term
 
toString() - Method in class wyautl_old.util.BinaryMatrix
 
toString() - Method in class wyc.builder.CodeGenerator.Environment
 
toString() - Method in class wyc.lang.Expr.AbstractVariable
 
toString() - Method in class wyc.lang.Expr.BinOp
 
toString() - Method in class wyc.lang.Expr.Cast
 
toString() - Method in class wyc.lang.Expr.Constant
 
toString() - Method in class wyc.lang.Expr.ConstantAccess
 
toString() - Method in class wyc.lang.Expr.Dereference
 
toString() - Method in class wyc.lang.Expr.FieldAccess
 
toString() - Method in class wyc.lang.Expr.IndexOf
 
toString() - Method in class wyc.lang.Expr.LengthOf
 
toString() - Method in class wyc.lang.Expr.LocalVariable
 
toString() - Method in class wyc.lang.Expr.UnOp
 
toString() - Method in class wyc.lang.Nominal
 
toString() - Method in class wyc.lang.Stmt.Debug
 
toString() - Method in class wyc.lang.Stmt.Return
 
toString() - Method in class wycc.io.Token
 
toString() - Method in class wycc.lang.Attribute.Origin
 
toString() - Method in class wycc.lang.Attribute.Source
 
toString() - Method in class wycc.lang.NameID
 
toString() - Method in class wycc.util.Pair
 
toString() - Method in class wycc.util.Triple
 
toString() - Method in class wycs.core.Code
 
toString() - Method in class wycs.core.SemanticType
 
toString(int, int[]) - Method in class wycs.core.SemanticType
 
toString() - Method in class wycs.core.Value.Array
 
toString() - Method in class wycs.core.Value.Bool
 
toString() - Method in class wycs.core.Value.Decimal
 
toString() - Method in class wycs.core.Value.Integer
 
toString() - Method in class wycs.core.Value.Null
 
toString() - Method in class wycs.core.Value.String
 
toString() - Method in class wycs.core.Value.Tuple
 
toString() - Method in class wycs.solver.smt.Block
toString() - Method in class wycs.solver.smt.Smt2File
toString() - Method in class wycs.solver.smt.Sort.Any
toString() - Method in class wycs.solver.smt.Sort.Array
toString() - Method in class wycs.solver.smt.Sort.Bool
toString() - Method in class wycs.solver.smt.Sort.Int
toString() - Method in class wycs.solver.smt.Sort.Real
toString() - Method in class wycs.solver.smt.Sort.Set
Gets the name of this particular set sort, with it's type.
toString() - Method in class wycs.solver.smt.Sort.Tuple
Gets the name of this particular tuple sort, with it's types.
toString() - Method in class wycs.solver.smt.Stmt.Assert
toString() - Method in class wycs.solver.smt.Stmt.CheckSat
toString() - Method in class wycs.solver.smt.Stmt.DeclareFun
toString() - Method in class wycs.solver.smt.Stmt.DeclareSort
toString() - Method in class wycs.solver.smt.Stmt.DefineFun
toString() - Method in class wycs.solver.smt.Stmt.DefineSort
toString() - Method in class wycs.solver.smt.Stmt.Exit
toString() - Method in class wycs.solver.smt.Stmt.Pop
toString() - Method in class wycs.solver.smt.Stmt.Push
toString() - Method in class wycs.solver.smt.Stmt.SetLogic
toString() - Method in class wycs.solver.smt.Stmt.SetOption
toString() - Method in class wycs.solver.smt.Stmt
toString() - Method in class wycs.syntax.Expr.Binary
 
toString() - Method in class wycs.syntax.Expr.Cast
 
toString() - Method in class wycs.syntax.Expr.Constant
 
toString() - Method in class wycs.syntax.Expr.ConstantAccess
 
toString() - Method in class wycs.syntax.Expr.Exists
 
toString() - Method in class wycs.syntax.Expr.FieldAccess
 
toString() - Method in class wycs.syntax.Expr.ForAll
 
toString() - Method in class wycs.syntax.Expr.IndexOf
 
toString() - Method in class wycs.syntax.Expr.IndirectInvoke
 
toString() - Method in class wycs.syntax.Expr.Invoke
 
toString() - Method in class wycs.syntax.Expr.Is
 
toString() - Method in class wycs.syntax.Expr.Nary
 
toString() - Method in class wycs.syntax.Expr.Quantifier
 
toString() - Method in class wycs.syntax.Expr.Unary
 
toString() - Method in class wycs.syntax.Expr.Variable
 
toString() - Method in class wycs.syntax.SyntacticType.Any
 
toString() - Method in class wycs.syntax.SyntacticType.Bool
 
toString() - Method in class wycs.syntax.SyntacticType.Byte
 
toString() - Method in class wycs.syntax.SyntacticType.Char
 
toString() - Method in class wycs.syntax.SyntacticType.Int
 
toString() - Method in class wycs.syntax.SyntacticType.Intersection
 
toString() - Method in class wycs.syntax.SyntacticType.List
 
toString() - Method in class wycs.syntax.SyntacticType.Negation
 
toString() - Method in class wycs.syntax.SyntacticType.Nominal
 
toString() - Method in class wycs.syntax.SyntacticType.Null
 
toString() - Method in class wycs.syntax.SyntacticType.Real
 
toString() - Method in class wycs.syntax.SyntacticType.Record
 
toString() - Method in class wycs.syntax.SyntacticType.Reference
 
toString() - Method in class wycs.syntax.SyntacticType.Strung
 
toString() - Method in class wycs.syntax.SyntacticType.Tuple
 
toString() - Method in class wycs.syntax.SyntacticType.Union
 
toString() - Method in class wycs.syntax.SyntacticType.Variable
 
toString() - Method in class wycs.syntax.SyntacticType.Void
 
toString() - Method in class wycs.syntax.TypePattern.Leaf
 
toString() - Method in class wycs.syntax.TypePattern.Tuple
 
toString() - Method in class wyfs.util.DirectoryRoot.Entry
 
toString() - Method in class wyfs.util.DirectoryRoot.Folder
 
toString() - Method in class wyfs.util.DirectoryRoot
 
toString() - Method in class wyfs.util.JarFileRoot
 
toString() - Method in class wyfs.util.Trie
 
toString() - Method in class wyfs.util.VirtualRoot.Entry
 
toString() - Method in class wyfs.util.VirtualRoot.Folder
 
toString() - Method in class wyil.attributes.VariableDeclarations.Declaration
 
toString() - Method in class wyil.lang.CodeBlock.Index
 
toString() - Method in class wyil.lang.Codes.Assert
 
toString() - Method in class wyil.lang.Codes.Assign
 
toString() - Method in class wyil.lang.Codes.Assume
 
toString() - Method in class wyil.lang.Codes.BinaryOperator
 
toString() - Method in class wyil.lang.Codes.Const
 
toString() - Method in class wyil.lang.Codes.Convert
 
toString() - Method in class wyil.lang.Codes.Debug
 
toString() - Method in class wyil.lang.Codes.Dereference
 
toString() - Method in class wyil.lang.Codes.Fail
 
toString() - Method in class wyil.lang.Codes.FieldLoad
 
toString() - Method in class wyil.lang.Codes.Goto
 
toString() - Method in class wyil.lang.Codes.If
 
toString() - Method in class wyil.lang.Codes.IfIs
 
toString() - Method in class wyil.lang.Codes.IndexOf
 
toString() - Method in class wyil.lang.Codes.IndirectInvoke
 
toString() - Method in class wyil.lang.Codes.Invariant
 
toString() - Method in class wyil.lang.Codes.Invert
 
toString() - Method in class wyil.lang.Codes.Invoke
 
toString() - Method in class wyil.lang.Codes.Label
 
toString() - Method in class wyil.lang.Codes.Lambda
 
toString() - Method in class wyil.lang.Codes.LengthOf
 
toString() - Method in class wyil.lang.Codes.ListGenerator
 
toString() - Method in class wyil.lang.Codes.Loop
 
toString() - Method in class wyil.lang.Codes.Move
 
toString() - Method in class wyil.lang.Codes.NewList
 
toString() - Method in class wyil.lang.Codes.NewObject
 
toString() - Method in class wyil.lang.Codes.NewRecord
 
toString() - Method in class wyil.lang.Codes.NewTuple
 
toString() - Method in class wyil.lang.Codes.Nop
 
toString() - Method in class wyil.lang.Codes.Not
 
toString() - Method in class wyil.lang.Codes.Quantify
 
toString() - Method in class wyil.lang.Codes.Return
 
toString() - Method in class wyil.lang.Codes.Switch
 
toString() - Method in class wyil.lang.Codes.TupleLoad
 
toString() - Method in class wyil.lang.Codes.UnaryOperator
 
toString() - Method in class wyil.lang.Codes.Update
 
toString() - Method in class wyil.lang.Codes.Void
 
toString() - Method in class wyil.lang.Constant.Bool
 
toString() - Method in class wyil.lang.Constant.Byte
 
toString() - Method in class wyil.lang.Constant.Decimal
 
toString() - Method in class wyil.lang.Constant.Integer
 
toString() - Method in class wyil.lang.Constant.Lambda
 
toString() - Method in class wyil.lang.Constant.List
 
toString() - Method in class wyil.lang.Constant.Null
 
toString() - Method in class wyil.lang.Constant.Rational
 
toString() - Method in class wyil.lang.Constant.Record
 
toString() - Method in class wyil.lang.Constant.Tuple
 
toString() - Method in class wyil.lang.Constant.Type
 
toString() - Method in class wyil.lang.Modifier.Export
 
toString() - Method in class wyil.lang.Modifier.Native
 
toString() - Method in class wyil.lang.Modifier.Private
 
toString() - Method in class wyil.lang.Modifier.Public
 
toString() - Method in class wyil.lang.Type.Any
 
toString() - Method in class wyil.lang.Type.Bool
 
toString() - Method in class wyil.lang.Type.Byte
 
toString() - Method in class wyil.lang.Type.Compound
 
toString() - Method in class wyil.lang.Type.Int
 
toString() - Method in class wyil.lang.Type.Meta
 
toString() - Method in class wyil.lang.Type.Nominal
 
toString() - Method in class wyil.lang.Type.Null
 
toString() - Method in class wyil.lang.Type.Real
 
toString(Automaton) - Static method in class wyil.lang.Type
The following method constructs a string representation of the underlying automaton.
toString() - Method in class wyil.lang.Type.Void
 
toString() - Method in class wyjc.runtime.WyBool
 
toString() - Method in class wyjc.runtime.WyByte
 
toString() - Method in class wyjc.runtime.WyList
 
toString() - Method in class wyjc.runtime.WyRat
This method attempts to compute a string representation of the big rational which has at most 10 decimal places.
toString() - Method in class wyjc.runtime.WyRecord
 
toString() - Method in class wyjc.runtime.WyTuple
 
toSyntacticType() - Method in class wyc.lang.TypePattern.Intersection
 
toSyntacticType() - Method in class wyc.lang.TypePattern.Leaf
 
toSyntacticType() - Method