edu.mit.csail.sdg.squander.spec.ClassSpec Class Reference
[Specification]
Classes | |
| class | Invariant |
Public Member Functions | |
| ClassSpec (JType.Unary jtype, JavaScene javaScene) | |
| ClassSpec (Class clz, JType.Unary[] typeParams, JavaScene javaScene) | |
| boolean | isEmpty () |
| JType.Unary | jtype () |
| Class | clz () |
| JType.Unary[] | typeParams () |
| Collection< ClassSpec > | subs () |
| void | setSubs (Collection< ClassSpec > subs) |
| void | addSuper (ClassSpec superClsSpec) |
| JField | findField (String name) |
| JField | ensureField (String name) |
| JField | ensureField (String name, boolean recurse) |
| Collection< Invariant > | invariants () |
| Collection< Source > | specFields () |
| boolean | hasSpecField (String name) |
| Collection< JField > | usedFields () |
| Collection< JField > | usedFieldsAll () |
| void | addInvariant (Source src) |
| void | addSpecFieldSource (Source src) |
| void | addSpecField (JField field) |
| void | typecheck () |
| void | translateSpecs (ForgeScene forgeScene) |
| String | toString () |
Private Member Functions | |
| void | addUsedField (JField field) |
| String | extractSpecFieldName (Source src) |
Private Attributes | |
| final JType.Unary | jtype |
| final JavaScene | javaScene |
| Collection< ClassSpec > | subs |
| List< ClassSpec > | supers = new LinkedList<ClassSpec>() |
| Map< String, Source > | specFieldSources = new HashMap<String, Source>() |
| List< Source > | invariantSources = new ArrayList<Source>() |
| List< Invariant > | invariants = new ArrayList<Invariant>() |
| Map< String, JField > | usedFields = new HashMap<String, JField>() |
Detailed Description
Definition at line 24 of file ClassSpec.java.
Constructor & Destructor Documentation
| edu.mit.csail.sdg.squander.spec.ClassSpec.ClassSpec | ( | JType.Unary | jtype, | |
| JavaScene | javaScene | |||
| ) |
Definition at line 56 of file ClassSpec.java.
| edu.mit.csail.sdg.squander.spec.ClassSpec.ClassSpec | ( | Class | clz, | |
| JType.Unary[] | typeParams, | |||
| JavaScene | javaScene | |||
| ) |
Definition at line 61 of file ClassSpec.java.
Member Function Documentation
| void edu.mit.csail.sdg.squander.spec.ClassSpec.addInvariant | ( | Source | src | ) |
Definition at line 158 of file ClassSpec.java.
References edu.mit.csail.sdg.squander.spec.JavaScene.isFinished().
Referenced by edu.mit.csail.sdg.squander.spec.JavaScene.createClassSpec().
| void edu.mit.csail.sdg.squander.spec.ClassSpec.addSpecField | ( | JField | field | ) |
Definition at line 168 of file ClassSpec.java.
References edu.mit.csail.sdg.squander.spec.JavaScene.isFinished(), and edu.mit.csail.sdg.squander.spec.JField.isSpec().
Referenced by edu.mit.csail.sdg.squander.spec.TypeChecker.visitFieldDeclaration().
| void edu.mit.csail.sdg.squander.spec.ClassSpec.addSpecFieldSource | ( | Source | src | ) |
Definition at line 163 of file ClassSpec.java.
References edu.mit.csail.sdg.squander.spec.JavaScene.isFinished().
Referenced by edu.mit.csail.sdg.squander.spec.JavaScene.createClassSpec().
| void edu.mit.csail.sdg.squander.spec.ClassSpec.addSuper | ( | ClassSpec | superClsSpec | ) |
Definition at line 76 of file ClassSpec.java.
Referenced by edu.mit.csail.sdg.squander.spec.JavaScene.ensureClass().
| void edu.mit.csail.sdg.squander.spec.ClassSpec.addUsedField | ( | JField | field | ) | [private] |
Definition at line 221 of file ClassSpec.java.
References edu.mit.csail.sdg.squander.spec.JField.name.
| Class edu.mit.csail.sdg.squander.spec.ClassSpec.clz | ( | ) |
Definition at line 70 of file ClassSpec.java.
Referenced by edu.mit.csail.sdg.squander.spec.TypeChecker.getFldOwner(), and edu.mit.csail.sdg.squander.spec.JavaScene.subTypes().
| JField edu.mit.csail.sdg.squander.spec.ClassSpec.ensureField | ( | String | name, | |
| boolean | recurse | |||
| ) |
Definition at line 96 of file ClassSpec.java.
References edu.mit.csail.sdg.squander.spec.ISpecProvider.extractFieldSpec(), edu.mit.csail.sdg.squander.spec.JavaScene.isFinished(), edu.mit.csail.sdg.squander.spec.Source.isFuncField(), edu.mit.csail.sdg.squander.spec.JField.newJavaField(), edu.mit.csail.sdg.squander.spec.TypeChecker.setClsSpecForSpecField(), edu.mit.csail.sdg.squander.spec.JField.setFuncFlag(), and edu.mit.csail.sdg.squander.spec.Source.typecheck().
| JField edu.mit.csail.sdg.squander.spec.ClassSpec.ensureField | ( | String | name | ) |
Definition at line 91 of file ClassSpec.java.
Referenced by edu.mit.csail.sdg.squander.spec.NameSpace.findField().
| String edu.mit.csail.sdg.squander.spec.ClassSpec.extractSpecFieldName | ( | Source | src | ) | [private] |
Definition at line 225 of file ClassSpec.java.
References edu.mit.csail.sdg.squander.spec.Source.source.
| JField edu.mit.csail.sdg.squander.spec.ClassSpec.findField | ( | String | name | ) |
Definition at line 78 of file ClassSpec.java.
Referenced by edu.mit.csail.sdg.squander.serializer.special.SetSer.absFunc(), edu.mit.csail.sdg.squander.serializer.special.MapSer.absFunc(), edu.mit.csail.sdg.squander.serializer.special.ListSer.absFunc(), edu.mit.csail.sdg.squander.serializer.special.ArraySer.absFunc(), edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.arrayElems(), and edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.arrayLength().
| boolean edu.mit.csail.sdg.squander.spec.ClassSpec.hasSpecField | ( | String | name | ) |
Definition at line 145 of file ClassSpec.java.
Referenced by edu.mit.csail.sdg.squander.spec.TypeChecker.getFldOwner().
| Collection<Invariant> edu.mit.csail.sdg.squander.spec.ClassSpec.invariants | ( | ) |
Definition at line 143 of file ClassSpec.java.
| boolean edu.mit.csail.sdg.squander.spec.ClassSpec.isEmpty | ( | ) |
Definition at line 65 of file ClassSpec.java.
| JType.Unary edu.mit.csail.sdg.squander.spec.ClassSpec.jtype | ( | ) |
Definition at line 69 of file ClassSpec.java.
| void edu.mit.csail.sdg.squander.spec.ClassSpec.setSubs | ( | Collection< ClassSpec > | subs | ) |
Definition at line 74 of file ClassSpec.java.
Referenced by edu.mit.csail.sdg.squander.spec.JavaScene.subTypes().
| Collection<Source> edu.mit.csail.sdg.squander.spec.ClassSpec.specFields | ( | ) |
Definition at line 144 of file ClassSpec.java.
| Collection<ClassSpec> edu.mit.csail.sdg.squander.spec.ClassSpec.subs | ( | ) |
Definition at line 73 of file ClassSpec.java.
| String edu.mit.csail.sdg.squander.spec.ClassSpec.toString | ( | ) |
Definition at line 213 of file ClassSpec.java.
| void edu.mit.csail.sdg.squander.spec.ClassSpec.translateSpecs | ( | ForgeScene | forgeScene | ) |
Definition at line 185 of file ClassSpec.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.getEnv(), edu.mit.csail.sdg.squander.spec.Frame.locations, edu.mit.csail.sdg.squander.spec.ForgeScene.newThisVariable(), edu.mit.csail.sdg.squander.spec.JField.setAbsFun(), edu.mit.csail.sdg.squander.spec.JField.setBound(), edu.mit.csail.sdg.squander.spec.JField.setDomain(), edu.mit.csail.sdg.squander.spec.JField.setFrame(), edu.mit.csail.sdg.squander.spec.ForgeEnv.thisVar(), and edu.mit.csail.sdg.squander.spec.Source.translate().
| void edu.mit.csail.sdg.squander.spec.ClassSpec.typecheck | ( | ) |
Type-checks only invariants
Definition at line 177 of file ClassSpec.java.
Referenced by edu.mit.csail.sdg.squander.spec.JavaScene.ensureClass().
| JType.Unary [] edu.mit.csail.sdg.squander.spec.ClassSpec.typeParams | ( | ) |
Definition at line 71 of file ClassSpec.java.
Referenced by edu.mit.csail.sdg.squander.spec.TypeChecker.getFldOwner().
| Collection<JField> edu.mit.csail.sdg.squander.spec.ClassSpec.usedFields | ( | ) |
Definition at line 146 of file ClassSpec.java.
| Collection<JField> edu.mit.csail.sdg.squander.spec.ClassSpec.usedFieldsAll | ( | ) |
Definition at line 147 of file ClassSpec.java.
Referenced by edu.mit.csail.sdg.squander.serializer.special.DefaultObjSer.absFunc().
Member Data Documentation
List<Invariant> edu.mit.csail.sdg.squander.spec.ClassSpec.invariants = new ArrayList<Invariant>() [private] |
Definition at line 52 of file ClassSpec.java.
List<Source> edu.mit.csail.sdg.squander.spec.ClassSpec.invariantSources = new ArrayList<Source>() [private] |
Definition at line 51 of file ClassSpec.java.
final JavaScene edu.mit.csail.sdg.squander.spec.ClassSpec.javaScene [private] |
Definition at line 45 of file ClassSpec.java.
final JType.Unary edu.mit.csail.sdg.squander.spec.ClassSpec.jtype [private] |
Definition at line 44 of file ClassSpec.java.
Referenced by edu.mit.csail.sdg.squander.spec.TypeChecker.getFldOwner(), edu.mit.csail.sdg.squander.spec.JavaScene.subTypes(), edu.mit.csail.sdg.squander.spec.TypeChecker.visitAmbiguous(), and edu.mit.csail.sdg.squander.spec.TypeChecker.visitFieldDeclaration().
Map<String, Source> edu.mit.csail.sdg.squander.spec.ClassSpec.specFieldSources = new HashMap<String, Source>() [private] |
Definition at line 50 of file ClassSpec.java.
Collection<ClassSpec> edu.mit.csail.sdg.squander.spec.ClassSpec.subs [private] |
Definition at line 47 of file ClassSpec.java.
Referenced by edu.mit.csail.sdg.squander.spec.JavaScene.subTypes().
List<ClassSpec> edu.mit.csail.sdg.squander.spec.ClassSpec.supers = new LinkedList<ClassSpec>() [private] |
Definition at line 48 of file ClassSpec.java.
Map<String, JField> edu.mit.csail.sdg.squander.spec.ClassSpec.usedFields = new HashMap<String, JField>() [private] |
Definition at line 54 of file ClassSpec.java.
The documentation for this class was generated from the following file:
- src/edu/mit/csail/sdg/squander/spec/ClassSpec.java
