Overview  Package  Class   Use  Tree  Deprecated  Index  Help 
JML
 PREV   NEXT FRAMES    NO FRAMES    

Uses of Class
java.lang.String

Packages that use String
java.io JML Specifications for the corresponding types in the Java Developement Kit (JDK). 
java.lang JML Specifications for the corresponding types in the Java Developement Kit (JDK). 
java.lang.reflect JML Specifications for the corresponding types in the Java Developement Kit (JDK). 
java.math JML Specifications for the corresponding types in the Java Developement Kit (JDK). 
java.util JML Specifications for the corresponding types in the Java Developement Kit (JDK). 
java.util.regex JML Specifications for the corresponding types in the Java Developement Kit (JDK). 
org.jmlspecs.checker Contains the source code for a parser and typechecker for JML annotations and java code. 
org.jmlspecs.jmldoc The jmldoc tool documents java programs that contain JML (Java Modeling Language) annotations included as specially formatted comments; the generated html pages are very similar to those produced by javadoc, but with annotation information added. 
org.jmlspecs.jmldoc.jmldoc_142   
org.jmlspecs.jmlrac Generates Java classes from JML specifications that check assertions at runtime. 
org.jmlspecs.jmlrac.qexpr Translates JML quantified expressions into Java source code to evaluate them at runtime. 
org.jmlspecs.jmlrac.runtime Classes for use during runtime assertion checking for code compiled with JML's runtime assertion checking compiler (jmlc). 
org.jmlspecs.jmlspec A tool that can generate or compare specification skeletons from Java source or class files. 
org.jmlspecs.jmlunit Generates JUnit test classes from JML specifications. 
org.jmlspecs.jmlunit.strategies The types in this package are used in providing test data for JML/JUnit testing. 
org.jmlspecs.lang This package is a collection of types used in the definition of the JML language. 
org.jmlspecs.launcher The launcher allows the user to access all of the tools in JML. 
org.jmlspecs.models This package is a collection of types with immutable objects; it also enumerators (which have mutable objects) for the types of the immutable collections in the package. 
org.jmlspecs.models.resolve This package is a collection of types with immutable objects based on the RESOLVE specification language's mathematical models. 
org.jmlspecs.racwrap   
org.jmlspecs.racwrap.runner   
org.jmlspecs.samples.dbc This package contains samples of JML specifications written in the style of design by contract. 
org.jmlspecs.samples.digraph This package contains samples of JML specifications for directed graphs. 
org.jmlspecs.samples.dirobserver This package contains samples of JML specifications that illustrate issues in component-based programming relating to callbacks and JML's model program feature. 
org.jmlspecs.samples.jmlkluwer This package contains samples of JML specifications from the paper "JML: a Notation for Detailed Design". 
org.jmlspecs.samples.jmlrefman This package contains samples of JML specifications from the JML Reference Manual. 
org.jmlspecs.samples.jmltutorial This package contains samples of JML specifications from the tutorials. 
org.jmlspecs.samples.list This package contains samples of JML specifications that are related to lists of various flavors. 
org.jmlspecs.samples.list.list1   
org.jmlspecs.samples.list.list1.node   
org.jmlspecs.samples.list.list2   
org.jmlspecs.samples.list.list3   
org.jmlspecs.samples.list.node   
org.jmlspecs.samples.list.node2   
org.jmlspecs.samples.misc This package contains miscellaneous samples of JML specifications. 
org.jmlspecs.samples.prelimdesign This package contains samples of JML specifications from the paper Preliminary Design of JML. 
org.jmlspecs.samples.reader This package contains samples of JML specifications relating to some abstractions of input and output. 
org.jmlspecs.samples.sets This package contains samples of JML specifications relating to sets. 
org.jmlspecs.samples.stacks This package contains samples of JML specifications relating to stacks of various sorts. 
org.jmlspecs.samples.table This package contains samples of JML specifications relating to tables. 
org.jmlspecs.util   
org.jmlspecs.util.dis   
org.multijava.dis   
org.multijava.javadoc   
org.multijava.launcher The launcher allows the user to access all of the tools in MJ. 
org.multijava.mjc Implements mjc, a MultiJava compiler. 
org.multijava.mjdoc The mjdoc tool documents java programs that contain MultiJava (MJ) extensions to the Java progamming language; it produces html pages very similar to those produced by the javadoc tool. 
org.multijava.relaxed.rmjc   
org.multijava.relaxed.runtime   
org.multijava.relaxed.util   
org.multijava.util   
org.multijava.util.backend Provides an optimizer for methods for the compilers in MultiJava and the Java Modeling Language. 
org.multijava.util.classfile Provides an editor for classfiles used by MultiJava and the Java Modeling Language. 
org.multijava.util.compiler Provides utilities and superclasses for the compilers in MultiJava and the Java Modeling Language. 
org.multijava.util.guigen Implements the automatic generation of all of the GUIs for MultiJava and the Java Modeling Language. 
org.multijava.util.jperf Defines the perfect hashing function generator Package Specification JPerf is the perfect hashing function generator for the compilers in MultiJava and the Java Modeling Language. 
org.multijava.util.lexgen Provides a lexer for the compilers of MultiJava and the Java Modeling Language. 
org.multijava.util.msggen Implements the automatic generation of the data structure for all of the compiler messages in MultiJava and the Java Modeling Language. 
org.multijava.util.optgen Implements the automatic generation of the data structure for all of the command line options in MultiJava and the Java Modeling Language. 
org.multijava.util.optimize Provides an optimizer for classfiles used by MultiJava and the Java Modeling Language. 
org.multijava.util.testing Provides JUnit testing utilities for all of the parts of MultiJava and the Java Modeling Language. 
 

Uses of String in java.io
 

Fields in java.io declared as String
static String File.separator
           
private  String File.path
           
private static String File.tmpdir
           
static String File.pathSeparator
           
private  String PrintWriter.lineSeparator
           
 

Methods in java.io that return String
 String File.getAbsolutePath()
           
 String File.getCanonicalPath()
           
 String File.getName()
           
 String File.getParent()
           
 String File.getPath()
           
private static String File.getTempDir()
           
 String File.toString()
           
 String[] File.list()
           
 String[] File.list(FilenameFilter)
           
private static String File.slashify(String, boolean)
           
abstract  String DataInput.readLine()
           
abstract  String DataInput.readUTF()
           
 String BufferedReader.readLine()
           
(package private)  String BufferedReader.readLine(boolean)
           
 String OutputStreamWriter.getEncoding()
           
 String RandomAccessFile.readLine()
           
 String RandomAccessFile.readUTF()
           
 String ByteArrayOutputStream.toString()
           
 String ByteArrayOutputStream.toString(int)
           
 String ByteArrayOutputStream.toString(String)
           
 

Methods in java.io with parameters of type String
private static boolean File.checkAndCreate(String, SecurityManager)
           
private static String File.slashify(String, boolean)
           
static File File.createTempFile(String, String)
           
static File File.createTempFile(String, String, File)
           
private static File File.generateFile(String, String, File)
           
abstract  boolean FilenameFilter.accept(File, String)
           
 void Writer.write(String)
           
 void Writer.write(String, int, int)
           
 void PrintStream.print(String)
           
 void PrintStream.println(String)
           
private  void PrintStream.write(String)
           
 void PrintWriter.print(String)
           
 void PrintWriter.println(String)
           
 void PrintWriter.write(String)
           
 void PrintWriter.write(String, int, int)
           
 void OutputStreamWriter.write(String, int, int)
           
abstract  void DataOutput.writeBytes(String)
           
abstract  void DataOutput.writeChars(String)
           
abstract  void DataOutput.writeUTF(String)
           
 void RandomAccessFile.writeBytes(String)
           
 void RandomAccessFile.writeChars(String)
           
 void RandomAccessFile.writeUTF(String)
           
private  void RandomAccessFile.open(String, int)
           
 String ByteArrayOutputStream.toString(String)
           
 

Constructors in java.io with parameters of type String
File(String)
           
File(String, int)
           
File(File, String)
           
File(String, String)
           
IOException(String)
           
PrintStream(OutputStream, boolean, String)
           
OutputStreamWriter(OutputStream, String)
           
FileWriter(String)
           
FileWriter(String, boolean)
           
RandomAccessFile(File, String)
           
RandomAccessFile(String, String)
           
 

Uses of String in java.lang
 

Fields in java.lang declared as String
private  String Throwable.detailMessage
           
private static String[] ClassLoader.usr_paths
           
private static String[] ClassLoader.sys_paths
           
private  String Class.name
           
 

Methods in java.lang that return String
 String Object.toString()
           
 String String.intern()
           
 String String.toLowerCase()
           
 String String.toString()
           
 String String.toUpperCase()
           
 String String.trim()
           
static String String.valueOf(char)
           
 String String.replace(char, char)
           
static String String.valueOf(double)
           
static String String.valueOf(float)
           
 String String.substring(int)
           
static String String.valueOf(int)
           
 String String.substring(int, int)
           
static String String.valueOf(long)
           
static String String.valueOf(boolean)
           
static String String.copyValueOf(char[])
           
static String String.valueOf(char[])
           
static String String.copyValueOf(char[], int, int)
           
static String String.valueOf(char[], int, int)
           
static String String.valueOf(Object)
           
 String String.concat(String)
           
 String[] String.split(String)
           
 String[] String.split(String, int)
           
 String String.toLowerCase(Locale)
           
 String String.toUpperCase(Locale)
           
 String String.replaceAll(String, String)
           
 String String.replaceFirst(String, String)
           
abstract  String CharSequence.toString()
           
 String Throwable.getLocalizedMessage()
           
 String Throwable.getMessage()
           
 String Throwable.toString()
           
protected  String ClassLoader.findLibrary(String)
           
private static String[] ClassLoader.initializePath(String)
           
 String Class.getName()
           
private  String Class.getName0()
           
 String Class.toString()
           
private static String Class.argumentTypesToString(Class[])
           
private  String Class.resolveName(String)
           
 String Byte.toString()
           
static String Byte.toString(byte)
           
 String Character.toString()
           
static String Character.toString(char)
           
 String Double.toString()
           
static String Double.toString(double)
           
 String Float.toString()
           
static String Float.toString(float)
           
 String Integer.toString()
           
static String Integer.toBinaryString(int)
           
static String Integer.toHexString(int)
           
static String Integer.toOctalString(int)
           
static String Integer.toString(int)
           
static String Integer.toString(int, int)
           
private static String Integer.toUnsignedString(int, int)
           
 String Long.toString()
           
static String Long.toBinaryString(long)
           
static String Long.toHexString(long)
           
static String Long.toOctalString(long)
           
static String Long.toString(long)
           
static String Long.toString(long, int)
           
private static String Long.toUnsignedString(long, int)
           
 String Short.toString()
           
static String Short.toString(short)
           
 String StringBuffer.toString()
           
 String StringBuffer.substring(int)
           
 String StringBuffer.substring(int, int)
           
 

Methods in java.lang with parameters of type String
 boolean String.regionMatches(int, String, int, int)
           
 int String.compareTo(String)
           
 int String.compareToIgnoreCase(String)
           
 int String.indexOf(String)
           
 int String.lastIndexOf(String)
           
 boolean String.endsWith(String)
           
 boolean String.equalsIgnoreCase(String)
           
 boolean String.matches(String)
           
 boolean String.startsWith(String)
           
 byte[] String.getBytes(String)
           
 int String.indexOf(String, int)
           
 int String.lastIndexOf(String, int)
           
 boolean String.startsWith(String, int)
           
 boolean String.regionMatches(boolean, int, String, int, int)
           
 String String.concat(String)
           
 String[] String.split(String)
           
 String[] String.split(String, int)
           
 String String.replaceAll(String, String)
           
 String String.replaceFirst(String, String)
           
(package private)  boolean ClassLoader.desiredAssertionStatus(String)
           
 void ClassLoader.setClassAssertionStatus(String, boolean)
           
 void ClassLoader.setPackageAssertionStatus(String, boolean)
           
private  boolean ClassLoader.checkName(String, boolean)
           
 InputStream ClassLoader.getResourceAsStream(String)
           
static InputStream ClassLoader.getSystemResourceAsStream(String)
           
private  Class ClassLoader.findBootstrapClass(String)
           
private  Class ClassLoader.findBootstrapClass0(String)
           
protected  Class ClassLoader.findClass(String)
           
protected  Class ClassLoader.findLoadedClass(String)
           
private  Class ClassLoader.findLoadedClass0(String)
           
protected  Class ClassLoader.findSystemClass(String)
           
 Class ClassLoader.loadClass(String)
           
private  Class ClassLoader.loadClassInternal(String)
           
protected  Class ClassLoader.loadClass(String, boolean)
           
protected  Class ClassLoader.defineClass(String, byte[], int, int)
           
protected  Package ClassLoader.getPackage(String)
           
(package private) static void ClassLoader.loadLibrary(Class, String, boolean)
           
(package private) static long ClassLoader.findNative(ClassLoader, String)
           
protected  String ClassLoader.findLibrary(String)
           
private static String[] ClassLoader.initializePath(String)
           
protected  URL ClassLoader.findResource(String)
           
private static URL ClassLoader.getBootstrapResource(String)
           
 URL ClassLoader.getResource(String)
           
static URL ClassLoader.getSystemResource(String)
           
private  void ClassLoader.checkCerts(String, java.security.CodeSource)
           
protected  Enumeration ClassLoader.findResources(String)
           
private static Enumeration ClassLoader.getBootstrapResources(String)
           
 Enumeration ClassLoader.getResources(String)
           
static Enumeration ClassLoader.getSystemResources(String)
           
protected  Class ClassLoader.defineClass(String, byte[], int, int, java.security.ProtectionDomain)
           
private  Class ClassLoader.defineClass0(String, byte[], int, int, java.security.ProtectionDomain)
           
protected  Package ClassLoader.definePackage(String, String, String, String, String, String, String, URL)
           
 InputStream Class.getResourceAsStream(String)
           
static Class Class.forName(String)
           
(package private) static Class Class.getPrimitiveClass(String)
           
private  String Class.resolveName(String)
           
 Field Class.getDeclaredField(String)
           
 Field Class.getField(String)
           
private  Field Class.getField0(String)
           
 URL Class.getResource(String)
           
static Class Class.forName(String, boolean, ClassLoader)
           
private static Class Class.forName0(String, boolean, ClassLoader)
           
private  Field Class.searchFields(Field[], String)
           
 Method Class.getDeclaredMethod(String, Class[])
           
 Method Class.getMethod(String, Class[])
           
private  Method Class.getMethod0(String, Class[])
           
private static Method Class.searchMethods(Method[], String, Class[])
           
static byte Byte.parseByte(String)
           
static byte Byte.parseByte(String, int)
           
static Byte Byte.decode(String)
           
static Byte Byte.valueOf(String)
           
static Byte Byte.valueOf(String, int)
           
(package private) static NumberFormatException NumberFormatException.forInputString(String)
           
static double Double.parseDouble(String)
           
static Double Double.valueOf(String)
           
static float Float.parseFloat(String)
           
static Float Float.valueOf(String)
           
static int Integer.parseInt(String)
           
static int Integer.parseInt(String, int)
           
static Integer Integer.decode(String)
           
static Integer Integer.getInteger(String)
           
static Integer Integer.valueOf(String)
           
static Integer Integer.getInteger(String, int)
           
static Integer Integer.valueOf(String, int)
           
static Integer Integer.getInteger(String, Integer)
           
static long Long.parseLong(String)
           
static long Long.parseLong(String, int)
           
static Long Long.decode(String)
           
static Long Long.getLong(String)
           
static Long Long.valueOf(String)
           
static Long Long.valueOf(String, int)
           
static Long Long.getLong(String, long)
           
static Long Long.getLong(String, Long)
           
static short Short.parseShort(String)
           
static short Short.parseShort(String, int)
           
static Short Short.decode(String)
           
static Short Short.valueOf(String)
           
static Short Short.valueOf(String, int)
           
 int StringBuffer.indexOf(String)
           
 int StringBuffer.lastIndexOf(String)
           
 int StringBuffer.indexOf(String, int)
           
 int StringBuffer.lastIndexOf(String, int)
           
 StringBuffer StringBuffer.replace(int, int, String)
           
 StringBuffer StringBuffer.insert(int, String)
           
 StringBuffer StringBuffer.append(String)
           
 

Constructors in java.lang with parameters of type String
String(String)
           
String(byte[], int, int, String)
           
String(byte[], String)
           
Throwable(String)
           
Throwable(String, Throwable)
           
Exception(String)
           
Exception(String, Throwable)
           
RuntimeException(String)
           
RuntimeException(String, Throwable)
           
UnsupportedOperationException(String)
           
ClassNotFoundException(String)
           
ClassNotFoundException(String, Throwable)
           
ClassCastException(String)
           
Error(String)
           
Error(String, Throwable)
           
Byte(String)
           
IllegalArgumentException(String)
           
NumberFormatException(String)
           
Double(String)
           
IllegalStateException(String)
           
NullPointerException(String)
           
IndexOutOfBoundsException(String)
           
ArithmeticException(String)
           
Float(String)
           
Integer(String)
           
Long(String)
           
Short(String)
           
VirtualMachineError(String)
           
OutOfMemoryError(String)
           
StringBuffer(String)
           
NoSuchMethodException(String)
           
SecurityException(String)
           
InternalError(String)
           
CloneNotSupportedException(String)
           
IllegalAccessException(String)
           
 

Uses of String in java.lang.reflect
 

Fields in java.lang.reflect declared as String
private  String Method.name
           
private  String Field.name
           
 

Methods in java.lang.reflect that return String
 String Method.getName()
           
 String Method.toString()
           
abstract  String Member.getName()
           
 String Field.getName()
           
 String Field.toString()
           
(package private) static String Field.getTypeName(Class)
           
 

Constructors in java.lang.reflect with parameters of type String
Method(Class, String, Class[], Class, Class[], int, int)
           
Field(Class, String, Class, int, int)
           
InvocationTargetException(Throwable, String)
           
 

Uses of String in java.math
 

Fields in java.math declared as String
private static String[] BigInteger.zeros
           
 

Methods in java.math that return String
 String BigInteger.toString()
           
 String BigInteger.toString(int)
           
 

Constructors in java.math with parameters of type String
BigInteger(String)
           
BigInteger(String, int)
           
 

Uses of String in java.util
 

Fields in java.util declared as String
private static String Properties.strictKeyValueSeparators
           
private static String Properties.whiteSpaceChars
           
private static String Properties.keyValueSeparators
           
private static String Properties.specialSaveChars
           
 

Methods in java.util that return String
 String EventObject.toString()
           
 String AbstractCollection.toString()
           
 String Vector.toString()
           
 String AbstractMap.toString()
           
 String Hashtable.toString()
           
 String Properties.getProperty(String)
           
private  String Properties.loadConvert(String)
           
private  String Properties.saveConvert(String, boolean)
           
 String Properties.getProperty(String, String)
           
 String BitSet.toString()
           
 

Methods in java.util with parameters of type String
private  boolean Properties.continueLine(String)
           
private static void Properties.writeln(BufferedWriter, String)
           
 void Properties.save(OutputStream, String)
           
 void Properties.store(OutputStream, String)
           
 String Properties.getProperty(String)
           
private  String Properties.loadConvert(String)
           
private  String Properties.saveConvert(String, boolean)
           
 Object Properties.setProperty(String, String)
           
 String Properties.getProperty(String, String)
           
 

Constructors in java.util with parameters of type String
NoSuchElementException(String)
           
 

Uses of String in java.util.regex
 

Fields in java.util.regex declared as String
private  String Pattern.normalizedPattern
           
private static String[] Pattern.categoryNames
           
private static String[] Pattern.familyNames
           
private  String Pattern.pattern
           
 

Methods in java.util.regex that return String
 String Pattern.pattern()
           
 String[] Pattern.split(CharSequence)
           
 String[] Pattern.split(CharSequence, int)
           
private  String Pattern.composeOneStep(String)
           
private  String Pattern.produceEquivalentAlternation(String)
           
private  String[] Pattern.producePermutations(String)
           
 

Methods in java.util.regex with parameters of type String
private  void Pattern.accept(int, String)
           
static boolean Pattern.matches(String, CharSequence)
           
private  String Pattern.composeOneStep(String)
           
private  String Pattern.produceEquivalentAlternation(String)
           
private  String[] Pattern.producePermutations(String)
           
static Pattern Pattern.compile(String)
           
static Pattern Pattern.compile(String, int)
           
private  Pattern.Node Pattern.error(String)
           
private  Pattern.Node Pattern.retrieveCategoryNode(String)
           
private  Pattern.Node Pattern.retrieveFamilyNode(String)
           
private  Pattern.Node Pattern.familyError(String, String)
           
 

Constructors in java.util.regex with parameters of type String
Pattern(String, int)
           
 

Uses of String in org.jmlspecs.checker
 

Fields in org.jmlspecs.checker declared as String
static String JmlNode.MJCVISIT_MESSAGE
           
static String Constants.JML_JMLObjectSet
           
static String[] Constants.ACCESS_FLAG_NAMES
          These arrays are used to map flags to names for pretty printing and error messages and to issue style warnings for modifiers out of order.
static String Constants.TN_JMLOBJECTSET
          Used in typechecking set comprehension expressions.
static String Constants.TN_JMLVALUESET
          Used in typechecking set comprehension expressions.
static String Constants.TN_JMLTYPE
          Used in typechecking set comprehension expressions.
static String TestSuite.TEST_DESC
           
private  String JavadocJmlLexer.eol
           
static String[] JavadocJmlParser._tokenNames
           
private  String JmlLabeled.label
           
private  String JmlMethodDeclaration.thisStringRep
           
protected  String JmlMethodName.stringRepresentation
          Internally used
private  String JmlInformalExpression.text
          The text of this informal description.
private  String JmlInformalStoreRef.text
          The text of this informal description store reference.
private  String JmlLabelExpression.ident
           
private  String JmlMapsIntoClause.fieldId
           
private  String JmlMethodNameList.stringRepresentation
           
private  String JmlName.ident
           
private  String JmlName.name
           
private  String JmlOldExpression.label
           
private  String JmlRefinePrefix.fileName
           
private  String JmlRefinePrefix.packageName
           
private  String JmlSetComprehension.ident
           
private  String JmlSignalsClause.ident
           
private  String JmlStoreRefExpression.name
           
private  String JmlVariableDefinition.racField
          The name of RAC field generated for this variable.
private  String JmlCommonOptions.filter
           
private  String JmlCommonOptions.experiment
           
private  String JmlCommonOptions.universesx
           
private  String JmlCommonOptions.excludefiles
           
(package private) static String[] JmlFileFinder.suffixes
           
(package private) static String[] JmlFileFinder.suffixes1
           
(package private) static String JmlFileFinder.SYMBOL_SUFFIX
           
(package private)  String JmlGUI.JmlGUIFileFilter.suffix
           
private  String[] JmlGUI.JmlCompilation.files
           
static String[] JmlParser._tokenNames
           
(package private)  String JmlParser.StringBooleanPair.str
           
private static String[] Main.Filter.suffixes
           
private static String NonNullStatistics.currMethod
           
private static String NonNullStatistics.currClass
           
private static String[] NonNullStatistics.strArgs
           
 

Methods in org.jmlspecs.checker that return String
protected static String JmlNode.privacyString(long privacy)
          Return a string representation of the given visibility; the argument may be the complete set of modifiers; note that "package" is returned if no visibility level is specified.
protected  String Main.getWarningFilterNameFromOptions(MjcCommonOptions opts)
           
static String Main.makeRelative(String path, String referenceDir, String separator)
          This function should return a path for the first argument that is relative to the second argument (which may be a directory or a file); if the paths are the same, an empty string is returned.
 String TestSuite.TestSuite$1.toString()
           
 String JmlFormalParameter.modifiersAsString()
          Returns any parameter modifiers as a String; if the String is not empty, it will have a trailing space.
 String JmlConstraint.toString()
           
 String JmlRepresentsDecl.ident()
          Returns the identifier of the represented model field.
 String CTypeType.toString()
          Transforms this type to a string
 String JavadocJmlParser.description()
           
 String JmlLabeled.label()
           
 String JmlMemberDeclaration.stringRepresentation()
           
 String JmlMemberDeclaration.findJavaFileInRefinement()
           
 String JmlTypeDeclaration.ident()
          Returns the identifier for this type declaration.
 String JmlClassDeclaration.superName()
           
 String JmlClassOrGFImport.getName()
           
 String JmlClassOrGFImport.ident()
           
 String JmlCompilationUnit.packageNameAsString()
           
 String JmlCompilationUnit.getFilePath()
           
 String JmlCompilationUnit.fileNameIdent()
           
 String JmlMethodDeclaration.ident()
           
 String JmlMethodDeclaration.stringRepresentation()
           
 String JmlMethodName.toString()
           
 String JmlMethodName.getPrefixName()
          Returns a String representation of the prefix to the method, i.e., the receiver expression, used for creating error messages.
 String JmlConstructorName.toString()
           
 String JmlFieldDeclaration.ident()
          Returns the identifier of this field declaration
 String JmlInformalExpression.text()
          Returns the text of this informal description.
 String JmlInformalStoreRef.text()
           
 String JmlLabelExpression.ident()
           
 String JmlLoopStatement.label()
          Returns the label if this statement is a labeled loop statement; otherwise, returns null.
 String JmlMapsIntoClause.fieldIdent()
           
 String JmlMethodNameList.toString()
           
 String JmlMonitorsForVarAssertion.fieldIdent()
           
 String JmlName.ident()
           
 String JmlName.getName()
           
 String JmlOldExpression.label()
           
 String JmlPackageImport.getName()
          Returns the package name defined by this declaration.
 String JmlReadableIfVarAssertion.fieldIdent()
           
 String JmlWritableIfVarAssertion.fieldIdent()
           
 String JmlRefinePrefix.fileName()
           
 String JmlRelationalExpression.opString()
           
 String JmlRelationalExpression.toString()
           
 String JmlSetComprehension.ident()
           
 String JmlSignalsClause.ident()
           
 String JmlStoreRefExpression.getName()
           
 String JmlStoreRefExpression.toString()
           
 String JmlVariableDefinition.racField()
          Returns the name of RAC field generated for this variable.
 String JmlAssignableFieldSet.toString()
           
 String JmlSourceMethod.getGenericSignature()
           
 String JmlDataGroupMemberMap.toString()
           
 String JmlBinaryMember.ident()
           
 String JmlBinaryMember.stringRepresentation()
           
 String JmlBinaryMethod.stringRepresentation()
           
 String JmlVersionOptions.getShortOptions()
           
 String JmlVersionOptions.version()
           
 String JmlCommonOptions.filter()
           
 String JmlCommonOptions.set_filter(String filter)
           
 String JmlCommonOptions.experiment()
           
 String JmlCommonOptions.set_experiment(String experiment)
           
 String JmlCommonOptions.universesx()
           
 String JmlCommonOptions.set_universesx(String universesx)
           
 String JmlCommonOptions.excludefiles()
           
 String JmlCommonOptions.set_excludefiles(String excludefiles)
           
 String JmlCommonOptions.getShortOptions()
           
protected  String JmlGUI.getClasspath(Options opt)
           
protected  String JmlGUI.getSourcepath(Options opt)
           
protected  String JmlGUI.getWebpageName()
           
protected  String JmlGUI.getWebpageLocation()
           
 String JmlGUI.AllFilesGUIFileFilter.getDescription()
           
 String JmlGUI.JmlGUIFileFilter.getDescription()
           
 String JmlOptions.getShortOptions()
           
 String JmlNumericType.toString()
          Transforms this type to a string
 String JmlNumericType.getSignature()
          Transforms this type to a string
 String JmlParser.jIdentifier()
           
protected  String JmlTypeLoader.getFileIdent(File f)
          Returns the Java identifier associated with the name of the file contained in this file.
 

Methods in org.jmlspecs.checker with parameters of type String
protected  CField JmlSourceClass.lookupFieldHelper(String name, CExpressionContextType context)
          Searches a field in current class and parent hierarchy as needed
protected  CField JmlSourceClass.getDeclaredField(String ident)
          Returns the signature of the field with the given name declared in this class, or null if this class does not declare a field with the given name.
protected  boolean JmlSourceClass.isFieldRedefined(String ident, CExpressionContextType dummyContext)
          Returns true iff a field with same name is already defined in a superclass or an implemented interface.
protected  void JmlSourceClass.accumMostSpecificMethods(String name, CClass.NoDupStrategy actor, CMethodSet accum, CClassType[] args, CContextType context)
          Accumulates the set of methods with identifier name declared in the type represented by this, or added to the type by external methods, using the strategy actor.
static int JmlSourceClass.computeSuffixNumber(String fileName)
          Computes the number associated with the suffix of the given file name.
protected  void JmlSourceClass.accumLocalInternalMethods(String name, CClass.NoDupStrategy actor, CMethodSet accum, CClassType[] args)
          Accumulates the set of methods with identifier name declared in the type represented by this, using the strategy actor.
 CMethodSet JmlSourceClass.lookupJMLMethodName(String name, CContextType context)
          For looking up methods that are not overloaded and appear in JML clauses that list method calls.
protected  CClass JmlSourceClass.getDeclaredInnerType(String name)
          Searches for the inner type with the given name.
private  void JmlSourceClass.accumMethodsJMLOnly(CClass.NoDupStrategy actor, String name, CMethodSet accum)
          Accumulates the set of methods with identifier name declared in the type represented by this, ignoring external methods, using the strategy actor.
protected  ClassInfo JmlSourceClass.createClassInfo(long modifiers, String superClass, File sourceFile)
          Creates an instance of ClassInfo.
static void Main.main(String[] args)
          The entry point when starting this program from the command line.
static boolean Main.compile(String[] args)
          Second entry point.
static boolean Main.compile(String[] args, JmlOptions opt, OutputStream os)
          Entry point for the GUI
 boolean Main.parseArguments(String[] args, ArrayList infiles)
          Parses the argument list.
static String Main.makeRelative(String path, String referenceDir, String separator)
          This function should return a path for the first argument that is relative to the second argument (which may be a directory or a file); if the paths are the same, an empty string is returned.
protected  void JmlAbstractVisitor.visitBinaryExpression(JBinaryExpression self, String oper)
          Visits the given binary expression with the given operator.
 boolean AndNotPatternFilenameFilter.accept(File dir, String name)
          Return true just when we want to process this file name.
protected  CSourceClass JClassDeclarationWrapper.makeSignature(Main compiler, CClass owner, CMemberHost host, String prefix, boolean isAnon, boolean isMember)
          Generates the signature object for this class declaration.
protected  CSourceMethod JConstructorDeclarationWrapper.makeMethodSignature(CContextType context, MemberAccess access, String ident, CSpecializedType[] parameterTypes)
          Generates the signature object for this method declaration.
protected  CSourceClass JInterfaceDeclarationWrapper.makeSignature(Main compiler, CClass owner, CMemberHost host, String prefix, boolean isAnon, boolean isMember)
          Generates the signature object for this.
protected  CSourceMethod JMethodDeclarationWrapper.makeMethodSignature(CContextType context, MemberAccess access, String ident, CSpecializedType[] parameterTypes)
          Generates the signature object for this method declaration.
 void JmlTypeDeclaration.generateInterface(Main compiler, CClass owner, CMemberHost host, String prefix, boolean isAnon, boolean isMember)
          Generates a CSourceClass class signature singleton for this declaration.
 void JmlTypeDeclaration.setIdent(String ident)
           
private  JmlTypeDeclaration JmlTypeDeclaration.checkRedundantRepresents(JmlRepresentsDecl redundantRep, String ident)
           
private  void JmlTypeDeclaration.checkFieldsInterface(String javaFileName)
           
private  void JmlTypeDeclaration.checkMethodsInterface(String javaFileName)
           
static JmlClassDeclaration JmlClassDeclaration.makeInstance(TokenReference where, long modifiers, String ident, CClassType superType, boolean isWeakSubtype, CClassType[] interfaces, boolean[] interfaceWeaklyFlags, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JavadocComment javadoc, JavaStyleComment[] comment, boolean isRefinedType)
          Constructs a class declaration in the parsing tree.
 boolean JmlCompilationUnit.declaresType(String qualifiedName)
          Returns true iff this compilation unit contains a declaration for a top-level type with the given fully qualified name.
 boolean JmlCompilationUnit.declaresGF(String qualifiedName)
          Returns true iff this compilation unit contains a declaration for a generic function with the given fully qualified name.
static JmlMethodDeclaration JmlMethodDeclaration.makeInstance(TokenReference where, long modifiers, CType returnType, String ident, JFormalParameter[] parameters, CClassType[] exceptions, JBlock body, JavadocComment javadoc, JavaStyleComment[] comments, JmlMethodSpecification methodSpecification)
           
 void JmlMethodDeclaration.setIdent(String name)
          Set the name of this method; used by RAC.
 CSourceMethod JmlMethodDeclaration.checkInterfaceType(CContextType context, MemberAccess access, String ident)
          Performs the interface checks that are common to all sorts of methods.
static JmlConstructorDeclaration JmlConstructorDeclaration.makeInstance(TokenReference where, long modifiers, String ident, JFormalParameter[] params, CClassType[] exceptions, JConstructorBlock body, JavadocComment javadoc, JavaStyleComment[] comments, JmlMethodSpecification methodSpecification)
           
 JmlSourceField JmlDataGroupClause.checkDataGroup(CFlowControlContextType context, JExpression groupNameExpr, String ident, long privacy)
           
static JmlInformalExpression JmlInformalExpression.ofBoolean(TokenReference where, String text)
          Returns a new informal description of type boolean.
static JmlInformalExpression JmlInformalExpression.ofInteger(TokenReference where, String text)
          Returns a new informal description of type int.
static JmlInterfaceDeclaration JmlInterfaceDeclaration.makeInstance(TokenReference where, long modifiers, String ident, CClassType[] interfaces, boolean[] interfaceWeaklyFlags, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JavadocComment javadoc, JavaStyleComment[] comment, boolean isRefinedType)
          Constructs an interface declaration in the parsing tree.
 void JmlPackageImport.setClassUsed(String clazz)
          States that specified class in imported package is used.
 void JmlRefinePrefix.setPackageName(String packageName)
           
static JmlBinaryType JmlRefinePrefix.buildBinaryType(TokenReference where, String prefix)
           
 void JmlVariableDefinition.setRacField(String name)
          Set the name of RAC field of this variable to the given one.
protected  void JmlVisitorNI.imp(String method, Object self)
           
protected  void JmlAccumSubclassingInfo.visitBinaryExpression(JBinaryExpression self, String oper)
           
 boolean JmlSourceMethod.isApplicable(String ident, CType recvType, CType[] actuals, CClassType[] args)
          Returns true if this method is applicable to a method call with the given identifier and actual (static) argument types.
protected  MethodInfo JmlSourceMethod.createCMethodInfo(int modifiers, String name, String type, String[] exceptions, CSourceMethod method, boolean deprecated, boolean synthetic)
          Creates a method info object.
protected  MethodInfo JmlSourceMethod.createMethodInfo(int modifiers, String name, String type, String[] exceptions, CodeInfo code, boolean deprecated, boolean synthetic)
          Creates a method info object.
 CClass JmlContext.lookupClass(String name)
          Searches for a class with the given simple name according the procedure in JLS2 6.5.5.
 CTypeVariable JmlContext.lookupTypeVariable(String ident)
           
 CMethod JmlContext.lookupMethod(String name, CType[] params)
          Searches for the most specific method in the current context that is applicable to the given identifier and argument type tuple.
 CMethod JmlContext.lookupMethod(String name, CType[] params, CClassContextType context)
          Searches for the most specific method in the current context that is applicable to the given identifier and argument type tuple.
 CMethodSet JmlContext.lookupMethodOrSet(String name, CType[] params)
          Searches for the most specific method(s) in the current context that is applicable to the given identifier and argument type tuple.
 CMethodSet JmlContext.lookupMethodOrSet(String name, CType[] params, CClassContextType context)
          Searches for the most specific method(s) in the current context that is applicable to the given identifier and argument type tuple.
 CFieldAccessor JmlContext.lookupField(String ident)
          searches for a field with the given identifier
 CFieldAccessor JmlContext.lookupField(String ident, CExpressionContextType context)
          searches for a field with the given identifier
 JLocalVariable JmlContext.lookupLocalVariable(String ident)
          searches for a local variable with the given identifier
 JExpression JmlContext.lookupOuterLocalVariable(TokenReference ref, String ident)
          Finds a local variable with the given name that appears outside the current lexical contour.
 CFieldAccessor JmlContext.lookupOuterField(String ident)
          Searches for a field of the given name in the context surrounding the current lexical contour.
 CFieldAccessor JmlContext.lookupOuterField(String ident, CExpressionContextType context)
          Searches for a field of the given name in the context surrounding the current lexical contour.
 void JmlContext.resolveMaybeExtMethodRef(String ident)
          Searches for any imported external generic functions.
 void JmlContext.registerGFDecl(String methodIdent, CGenericFunctionCollection coll)
          Registers the declaration of an external generic function in this context.
 CFieldAccessor JmlExpressionContext.lookupField(String ident)
          searches for a field with the given identifier
 CFieldAccessor JmlExpressionContext.lookupOuterField(String ident)
          Searches for a field of the given name in the context surrounding the current lexical contour.
protected  CClassType[] JmlBinarySourceClass.loadInterfaces(String[] interfaces)
          Loads the interfaces specified by the Strings in the argument array (whether from other declarations in this compilation pass or from *.class files.)
private static CClass JmlBinarySourceClass.getOuterClassFrom(String clazz)
          Returns the surrounding class for the inner class named by the argument.
private static CMemberHost JmlBinarySourceClass.getHostFrom(String clazz)
          Returns the host for the class named by the argument.
 CClass JmlClassContext.lookupClass(String name)
          Searches for a class with the given simple name according the procedure in JLS2 6.5.5.
 CMethod JmlClassContext.lookupMethod(String ident, CType[] params, CClassContextType context)
          Searches for the most specific method when no receiver is explicit at the call site.
 CMethodSet JmlClassContext.lookupMethodOrSet(String ident, CType[] params, CClassContextType context)
          Searches for the most specific method(s) when no receiver is explicit at the call site.
 CFieldAccessor JmlClassContext.lookupOuterField(String ident, CExpressionContextType context)
          Searches for a field of the given name in the context surrounding the current lexical contour.
 CFieldAccessor JmlClassContext.lookupField(String ident, CExpressionContextType context)
          lookupField
 JExpression JmlClassContext.lookupOuterLocalVariable(TokenReference ref, String ident)
          Finds a local variable with the given name that appears outside the current lexical contour.
 JLocalVariable JmlClassContext.lookupLocalVariable(String ident)
          lookupLocalVariable
 void JmlClassContext.resolveMaybeExtMethodRef(String ident)
          Searches for any imported or private external generic functions.
 boolean JmlVersionOptions.setOption(String name, Object newValue)
           
 String JmlCommonOptions.set_filter(String filter)
           
 String JmlCommonOptions.set_experiment(String experiment)
           
 String JmlCommonOptions.set_universesx(String universesx)
           
 String JmlCommonOptions.set_excludefiles(String excludefiles)
           
 boolean JmlCommonOptions.setOption(String name, Object newValue)
           
 CClass JmlCompilationUnitContext.lookupClass(String name)
          Searches for a class with the given simple name according the procedure in JLS2 6.5.5.
 CMethod JmlCompilationUnitContext.lookupMethod(String name, CType[] params, CClassContextType context)
          Searches for the most specific method applicable to the given identifier and argument type tuple, in the current context.
 CMethodSet JmlCompilationUnitContext.lookupMethodOrSet(String name, CType[] params, CClassContextType context)
          Searches for the most specific method(s) applicable to the given identifier and argument type tuple, in the current context.
 CFieldAccessor JmlCompilationUnitContext.lookupField(String ident, CExpressionContextType context)
          searches for a field with the given identifier
 JLocalVariable JmlCompilationUnitContext.lookupLocalVariable(String ident)
          Finds the variable with the given identifier in this context.
 JExpression JmlCompilationUnitContext.lookupOuterLocalVariable(TokenReference ref, String ident)
          Finds a local variable with the given name that appears outside the current lexical contour.
 CFieldAccessor JmlCompilationUnitContext.lookupOuterField(String ident, CExpressionContextType context)
          Searches for a field of the given name in the context surrounding the current lexical contour.
 void JmlCompilationUnitContext.resolveMaybeExtMethodRef(String ident)
          Searches for any imported external generic functions.
static Main.PTMode Main.PTMode.mode(String s)
           
 JmlMapsIntoClause[] JmlDataGroupAccumulator.getMapsIntoClausesFor(String fieldId)
           
protected  FieldInfo JmlSourceField.createFieldInfo(int modifiers, String name, String type, Object value, boolean deprecated, boolean synthetic)
          Creates a new field info object.
 ClassPath.ClassDescription JmlFileFinder.find(String name)
          This method finds a file for the given class name; it first looks for a source file anywhere in the source path; if there is none, then a class file is sought on the class path.
 ClassPath.ClassDescription JmlFileFinder.findSourceFile(String name)
          Finds a source file per the implemented search order, which is to search for all the suffixes in each directory on the source path in turn.
private  ClassPath.ClassDescription JmlFileFinder.findSymbolFile(String name)
          Returns the symbol file for the given class name.
 JLabeledStatement JmlFlowControlContext.getLabeledStatement(String label)
          Returns the statement with the specified label.
 CClass JmlFlowControlContext.lookupClass(String name)
          Searches for a class with the given simple name according the procedure in JLS2 6.5.5.
 JLocalVariable JmlFlowControlContext.lookupLocalVariable(String ident)
          Returns the variable referred to by the given name in this context, recursing to surrounding contexts as appropriate.
static void JmlGUI.main(String[] args)
           
static JmlGUI JmlGUI.init(String[] args, boolean standAlone)
           
protected  boolean JmlGUI.dirInClassPath(Options opt, String dir)
           
protected  GUI.Compilation JmlGUI.createCompilationInstance(String[] files, Options opt, OutputStream os)
           
 boolean JmlGUI.AllFilesGUIFileFilter.hasActiveSuffix(String name)
           
 boolean JmlGUI.JmlGUIFileFilter.hasActiveSuffix(String name)
           
 boolean JmlOptions.setOption(String name, Object newValue)
           
(package private)  void JmlParser.TypeWeaklyList.add(String name, boolean _weakly)
           model_program { weaklyFlags.add( new Boolean( _weakly ) ); } also assignable weaklyFlags;
 boolean JmlSigBinaryMethod.isApplicable(String ident, CType recvType, CType[] actuals)
          Returns true if this method is applicable to a method call with the given identifier and actual (static) argument types.
 JmlCompilationUnit JmlTypeLoader.getSuspendedCUnit(String qName)
          Look for partially processed compilation unit (if suspended) for the qualified type name qName.
 void JmlTypeLoader.activateSymbolTableBuild(String qName)
          Reactivate the task for the qualified type name qName.
 void JmlTypeLoader.activateTypeCheck(String qName)
          Reactivate the task for the qualified type name qName.
protected  boolean JmlTypeLoader.isTrusted(String qName)
          Returns true if the information for the type or package of the given qualified name should be retained for subsequent compilation sessions.
protected  ClassInfo JmlTypeLoader.createClassInfo(String qName)
          Creates and returns a class info object by reading the symbol file for the class with the given fully qualified name qName.
 boolean Main.Filter.accept(File dir, String name)
           
static void NonNullStatistics.checkExpression(JExpression j, JmlContext context, String fn, int clause, boolean ifNot, boolean ifInvStatic)
           
static void NonNullStatistics.checkSpecification(JmlMethodDeclaration jmd, Object[] jscArr, JmlContext context, String fn)
           
static void NonNullStatistics.checkSpecCase(JmlSpecCase jsc, JmlContext context, String fn, boolean fromHeavy)
           
static void NonNullStatistics.checkSpecBody(JmlSpecBody jsb, JmlContext context, String fn)
           
static void NonNullStatistics.checkSpecBodyClause(JmlSpecBodyClause jsbc, JmlContext context, String fn)
           
private static void NonNullStatistics.handleNNElementExpr(JmlNonNullElementsExpression j, JmlContext context, String fn, int clause, boolean ifInvStatic)
           
private static void NonNullStatistics.handleInstanceofExpression(JInstanceofExpression j, JmlContext context, String fn, int clause, boolean ifInvStatic)
           
private static void NonNullStatistics.handleEqualityExpression(JmlEqualityExpression je, JmlContext context, String fn, int clause, boolean ifNot, boolean ifInvStatic)
           
private static void NonNullStatistics.handleFreshExpression(JmlFreshExpression jf, JmlContext context, int clause, String fn)
           
static void NonNullStatistics.handleMethodDeclaration(JmlMethodDeclaration jmd, JMethodDeclaration delegee, String fileName, JmlContext context)
           
static void NonNullStatistics.setCurrMethod(String methodIdent)
           
static void NonNullStatistics.setCurrClass(String classIdent)
           
static Vector NonNullStatistics.getSuperSpec(JmlMethodDeclaration jmd, String key)
           
private static void NonNullStatistics.putHmSpecCase(String key)
           
private static void NonNullStatistics.abortCurrentSpecCase(String fn)
           
private  JmlMethodSpecification TestJmlParser.methodSpecificationFrom(String mspec)
           
private  JmlModelProgStatement TestJmlParser.getModelProgStatement(String sourceCode)
           
private  JmlGuardedStatement TestJmlParser.getGuardedStatementFrom(String sourceCode)
           
private  JmlGeneralSpecCase TestJmlParser.getSpecCase(String sourceCode)
           
protected  void TestJmlParser.Helper.establishTest(String sourceCode, boolean parseJavadocs)
          Establish lexers and parsers for the given source code, parsing javadoc comments according to the given boolean.
protected  JmlCompilationUnit TestJmlParser.Helper.getJmlAST(String sourceCode)
           
protected  JmlMethodSpecification TestJmlParser.Helper.getMethodSpecification(String sourceCode)
           
protected  JmlGenericSpecCase TestJmlParser.Helper.getGenericSpecCase(String sourceCode)
           
protected  JmlGenericSpecCase TestJmlParser.Helper.getGenericSpecStatementCase(String sourceCode)
           
protected  JmlAbruptSpecCase TestJmlParser.Helper.getAbruptSpecCase(String sourceCode)
           
protected  JmlSpecBodyClause[] TestJmlParser.Helper.getSpecBody(String sourceCode)
           
protected  JmlRequiresClause TestJmlParser.Helper.getRequiresClause(String sourceCode)
           
protected  JmlSpecBodyClause TestJmlParser.Helper.getSpecBodyClause(String sourceCode)
           
protected  JmlModelProgram TestJmlParser.Helper.getModelProgram(long modifiers, String sourceCode)
           
protected  JmlSpecVarDecl[] TestJmlParser.Helper.getSpecVarDecls(String sourceCode)
           
protected  JStatement TestJmlParser.Helper.getStatement(String sourceCode)
           
 

Constructors in org.jmlspecs.checker with parameters of type String
JmlSourceClass(Main compiler, CClass owner, CMemberHost host, TokenReference where, long modifiers, String ident, String qualifiedName, boolean isAnonymous, boolean isMember, boolean deprecated)
          Constructs a class export from source
TestSuite(String name)
           
JmlFormalParameter(TokenReference where, int desc, CSpecializedType type, String ident, boolean isFinal, boolean isNonNull, boolean isNull)
          Constructs a formal parameter node in the parsing tree.
AndNotPatternFilenameFilter(FilenameFilter f, String p)
          Initialize this filter.
JClassDeclarationWrapper(TokenReference where, long modifiers, String ident, CClassType superType, CClassType[] interfaces, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JavadocComment javadoc, JavaStyleComment[] comments)
          Constructs a class declaration in the parsing tree.
JClassDeclarationWrapper(TokenReference where, long modifiers, String ident, CClassType superType, CClassType[] interfaces, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JavadocComment javadoc, JavaStyleComment[] comments, boolean isRefinedType)
          Constructs a class declaration in the parsing tree.
JConstructorDeclarationWrapper(TokenReference where, long modifiers, String ident, JFormalParameter[] parameters, CClassType[] exceptions, JConstructorBlock body, JavadocComment javadoc, JavaStyleComment[] comments)
          Construct a node in the parsing tree This method is directly called by the parser
JInterfaceDeclarationWrapper(TokenReference where, long modifiers, String ident, CClassType[] interfaces, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JavadocComment javadoc, JavaStyleComment[] comments, boolean isRefinedType)
          Constructs an interface declaration in the parsing tree.
JMethodDeclarationWrapper(TokenReference where, long modifiers, CType returnType, String ident, JFormalParameter[] parameters, CClassType[] exceptions, JBlock body, JavadocComment javadoc, JavaStyleComment[] comments)
          Construct a node in the parsing tree This method is directly called by the parser
JmlLabeled(TokenReference where, boolean isRedundantly, String label, JmlPredicate predOrNot, boolean isNotSpecified)
           
JmlBreaksClause(TokenReference where, boolean isRedundantly, String label, JmlPredicate predOrNot, boolean isNotSpecified)
           
JmlClassOrGFImport(TokenReference where, String name, JavaStyleComment[] comments, boolean isModel)
          Constructs an AST node for a class or external member import statement.
JmlContinuesClause(TokenReference where, boolean isRedundantly, String label, JmlPredicate predOrNot, boolean isNotSpecified)
           
JmlInformalExpression(TokenReference where, String text)
          Constructs an instance.
JmlInformalExpression(TokenReference where, String text, boolean isBoolean)
          Constructs an instance.
JmlInformalStoreRef(TokenReference where, String text)
           
JmlLabelExpression(TokenReference where, boolean isPosLabel, String ident, JmlSpecExpression specExpression)
           
JmlMapsIntoClause(TokenReference where, boolean redundantly, String fieldId, JmlStoreRefExpression memberRef, JmlStoreRefExpression[] groupList)
           
JmlName(TokenReference where, String ident)
          Construct an ident sort of name or name-suffix.
JmlOldExpression(TokenReference where, JmlSpecExpression specExpression, String label)
           
JmlPackageImport(TokenReference where, String name, JavaStyleComment[] comments, boolean isModel)
           
JmlRefinePrefix(TokenReference where, String fileName)
           
JmlSetComprehension(TokenReference where, CType type, CType memberType, String ident, JExpression supersetPred, JmlPredicate predicate)
           
JmlSignalsClause(TokenReference where, boolean isRedundantly, CType type, String ident, JmlPredicate pred, boolean notSpecified)
           
JmlVariableDefinition(TokenReference where, long modifiers, CType type, String ident, JExpression initializer)
          Construct a node in the parsing tree.
JmlSourceMethod(MemberAccess access, String ident, CType returnType, CSpecializedType[] paramTypes, CClassType[] exceptions, boolean deprecated, JBlock body, CContextType declarationContext, JMethodDeclaration declarationASTNode)
           
JmlBinaryType(TokenReference where, JmlBinarySourceClass member, String prefix)
          Constructs a class export from file.
JmlVersionOptions(String name)
           
JmlCommonOptions(String name)
           
JmlSourceField(JmlMemberAccess access, String ident, CType type, boolean deprecated)
          Constructs a field export
JmlGUI.JmlGUIFileFilter(String suffix)
           
JmlGUI.JmlCompilation(String[] files, JmlOptions options, OutputStream os)
           
JmlOptions(String name)
           
JmlOrdinalLiteral(TokenReference where, String image)
          Construct a node in the parsing tree
JmlParser.StringBooleanPair(String str, boolean bool)
           
TestJmlParser(String name)
          The constructor called by the JUnit framework.
TestJmlParser.Helper(String name)
           
 

Uses of String in org.jmlspecs.jmldoc
 

Fields in org.jmlspecs.jmldoc declared as String
private  String JavadocOptions.bootclasspath
           
private  String JavadocOptions.bottom
           
private  String JavadocOptions.charset
           
private  String JavadocOptions.docencoding
           
private  String JavadocOptions.doclet
           
private  String JavadocOptions.docletpath
           
private  String JavadocOptions.doctitle
           
private  String JavadocOptions.encoding
           
private  String JavadocOptions.exclude
           
private  String JavadocOptions.excludedocfilessubdir
           
private  String JavadocOptions.extdirs
           
private  String JavadocOptions.footer
           
private  String[][] JavadocOptions.group
           
private  String JavadocOptions.header
           
private  String JavadocOptions.helpfile
           
private  String JavadocOptions.J
           
private  String[][] JavadocOptions.link
           
private  String[][] JavadocOptions.linkoffline
           
private  String JavadocOptions.locale
           
private  String JavadocOptions.noqualifier
           
private  String JavadocOptions.overview
           
private  String JavadocOptions.stylesheetfile
           
private  String JavadocOptions.subpackages
           
private  String[][] JavadocOptions.tag
           
private  String JavadocOptions.taglet
           
private  String JavadocOptions.tagletpath
           
private  String JavadocOptions.windowtitle
           
private  String JmldocOptions.docpath
           
private  String JmldocOptions.fcns
           
 

Methods in org.jmlspecs.jmldoc that return String
 String JavadocOptions.bootclasspath()
           
 String JavadocOptions.set_bootclasspath(String bootclasspath)
           
 String JavadocOptions.bottom()
           
 String JavadocOptions.set_bottom(String bottom)
           
 String JavadocOptions.charset()
           
 String JavadocOptions.set_charset(String charset)
           
 String JavadocOptions.docencoding()
           
 String JavadocOptions.set_docencoding(String docencoding)
           
 String JavadocOptions.doclet()
           
 String JavadocOptions.set_doclet(String doclet)
           
 String JavadocOptions.docletpath()
           
 String JavadocOptions.set_docletpath(String docletpath)
           
 String JavadocOptions.doctitle()
           
 String JavadocOptions.set_doctitle(String doctitle)
           
 String JavadocOptions.encoding()
           
 String JavadocOptions.set_encoding(String encoding)
           
 String JavadocOptions.exclude()
           
 String JavadocOptions.set_exclude(String exclude)
           
 String JavadocOptions.excludedocfilessubdir()
           
 String JavadocOptions.set_excludedocfilessubdir(String excludedocfilessubdir)
           
 String JavadocOptions.extdirs()
           
 String JavadocOptions.set_extdirs(String extdirs)
           
 String JavadocOptions.footer()
           
 String JavadocOptions.set_footer(String footer)
           
 String[][] JavadocOptions.group()
           
 String[][] JavadocOptions.set_group(String[][] group)
           
 String JavadocOptions.header()
           
 String JavadocOptions.set_header(String header)
           
 String JavadocOptions.helpfile()
           
 String JavadocOptions.set_helpfile(String helpfile)
           
 String JavadocOptions.J()
           
 String JavadocOptions.set_J(String J)
           
 String[][] JavadocOptions.link()
           
 String[][] JavadocOptions.set_link(String[][] link)
           
 String[][] JavadocOptions.linkoffline()
           
 String[][] JavadocOptions.set_linkoffline(String[][] linkoffline)
           
 String JavadocOptions.locale()
           
 String JavadocOptions.set_locale(String locale)
           
 String JavadocOptions.noqualifier()
           
 String JavadocOptions.set_noqualifier(String noqualifier)
           
 String JavadocOptions.overview()
           
 String JavadocOptions.set_overview(String overview)
           
 String JavadocOptions.stylesheetfile()
           
 String JavadocOptions.set_stylesheetfile(String stylesheetfile)
           
 String JavadocOptions.subpackages()
           
 String JavadocOptions.set_subpackages(String subpackages)
           
 String[][] JavadocOptions.tag()
           
 String[][] JavadocOptions.set_tag(String[][] tag)
           
 String JavadocOptions.taglet()
           
 String JavadocOptions.set_taglet(String taglet)
           
 String JavadocOptions.tagletpath()
           
 String JavadocOptions.set_tagletpath(String tagletpath)
           
 String JavadocOptions.windowtitle()
           
 String JavadocOptions.set_windowtitle(String windowtitle)
           
 String JavadocOptions.getShortOptions()
           
 String JmldocOptions.docpath()
           
 String JmldocOptions.set_docpath(String docpath)
           
 String JmldocOptions.fcns()
           
 String JmldocOptions.set_fcns(String fcns)
           
 String JmldocOptions.getShortOptions()
           
static String Utils.modifierString(com.sun.tools.doclets.standard.AbstractSubWriter w, long m)
           
 

Methods in org.jmlspecs.jmldoc with parameters of type String
 String JavadocOptions.set_bootclasspath(String bootclasspath)
           
 String JavadocOptions.set_bottom(String bottom)
           
 String JavadocOptions.set_charset(String charset)
           
 String JavadocOptions.set_docencoding(String docencoding)
           
 String JavadocOptions.set_doclet(String doclet)
           
 String JavadocOptions.set_docletpath(String docletpath)
           
 String JavadocOptions.set_doctitle(String doctitle)
           
 String JavadocOptions.set_encoding(String encoding)
           
 String JavadocOptions.set_exclude(String exclude)
           
 String JavadocOptions.set_excludedocfilessubdir(String excludedocfilessubdir)
           
 String JavadocOptions.set_extdirs(String extdirs)
           
 String JavadocOptions.set_footer(String footer)
           
 String[][] JavadocOptions.set_group(String[][] group)
           
 String JavadocOptions.set_header(String header)
           
 String JavadocOptions.set_helpfile(String helpfile)
           
 String JavadocOptions.set_J(String J)
           
 String[][] JavadocOptions.set_link(String[][] link)
           
 String[][] JavadocOptions.set_linkoffline(String[][] linkoffline)
           
 String JavadocOptions.set_locale(String locale)
           
 String JavadocOptions.set_noqualifier(String noqualifier)
           
 String JavadocOptions.set_overview(String overview)
           
 String JavadocOptions.set_stylesheetfile(String stylesheetfile)
           
 String JavadocOptions.set_subpackages(String subpackages)
           
 String[][] JavadocOptions.set_tag(String[][] tag)
           
 String JavadocOptions.set_taglet(String taglet)
           
 String JavadocOptions.set_tagletpath(String tagletpath)
           
 String JavadocOptions.set_windowtitle(String windowtitle)
           
 boolean JavadocOptions.setOption(String name, Object newValue)
           
static void JmldocGUI.main(String[] args)
           
static void JmldocGUI.init(String[] args, boolean standAlone)
           
 String JmldocOptions.set_docpath(String docpath)
           
 String JmldocOptions.set_fcns(String fcns)
           
 boolean JmldocOptions.setOption(String name, Object newValue)
           
static void Main.main(String[] args)
           
static boolean Main.compile(String[] args)
           
 

Constructors in org.jmlspecs.jmldoc with parameters of type String
JavadocOptions(String name)
           
JmldocOptions(String name)
           
 

Uses of String in org.jmlspecs.jmldoc.jmldoc_142
 

Fields in org.jmlspecs.jmldoc.jmldoc_142 declared as String
private static String JmlHTML.eol
          The string that terminates lines on this platform.
private static String JmlHTML.jmlbegin
          Used to begin any section of material added to an HTML file.
private static String JmlHTML.jmlend
          Used to end any section of material added to an HTML file.
private static String JmlHTML.jmlcomment1
           
private static String JmlHTML.jmlcomment2
           
private static String JmlHTML.oldsuffix
          This string is used as a suffix for the backup files - the original html files before begin altered by adding jml annotations.
private static String JmlHTML.newsuffix
          This string is used as a suffix for the new html file, temporarily; Once the file is complete it is moved on top of the old one.
private static String JmlHTML.adjustedDestination
          This gives the absolute path of the destination for generated html files.
private static String JmlHTML.suffix
          The value of the suffix that javadoc uses on this platform for html files, with the leading period.
private static String JmlHTML.alternateSuffix
          A second suffix for html files that should be tried.
protected  String JmlHTML.currentFilePath
           
private  String JmlHTML.classSpecsTitle
           
(package private)  String JmldocGUI.JmldocGUIFileFilter.suffix
           
private  String[] JmldocGUI.JmldocCompilation.files
           
private static String SpecWriter.eol
          The string that terminates lines on this platform.
static String SpecWriter.BREOL
           
 String JmlHTML.IntString.text
          The text to be inserted at the given position.
 

Methods in org.jmlspecs.jmldoc.jmldoc_142 that return String
 String JmldocFieldSubWriter.getLink(CClass container, CField fd, String label)
           
protected  String JmlHTML.generateClassSpecification(JmlTypeDeclaration jmltype, com.sun.tools.doclets.standard.HtmlStandardWriter writer)
          This generates the full html insert for the class level specifications, including those for any super classes and including the leading jmlbegin and jmlend strings.
(package private) static String JmlHTML.makeSig(JmlMethodDeclaration m, JmlTypeDeclaration jmltype)
          This function returns a String giving the signature of a method - the method name and fully qualified argument types, but not formal parameter names.
 String JmlHTML.generateFieldSpecification(JFieldDeclarationType jm, JmldocFieldSubWriter fsw)
           
 String JmlHTML.generateMethodSpecification(JmlMethodDeclaration jm, CClass cclass, String sig, com.sun.tools.doclets.standard.HtmlStandardWriter writer)
           
 String JmlHTML.linkString(CClass cclass, boolean fullname, com.sun.tools.doclets.standard.HtmlStandardWriter writer)
          This function generates a String giving the name of the class corresponding to 'cclass'; if an html file can be located for this class, then the string consists of an HTML link reference to that class.
protected  String JmldocGUI.getClasspath(Options opt)
           
protected  String JmldocGUI.getSourcepath(Options opt)
           
protected  String JmldocGUI.getWebpageName()
           
protected  String JmldocGUI.getWebpageLocation()
           
 String JmldocGUI.AllFilesGUIFileFilter.getDescription()
           
 String JmldocGUI.JmldocGUIFileFilter.getDescription()
           
 String JmldocStandard.name()
           
 String SpecWriter.toString()
          Returns the accumulated text.
 String SpecWriter.htmlop(int op, JRelationalExpression s)
           
static String SpecWriter.jmlModifiers(long mods)
           
 String SpecWriter.convertToHtml(String s)
          Copies the input string to the output, replacing instances of special html characters by html representations (less than symbols, greater than symbols, ampersands).
private  String SpecWriter.replace(String s, char c, String rep)
           
 

Methods in org.jmlspecs.jmldoc.jmldoc_142 with parameters of type String
static void Main.main(String[] args)
          The entry point when starting this program from the command line.
static boolean Main.compile(String[] args)
          Second entry point.
 boolean Main.runParser(String[] args, MjcCommonOptions opt, ArrayList infiles)
          Runs the argument parser only so the GUI can process options from the command line
static boolean Main.compile(String[] args, JmldocOptions opt, OutputStream os)
          Entry point for the GUI
 boolean Main.parseArguments(String[] args, ArrayList infiles)
          Parses the argument list.
protected  void Main.addRecursivePackages(String packageName, File dir, ArrayList dirs)
          This adds all subdirectories (recursively) as packages to be processed.
 String JmldocFieldSubWriter.getLink(CClass container, CField fd, String label)
           
(package private)  void JmlHTML.jmlize(JTypeDeclarationType jtype, String packageRoot)
          This method generates the html file for the class represented by 'jtype'.
protected  boolean JmlHTML.checkFile(String dp, boolean useD, String cp, String suf)
          This function checks whether a html file exists with a name constructed from the given class name (cp), and the given settings of the destination directory (dp), useDollar (useD) and suffix to use (suf).
protected  boolean JmlHTML.findFile(String cpath, String packageRoot)
          This function finds an html file for the given class name (cpath) and directory containing the package root (packageRoot).
 void JmlHTML.findSections(String fileString, String begin, String end, ArrayList extracts)
          This function finds all occurrences of text in 'fileString' bracketed by the given begin and end Strings.
 void JmlHTML.findSections(String fileString, String begin, ArrayList extracts)
          This function finds all occurrences of the string begin in 'fileString' .
protected  void JmlHTML.classSpecs(JmlTypeDeclaration jmltype, StringBuffer sb, boolean inherited, String title)
          This method generates the html describing the specifications of class/interface jmltype.
 void JmlHTML.printClassSpecsHeader(StringBuffer classspec, boolean inherited, String title)
           
 void JmlHTML.printClassSpecsHeaderInherited(StringBuffer classspec, String title)
           
protected  void JmlHTML.insertMethodSpecs(JmlTypeDeclaration jmltype, String fileString, ArrayList insertions)
          This method generates the html text for the specifications of the methods for type jmlType, with reference to the original file content in fileString.
protected  void JmlHTML.insertFieldSpecs(JmlTypeDeclaration jmltype, String fileString, ArrayList insertions)
          This method generates the html text for the specifications of the fields for type jmlType, with reference to the original file content in fileString.
protected  void JmlHTML.insertMethodSpecs(JmlMethodDeclaration jm, String fileString, ArrayList insertions, String sig, JmlTypeDeclaration jmltype)
          This method generates the specification text for the method jm with signature string sig belonging to class jmltype, and with reference to the original html file in fileString.
 String JmlHTML.generateMethodSpecification(JmlMethodDeclaration jm, CClass cclass, String sig, com.sun.tools.doclets.standard.HtmlStandardWriter writer)
           
protected  boolean JmlHTML.superSpecification(StringBuffer s, CClass sclass, JmlMethodDeclaration jm, String sig, boolean isclass, com.sun.tools.doclets.standard.HtmlStandardWriter writer)
          Generates the html for any specifications for the method 'jm' in the super class 'sclass'.
static void JmldocGUI.main(String[] args)
           
static JmldocGUI JmldocGUI.init(String[] args, boolean standAlone)
           
protected  boolean JmldocGUI.dirInClassPath(Options opt, String dir)
           
protected  GUI.Compilation JmldocGUI.createCompilationInstance(String[] files, Options opt, OutputStream os)
           
 boolean JmldocGUI.AllFilesGUIFileFilter.hasActiveSuffix(String name)
           
 boolean JmldocGUI.JmldocGUIFileFilter.hasActiveSuffix(String name)
           
 void SpecWriter.append(String s)
          Appends the given string to the SpecWriter's buffer.
 void SpecWriter.visitJmlBehaviorSpecHelper(JmlHeavyweightSpec self, String s)
           
 void SpecWriter.visitJmlExampleHelper(JmlExample self, String title)
           
 String SpecWriter.convertToHtml(String s)
          Copies the input string to the output, replacing instances of special html characters by html representations (less than symbols, greater than symbols, ampersands).
private  String SpecWriter.replace(String s, char c, String rep)
           
 

Constructors in org.jmlspecs.jmldoc.jmldoc_142 with parameters of type String
JmldocClassWriter(com.sun.tools.doclets.standard.ConfigurationStandard configuration, String path, String filename, com.sun.javadoc.ClassDoc classdoc, com.sun.javadoc.ClassDoc prev, com.sun.javadoc.ClassDoc next, com.sun.tools.doclets.ClassTree classtree, boolean nopackage)
           
JmldocGUI.JmldocGUIFileFilter(String suffix)
           
JmldocGUI.JmldocCompilation(String[] files, JmldocOptions options, OutputStream os)
           
JmlHTML.IntString(int offset, String text)
          A constructor, taking an integer position and the text to be inserted at that position.
 

Uses of String in org.jmlspecs.jmlrac
 

Fields in org.jmlspecs.jmlrac declared as String
private static String[] TransUtils.nonReflectiveTypes
          An array of type names to which non-reflective calls would be made for specification inheritance.
private static String[] TransUtils.nonReflectiveRefinementTypes
          An array of type names to which non-reflective calls would be made for specification inheritance.
static String RacConstants.TN_SURROGATE
          The name of the surrogate class for an interface.
static String RacConstants.TN_JMLSURROGATE
          The name of the interface that all surrogate classes have to implement.
static String RacConstants.TN_JMLCHECKABLE
          The type name of a private delegee field (VN_DELEGEE) of the surrogate class (TN_SURROGATE) for an interface.
static String RacConstants.TN_JMLVALUE
          The name of a special wrapper class that can encapsulate two special values in addition to Java regular values: undefined and non-executable.
static String RacConstants.TN_JMLUNIT_TEST_POSTFIX
          The name of test class generated by jmlunit.
static String RacConstants.TN_JMLUNIT_TESTDATA_POSTFIX
          The name of test case class generated by jmlunit.
static String RacConstants.MN_CHECK_PRE
          The method name prefix for methods that check method preconditions, often called precondition check methods.
static String RacConstants.MN_CHECK_POST
          The method name prefix for methods that check normal postconditions, often called normal postcondition check methods.
static String RacConstants.MN_CHECK_XPOST
          The method name prefix for methods that check exceptional postconditions, often called exceptional postcondition check methods.
static String RacConstants.MN_EVAL_OLD
          The method name prefix for methods that evaluate, in the pre-state, old expressions appearing in history constraints, for use in the post-state by constraint check methods.
static String RacConstants.MN_CHECK_INV
          The method name prefix for methods that check invariants.
static String RacConstants.MN_CHECK_HC
          The method name prefix for methods that check history constraints.
static String RacConstants.MN_INTERNAL
          The method name prefix for renaming original methods into private internal methods.
static String RacConstants.MN_MODEL
          The method name prefix for access methods generated for model fields.
static String RacConstants.MN_SPEC
          The method name prefix for spec_public and spec_protected access methods generated for spec_public and spec_protected fields.
static String RacConstants.MN_GHOST
          The variable and method name prefix for the private field and a pair of access methods generated for a ghost variable.
static String RacConstants.MN_SPEC_PUBLIC
          The method name prefix of access methods generated for spec_public and spec_protected methods.
static String RacConstants.MN_MODEL_PUBLIC
          The method name prefix of access methods generated for model methods.
static String RacConstants.MN_SAVE_TO
          The method name prefix for the method that saves pre-state values into the private stack field (VN_STACK_VAR) for possible recursive method calls.
static String RacConstants.MN_RESTORE_FROM
          The method name prefix for the method that restores pre-state values from the private stack field (VN_STACK_VAR) for possible recursive method calls.
static String RacConstants.MN_INIT
          The name of the internal method and the assertion check methods for the constructors.
static String RacConstants.VN_ERROR_SET
          The name of a set variable that holds information about all the assertion violations detected so far by the runtime assertion checker.
static String RacConstants.VN_PRECOND
           
static String RacConstants.VN_RESULT
          The name of a varialbe that holds the return value of the method being assertion checked.
static String RacConstants.VN_XRESULT
          The name of a variable that holds the exceptional result of the method being assertion checked.
static String RacConstants.VN_FREE_VAR
          The name of local variables to be generated to evaluate varisous JML predicates and expressions.
static String RacConstants.VN_CATCH_VAR
          The name of variables to generate for use in catch clauses.
static String RacConstants.VN_OLD_VAR
          The name of a private field generated to store the pre-state value of an old expression in postcoditions and history constraints and an old variable appearing in a method specification.
static String RacConstants.VN_PRE_VAR
          The name of a private field generated to store the result of precondition evaluation, for reference by the postcondition check methods.
static String RacConstants.VN_POST_VAR
          The name of a local variable generated to store the result of evaluating a specification case of a postcondition
static String RacConstants.VN_ASSERTION
           
static String RacConstants.VN_EXCEPTION
          Name of the exception parameter.
static String RacConstants.VN_STACK_VAR
          Name of the stack variable.
static String RacConstants.VN_INIT
          Name of a non-static boolean field that indicates whether a class instance, during its construction, has finished its initialization.
static String RacConstants.VN_CLASS_INIT
          Name of a static boolean field that indicates whether the initialization of a class or an inteface has been completed.
static String RacConstants.VN_DELEGEE
          Name of a private delegee field of a surrogate class (TN_SURROGATE) for an interface.
static String RacConstants.VN_RAC_LEVEL
          Name of the static field generated by the runtime assertion checker to indicate the per-class runtime assertion check level.
static String RacConstants.VN_RAC_COMPILED
          Name of the static final field generated by the runtime assertion checker to indicate that a type is compiled with the runtime asssertion check code.
static