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.awt.event   
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.awt.event
 

Fields in java.awt.event declared as String
(package private)  String ActionEvent.actionCommand
           
 

Methods in java.awt.event that return String
 String ComponentEvent.paramString()
           
 String WindowEvent.paramString()
           
 String ActionEvent.getActionCommand()
           
 String ActionEvent.paramString()
           
 String ItemEvent.paramString()
           
 

Constructors in java.awt.event with parameters of type String
ActionEvent(Object, int, String)
           
ActionEvent(Object, int, String, int)
           
ActionEvent(Object, int, String, long, int)
           
 

Uses of String in java.io
 

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

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

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

Constructors in java.io with parameters of type String
File(String, int)
           
File(String, File)
           
File(String)
           
File(String, String)
           
File(File, String)
           
IOException(String)
           
IOException(String, Throwable)
           
PrintStream(OutputStream, boolean, String)
           
PrintStream(String)
           
PrintStream(String, String)
           
PrintStream(File, String)
           
PrintWriter(String)
           
PrintWriter(String, String)
           
PrintWriter(File, String)
           
OutputStreamWriter(OutputStream, String)
           
FileWriter(String)
           
FileWriter(String, boolean)
           
RandomAccessFile(String, String)
           
RandomAccessFile(File, 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.substring(int)
           
 String String.substring(int, int)
           
 String String.concat(String)
           
 String String.replace(char, char)
           
 String String.replaceFirst(String, String)
           
 String String.replaceAll(String, String)
           
 String String.replace(CharSequence, CharSequence)
           
 String[] String.split(String, int)
           
 String[] String.split(String)
           
 String String.toLowerCase(Locale)
           
 String String.toLowerCase()
           
 String String.toUpperCase(Locale)
           
 String String.toUpperCase()
           
 String String.trim()
           
 String String.toString()
           
static String String.format(String, Object[])
           
static String String.format(Locale, String, Object[])
           
static String String.valueOf(Object)
           
static String String.valueOf(char[])
           
static String String.valueOf(char[], int, int)
           
static String String.copyValueOf(char[], int, int)
           
static String String.copyValueOf(char[])
           
static String String.valueOf(boolean)
           
static String String.valueOf(char)
           
static String String.valueOf(int)
           
static String String.valueOf(long)
           
static String String.valueOf(float)
           
static String String.valueOf(double)
           
 String String.intern()
           
abstract  String CharSequence.toString()
           
 String Throwable.getMessage()
           
 String Throwable.getLocalizedMessage()
           
 String Throwable.toString()
           
private  String ClassLoader.defineClassSourceLocation(ProtectionDomain)
           
protected  String ClassLoader.findLibrary(String)
           
private static String[] ClassLoader.initializePath(String)
           
 String Class.toString()
           
 String Class.getName()
           
private  String Class.getName0()
           
 String Class.getSimpleName()
           
 String Class.getCanonicalName()
           
private  String Class.getSimpleBinaryName()
           
private  String Class.resolveName(String)
           
private  String Class.getGenericSignature()
           
private static String Class.argumentTypesToString(Class[])
           
static String Byte.toString(byte)
           
 String Byte.toString()
           
 String Character.toString()
           
static String Character.toString(char)
           
static String Double.toString(double)
           
static String Double.toHexString(double)
           
 String Double.toString()
           
static String Float.toString(float)
           
static String Float.toHexString(float)
           
 String Float.toString()
           
static String Integer.toString(int, int)
           
static String Integer.toHexString(int)
           
static String Integer.toOctalString(int)
           
static String Integer.toBinaryString(int)
           
private static String Integer.toUnsignedString(int, int)
           
static String Integer.toString(int)
           
 String Integer.toString()
           
static String Long.toString(long, int)
           
static String Long.toHexString(long)
           
static String Long.toOctalString(long)
           
static String Long.toBinaryString(long)
           
private static String Long.toUnsignedString(long, int)
           
static String Long.toString(long)
           
 String Long.toString()
           
static String Short.toString(short)
           
 String Short.toString()
           
 String AbstractStringBuilder.substring(int)
           
 String AbstractStringBuilder.substring(int, int)
           
abstract  String AbstractStringBuilder.toString()
           
 String StringBuffer.substring(int)
           
 String StringBuffer.substring(int, int)
           
 String StringBuffer.toString()
           
 

Methods in java.lang with parameters of type String
 byte[] String.getBytes(String)
           
 boolean String.equalsIgnoreCase(String)
           
 int String.compareTo(String)
           
 int String.compareToIgnoreCase(String)
           
 boolean String.regionMatches(int, String, int, int)
           
 boolean String.regionMatches(boolean, int, String, int, int)
           
 boolean String.startsWith(String, int)
           
 boolean String.startsWith(String)
           
 boolean String.endsWith(String)
           
 int String.indexOf(String)
           
 int String.indexOf(String, int)
           
 int String.lastIndexOf(String)
           
 int String.lastIndexOf(String, int)
           
 String String.concat(String)
           
 boolean String.matches(String)
           
 String String.replaceFirst(String, String)
           
 String String.replaceAll(String, String)
           
 String[] String.split(String, int)
           
 String[] String.split(String)
           
static String String.format(String, Object[])
           
static String String.format(Locale, String, Object[])
           
 Class ClassLoader.loadClass(String)
           
protected  Class ClassLoader.loadClass(String, boolean)
           
private  Class ClassLoader.loadClassInternal(String)
           
protected  Class ClassLoader.findClass(String)
           
protected  Class ClassLoader.defineClass(String, byte[], int, int)
           
private  ProtectionDomain ClassLoader.preDefineClass(String, ProtectionDomain)
           
private  Class ClassLoader.defineTransformedClass(String, byte[], int, int, ProtectionDomain, ClassFormatError, String)
           
protected  Class ClassLoader.defineClass(String, byte[], int, int, ProtectionDomain)
           
protected  Class ClassLoader.defineClass(String, ByteBuffer, ProtectionDomain)
           
private  Class ClassLoader.defineClass0(String, byte[], int, int, ProtectionDomain)
           
private  Class ClassLoader.defineClass1(String, byte[], int, int, ProtectionDomain, String)
           
private  Class ClassLoader.defineClass2(String, ByteBuffer, int, int, ProtectionDomain, String)
           
private  boolean ClassLoader.checkName(String)
           
private  void ClassLoader.checkCerts(String, CodeSource)
           
protected  Class ClassLoader.findSystemClass(String)
           
private  Class ClassLoader.findBootstrapClass0(String)
           
private  Class ClassLoader.findBootstrapClass(String)
           
protected  Class ClassLoader.findLoadedClass(String)
           
private  Class ClassLoader.findLoadedClass0(String)
           
 URL ClassLoader.getResource(String)
           
 Enumeration ClassLoader.getResources(String)
           
protected  URL ClassLoader.findResource(String)
           
protected  Enumeration ClassLoader.findResources(String)
           
static URL ClassLoader.getSystemResource(String)
           
static Enumeration ClassLoader.getSystemResources(String)
           
private static URL ClassLoader.getBootstrapResource(String)
           
private static Enumeration ClassLoader.getBootstrapResources(String)
           
 InputStream ClassLoader.getResourceAsStream(String)
           
static InputStream ClassLoader.getSystemResourceAsStream(String)
           
protected  Package ClassLoader.definePackage(String, String, String, String, String, String, String, URL)
           
protected  Package ClassLoader.getPackage(String)
           
protected  String ClassLoader.findLibrary(String)
           
private static String[] ClassLoader.initializePath(String)
           
(package private) static void ClassLoader.loadLibrary(Class, String, boolean)
           
(package private) static long ClassLoader.findNative(ClassLoader, String)
           
 void ClassLoader.setPackageAssertionStatus(String, boolean)
           
 void ClassLoader.setClassAssertionStatus(String, boolean)
           
(package private)  boolean ClassLoader.desiredAssertionStatus(String)
           
static Class Class.forName(String)
           
static Class Class.forName(String, boolean, ClassLoader)
           
private static Class Class.forName0(String, boolean, ClassLoader)
           
 Field Class.getField(String)
           
 Method Class.getMethod(String, Class[])
           
 Field Class.getDeclaredField(String)
           
 Method Class.getDeclaredMethod(String, Class[])
           
 InputStream Class.getResourceAsStream(String)
           
 URL Class.getResource(String)
           
(package private) static Class Class.getPrimitiveClass(String)
           
private  String Class.resolveName(String)
           
private  Field Class.searchFields(Field[], String)
           
private  Field Class.getField0(String)
           
private static Method Class.searchMethods(Method[], String, Class[])
           
private  Method Class.getMethod0(String, Class[])
           
static byte Byte.parseByte(String)
           
static byte Byte.parseByte(String, int)
           
static Byte Byte.valueOf(String, int)
           
static Byte Byte.valueOf(String)
           
static Byte Byte.decode(String)
           
(package private) static NumberFormatException NumberFormatException.forInputString(String)
           
static Double Double.valueOf(String)
           
static double Double.parseDouble(String)
           
static Float Float.valueOf(String)
           
static float Float.parseFloat(String)
           
static int Integer.parseInt(String, int)
           
static int Integer.parseInt(String)
           
static Integer Integer.valueOf(String, int)
           
static Integer Integer.valueOf(String)
           
static Integer Integer.getInteger(String)
           
static Integer Integer.getInteger(String, int)
           
static Integer Integer.getInteger(String, Integer)
           
static Integer Integer.decode(String)
           
static long Long.parseLong(String, int)
           
static long Long.parseLong(String)
           
static Long Long.valueOf(String, int)
           
static Long Long.valueOf(String)
           
static Long Long.decode(String)
           
static Long Long.getLong(String)
           
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.valueOf(String, int)
           
static Short Short.valueOf(String)
           
static Short Short.decode(String)
           
 AbstractStringBuilder AbstractStringBuilder.append(String)
           
 AbstractStringBuilder AbstractStringBuilder.replace(int, int, String)
           
 AbstractStringBuilder AbstractStringBuilder.insert(int, String)
           
 int AbstractStringBuilder.indexOf(String)
           
 int AbstractStringBuilder.indexOf(String, int)
           
 int AbstractStringBuilder.lastIndexOf(String)
           
 int AbstractStringBuilder.lastIndexOf(String, int)
           
 StringBuffer StringBuffer.append(String)
           
 StringBuffer StringBuffer.replace(int, int, String)
           
 StringBuffer StringBuffer.insert(int, String)
           
 int StringBuffer.indexOf(String)
           
 int StringBuffer.indexOf(String, int)
           
 int StringBuffer.lastIndexOf(String)
           
 int StringBuffer.lastIndexOf(String, int)
           
 AbstractStringBuilder StringBuffer.insert(int, String)
           
 AbstractStringBuilder StringBuffer.replace(int, int, String)
           
 AbstractStringBuilder 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)
           
UnsupportedOperationException(String, Throwable)
           
ClassNotFoundException(String)
           
ClassNotFoundException(String, Throwable)
           
ClassCastException(String)
           
Error(String)
           
Error(String, Throwable)
           
Byte(String)
           
IllegalArgumentException(String)
           
IllegalArgumentException(String, Throwable)
           
NumberFormatException(String)
           
NullPointerException(String)
           
Double(String)
           
IllegalStateException(String)
           
IllegalStateException(String, Throwable)
           
IndexOutOfBoundsException(String)
           
ArithmeticException(String)
           
Float(String)
           
Integer(String)
           
Long(String)
           
Short(String)
           
VirtualMachineError(String)
           
OutOfMemoryError(String)
           
StringBuffer(String)
           
NoSuchMethodException(String)
           
SecurityException(String)
           
SecurityException(String, Throwable)
           
InternalError(String)
           
CloneNotSupportedException(String)
           
IllegalAccessException(String)
           
 

Uses of String in java.lang.reflect
 

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

Methods in java.lang.reflect that return String
private  String Method.getGenericSignature()
           
 String Method.getName()
           
 String Method.toString()
           
 String Method.toGenericString()
           
abstract  String Member.getName()
           
private  String Field.getGenericSignature()
           
 String Field.getName()
           
 String Field.toString()
           
 String Field.toGenericString()
           
(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, String, byte[], byte[], byte[])
           
Field(Class, String, Class, int, int, String, byte[])
           
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(int)
           
 String BigInteger.toString()
           
 

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

Uses of String in java.util
 

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

Methods in java.util with parameters of type String
 Object Properties.setProperty(String, String)
           
private  String Properties.saveConvert(String, boolean, boolean)
           
private static void Properties.writeComments(BufferedWriter, String)
           
 void Properties.save(OutputStream, String)
           
 void Properties.store(Writer, String)
           
 void Properties.store(OutputStream, String)
           
private  void Properties.store0(BufferedWriter, String, boolean)
           
 void Properties.storeToXML(OutputStream, String)
           
 void Properties.storeToXML(OutputStream, String, String)
           
 String Properties.getProperty(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  String Pattern.pattern
           
 

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

Methods in java.util.regex with parameters of type String
static Pattern Pattern.compile(String)
           
static Pattern Pattern.compile(String, int)
           
static boolean Pattern.matches(String, CharSequence)
           
static String Pattern.quote(String)
           
private  String Pattern.produceEquivalentAlternation(String)
           
private  String[] Pattern.producePermutations(String)
           
private  String Pattern.composeOneStep(String)
           
private  void Pattern.accept(int, String)
           
private  PatternSyntaxException Pattern.error(String)
           
private  Pattern.CharProperty Pattern.unicodeBlockPropertyFor(String)
           
private  Pattern.CharProperty Pattern.charPropertyNodeFor(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.
static String JmlAdmissibilityVisitor.ADMISSIBILITY_CLASSICAL
          Command line option to enable classical admissibility checks
static String JmlAdmissibilityVisitor.ADMISSIBILITY_NONE
          Command line option to disable admissibility checks
static String JmlAdmissibilityVisitor.ADMISSIBILITY_OWNERSHIP
          Command line option to enable ownership admissibility checks
private  String JmlCommonOptions.filter
           
private  String JmlCommonOptions.experiment
           
private  String JmlCommonOptions.universesx
           
private  String JmlCommonOptions.excludefiles
           
private  String JmlCommonOptions.admissibility
           
(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
           
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 JmlPredicate.toString()
           
 String JmlReadableIfVarAssertion.fieldIdent()
           
 String JmlWritableIfVarAssertion.fieldIdent()
           
 String JmlRefinePrefix.fileName()
           
 String JmlRelationalExpression.opString()
           
 String JmlRelationalExpression.toString()
           
 String JmlSetComprehension.ident()
           
 String JmlSignalsClause.ident()
           
 String JmlSpecExpression.toString()
           
 String JmlStoreRefExpression.getName()
           
 String JmlStoreRefExpression.toString()
           
 String JmlVariableDefinition.racField()
          Returns the name of RAC field generated for this variable.
private static String JmlAdmissibilityVisitor.getAdmissibility()
          This method takes the command line admissibility string and returns the appropriate canonical admissibility option string.
 String JmlAssignableFieldSet.toString()
           
 String JmlSourceMethod.getGenericSignature()
           
 String JmlDataGroupMemberMap.toString()
           
 String JmlBinaryMember.ident()
           
 String JmlBinaryMember.stringRepresentation()
           
 String JmlBinaryMethod.stringRepresentation()
           
 String JmlCastExpression.toString()
           
 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.admissibility()
           
 String JmlCommonOptions.set_admissibility(String admissibility)
           
 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, CTypeVariable[] typevariables, 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, CTypeVariable[] typevariables, 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, CTypeVariable[] typevariables, 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)
           
 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.dumpNonNulls(String msg)
           
 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.
 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.
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.
 CTypeVariable JmlClassContext.lookupTypeVariable(String ident)
           
 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)
           
 String JmlCommonOptions.set_admissibility(String admissibility)
           
 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)
           
 CTypeVariable JmlMethodContext.lookupTypeVariable(String ident)
           
 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.
 void JmlFlowControlContext.dumpNonNulls(String msg)
           
 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  org.multijava.util.gui.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)
           
 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)
           
static void NonNullStatistics.hmNonnullPut(String key, String value)
           
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, CTypeVariable[] typevariables, boolean isAnonymous, boolean isMember, boolean deprecated)
          Constructs a class export from source
TestSuite(String name)
           
JmlFormalParameter(TokenReference where, long modifiers, int desc, CSpecializedType type, String ident)
          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, CTypeVariable[] typevariables, 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, CTypeVariable[] typevariables, 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, CTypeVariable[] typevariables, 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, long modifiers, 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, CTypeVariable[] typevariables, 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
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(