edu.mit.csail.sdg.squander.spec.MethodSpec Class Reference
[Specification]

Collaboration diagram for edu.mit.csail.sdg.squander.spec.MethodSpec:
Collaboration graph
[legend]

List of all members.

Classes

class  CaseSource

Public Member Functions

Options options ()
boolean isHelper ()
boolean isPure ()
List< CaseSource > cases ()
boolean isTrivial ()
Map< JType.Unary, Integer > freshObjects ()
void typecheck (JavaScene javaScene)
void translateSpecs (ForgeEnv env, ForgeScene forgeScene)
void addOptions (Options opt)

Package Functions

 MethodSpec ()
void addFreshObj (Class<?> cls, Class<?>[] typeParams, int num)
void addCase (Source requires, Source ensures, Source modifies, boolean exceptional)
void mergeCasesWith (MethodSpec ms)
void makeHelper ()
void makePure ()

Private Attributes

final List< CaseSource > cases
final Map< String, CaseSource > pre2cs = new HashMap<String, CaseSource>()
final Map< JType.Unary, Integer > freshObj = new HashMap<JType.Unary, Integer>()
Options options
boolean helper
boolean pure

Detailed Description

Method specification source. Abstract data type that holds method specifications.

Empty specification source should be the identity with respect to the union operation.

Author:
kuat
Aleksandar Milicevic

Definition at line 27 of file MethodSpec.java.

Constructor & Destructor Documentation

edu.mit.csail.sdg.squander.spec.MethodSpec.MethodSpec (  )  [package]

Definition at line 73 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.cases(), edu.mit.csail.sdg.squander.spec.MethodSpec.helper, and edu.mit.csail.sdg.squander.spec.MethodSpec.pure.

Member Function Documentation

void edu.mit.csail.sdg.squander.spec.MethodSpec.addCase ( Source  requires,
Source  ensures,
Source  modifies,
boolean  exceptional 
) [package]

Definition at line 114 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.cases(), edu.mit.csail.sdg.squander.spec.MethodSpec.CaseSource.exceptional, edu.mit.csail.sdg.squander.spec.MethodSpec.CaseSource.frmSrc, edu.mit.csail.sdg.squander.spec.Source.ns, edu.mit.csail.sdg.squander.spec.MethodSpec.CaseSource.postSrc(), edu.mit.csail.sdg.squander.spec.MethodSpec.pre2cs, edu.mit.csail.sdg.squander.spec.Source.rule, and edu.mit.csail.sdg.squander.spec.Source.source.

Referenced by edu.mit.csail.sdg.squander.spec.ReflectiveSpecProvider.extractMethodSpecNonRecursive().

void edu.mit.csail.sdg.squander.spec.MethodSpec.addFreshObj ( Class<?>  cls,
Class<?>[]  typeParams,
int  num 
) [package]

Definition at line 103 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.freshObj.

Referenced by edu.mit.csail.sdg.squander.spec.ReflectiveSpecProvider.extractMethodSpecNonRecursive().

void edu.mit.csail.sdg.squander.spec.MethodSpec.addOptions ( Options  opt  ) 

Definition at line 99 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.options().

Referenced by edu.mit.csail.sdg.squander.spec.ReflectiveSpecProvider.extractMethodSpecNonRecursive().

List<CaseSource> edu.mit.csail.sdg.squander.spec.MethodSpec.cases (  ) 

Definition at line 68 of file MethodSpec.java.

Referenced by edu.mit.csail.sdg.squander.spec.MethodSpec.addCase(), edu.mit.csail.sdg.squander.spec.MethodSpec.isTrivial(), edu.mit.csail.sdg.squander.spec.MethodSpec.mergeCasesWith(), edu.mit.csail.sdg.squander.spec.MethodSpec.MethodSpec(), edu.mit.csail.sdg.squander.spec.MethodSpec.translateSpecs(), and edu.mit.csail.sdg.squander.spec.MethodSpec.typecheck().

Map<JType.Unary, Integer> edu.mit.csail.sdg.squander.spec.MethodSpec.freshObjects (  ) 

Definition at line 71 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.freshObj.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.createFreshObjects().

boolean edu.mit.csail.sdg.squander.spec.MethodSpec.isHelper (  ) 

Definition at line 66 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.helper.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.getSpec().

boolean edu.mit.csail.sdg.squander.spec.MethodSpec.isPure (  ) 

Definition at line 67 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.pure.

boolean edu.mit.csail.sdg.squander.spec.MethodSpec.isTrivial (  ) 

Definition at line 69 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.cases(), and edu.mit.csail.sdg.squander.spec.MethodSpec.pure.

void edu.mit.csail.sdg.squander.spec.MethodSpec.makeHelper (  )  [package]

Definition at line 145 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.helper.

void edu.mit.csail.sdg.squander.spec.MethodSpec.makePure (  )  [package]

Definition at line 149 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.pure.

Referenced by edu.mit.csail.sdg.squander.spec.ReflectiveSpecProvider.extractMethodSpecNonRecursive().

void edu.mit.csail.sdg.squander.spec.MethodSpec.mergeCasesWith ( MethodSpec  ms  )  [package]

Definition at line 140 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.cases.

Options edu.mit.csail.sdg.squander.spec.MethodSpec.options (  ) 

Definition at line 65 of file MethodSpec.java.

Referenced by edu.mit.csail.sdg.squander.spec.MethodSpec.addOptions().

void edu.mit.csail.sdg.squander.spec.MethodSpec.translateSpecs ( ForgeEnv  env,
ForgeScene  forgeScene 
)

Definition at line 88 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.cases().

Referenced by edu.mit.csail.sdg.squander.spec.JavaScene.translateSpecs().

void edu.mit.csail.sdg.squander.spec.MethodSpec.typecheck ( JavaScene  javaScene  ) 

Definition at line 79 of file MethodSpec.java.

References edu.mit.csail.sdg.squander.spec.MethodSpec.cases().

Referenced by edu.mit.csail.sdg.squander.spec.JavaScene.setMethod().

Member Data Documentation

final List<CaseSource> edu.mit.csail.sdg.squander.spec.MethodSpec.cases [private]

Definition at line 57 of file MethodSpec.java.

Referenced by edu.mit.csail.sdg.squander.spec.CompositeSpecProvider.extractMethodSpec(), edu.mit.csail.sdg.squander.engine.ForgeConverter.getSpec(), and edu.mit.csail.sdg.squander.spec.MethodSpec.mergeCasesWith().

final Map<JType.Unary, Integer> edu.mit.csail.sdg.squander.spec.MethodSpec.freshObj = new HashMap<JType.Unary, Integer>() [private]

Definition at line 59 of file MethodSpec.java.

Referenced by edu.mit.csail.sdg.squander.spec.MethodSpec.addFreshObj(), and edu.mit.csail.sdg.squander.spec.MethodSpec.freshObjects().

boolean edu.mit.csail.sdg.squander.spec.MethodSpec.helper [private]

Definition at line 62 of file MethodSpec.java.

Referenced by edu.mit.csail.sdg.squander.spec.MethodSpec.isHelper(), edu.mit.csail.sdg.squander.spec.MethodSpec.makeHelper(), and edu.mit.csail.sdg.squander.spec.MethodSpec.MethodSpec().

Options edu.mit.csail.sdg.squander.spec.MethodSpec.options [private]

Definition at line 60 of file MethodSpec.java.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.exeSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.finish().

final Map<String, CaseSource> edu.mit.csail.sdg.squander.spec.MethodSpec.pre2cs = new HashMap<String, CaseSource>() [private]

Definition at line 58 of file MethodSpec.java.

Referenced by edu.mit.csail.sdg.squander.spec.MethodSpec.addCase().

boolean edu.mit.csail.sdg.squander.spec.MethodSpec.pure [private]

Definition at line 63 of file MethodSpec.java.

Referenced by edu.mit.csail.sdg.squander.spec.MethodSpec.isPure(), edu.mit.csail.sdg.squander.spec.MethodSpec.isTrivial(), edu.mit.csail.sdg.squander.spec.MethodSpec.makePure(), and edu.mit.csail.sdg.squander.spec.MethodSpec.MethodSpec().

The documentation for this class was generated from the following file:
Generated by  doxygen 1.6.2-20100208