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

Collaboration diagram for edu.mit.csail.sdg.squander.spec.Spec:

[legend]

List of all members.

Classes
class	SpecCase
Public Member Functions
	Spec (JavaScene javaScene, ForgeScene forgeScene)
JavaScene	javaScene ()
ForgeScene	forgeScene ()
Collection< SpecCase >	cases ()
boolean	isEmpty ()
void	addCase (ForgeExpression requires, ForgeExpression ensures, Frame frame, boolean helper)
ForgeExpression	invariant ()
ForgeExpression	wellformedPre (Set< GlobalVariable > modifiable)
ForgeExpression	wellformedPost (Set< GlobalVariable > modifiable)
ForgeExpression	concreteConstraint (Set< GlobalVariable > unmodifiable)
ForgeExpression	abstractConstraint ()
ForgeExpression	funcConstraint ()
String	toString ()
Private Member Functions
ForgeExpression	fieldConstraint (JField field)
Private Attributes
final JavaScene	javaScene
final ForgeScene	forgeScene
final List< SpecCase >	cases
Static Private Attributes
static int	fieldCounter = 0

---

Detailed Description

Specification.

proc: Procedure cases: set SpecCase

Author:

Kuat Yessenov (kuat@mit.edu)

Aleksandar Milicevic

Definition at line 32 of file Spec.java.

---

Constructor & Destructor Documentation

edu.mit.csail.sdg.squander.spec.Spec.Spec	(	JavaScene	javaScene,
		ForgeScene	forgeScene
	)

Definition at line 83 of file Spec.java.

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

---

Member Function Documentation

ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.abstractConstraint

(

)

Definition at line 226 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.JavaScene.classSpecs(), edu.mit.csail.sdg.squander.spec.Spec.fieldConstraint(), edu.mit.csail.sdg.squander.spec.Spec.forgeScene(), edu.mit.csail.sdg.squander.spec.Spec.javaScene(), and edu.mit.csail.sdg.squander.spec.ForgeScene.program.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.getPostSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getPostSpec(), edu.mit.csail.sdg.squander.engine.SquanderImpl.getPreSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPreSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getPreSpec(), and edu.mit.csail.sdg.squander.spec.Spec.toString().

void edu.mit.csail.sdg.squander.spec.Spec.addCase	(	ForgeExpression	requires,
		ForgeExpression	ensures,
		Frame	frame,
		boolean	helper
	)

Definition at line 103 of file Spec.java.

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

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

Collection<SpecCase> edu.mit.csail.sdg.squander.spec.Spec.cases

(

)

Definition at line 96 of file Spec.java.

Referenced by edu.mit.csail.sdg.squander.spec.Spec.addCase(), edu.mit.csail.sdg.squander.spec.Spec.isEmpty(), edu.mit.csail.sdg.squander.spec.Spec.Spec(), and edu.mit.csail.sdg.squander.spec.Spec.toString().

ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.concreteConstraint

(

Set< GlobalVariable >

unmodifiable

)

Skips over the unmodifiable vars

Definition at line 208 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.JavaScene.classSpecs(), edu.mit.csail.sdg.squander.spec.Spec.fieldConstraint(), edu.mit.csail.sdg.squander.spec.Spec.forgeScene(), edu.mit.csail.sdg.squander.spec.ForgeScene.global(), edu.mit.csail.sdg.squander.spec.Spec.javaScene(), and edu.mit.csail.sdg.squander.spec.ForgeScene.program.

Referenced by edu.mit.csail.sdg.squander.spec.Spec.toString(), edu.mit.csail.sdg.squander.spec.Spec.wellformedPost(), and edu.mit.csail.sdg.squander.spec.Spec.wellformedPre().

ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.fieldConstraint

(

JField

field

)

[private]

Definition at line 275 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.JField.declaringType, edu.mit.csail.sdg.squander.spec.Spec.fieldCounter, edu.mit.csail.sdg.squander.spec.Spec.forgeScene(), edu.mit.csail.sdg.squander.spec.JField.getAbsFun(), edu.mit.csail.sdg.squander.spec.JField.getBound(), edu.mit.csail.sdg.squander.spec.ForgeScene.global(), edu.mit.csail.sdg.squander.spec.JField.isSpec(), edu.mit.csail.sdg.squander.spec.JField.isStatic(), edu.mit.csail.sdg.squander.spec.JField.owningType, edu.mit.csail.sdg.squander.spec.ForgeScene.program, and edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().

Referenced by edu.mit.csail.sdg.squander.spec.Spec.abstractConstraint(), edu.mit.csail.sdg.squander.spec.Spec.concreteConstraint(), and edu.mit.csail.sdg.squander.spec.Spec.funcConstraint().

ForgeScene edu.mit.csail.sdg.squander.spec.Spec.forgeScene

(

)

Definition at line 95 of file Spec.java.

Referenced by edu.mit.csail.sdg.squander.spec.Spec.abstractConstraint(), edu.mit.csail.sdg.squander.spec.Spec.concreteConstraint(), edu.mit.csail.sdg.squander.spec.Spec.fieldConstraint(), edu.mit.csail.sdg.squander.spec.Spec.funcConstraint(), edu.mit.csail.sdg.squander.spec.Spec.invariant(), edu.mit.csail.sdg.squander.spec.Spec.wellformedPost(), and edu.mit.csail.sdg.squander.spec.Spec.wellformedPre().

ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.funcConstraint

(

)

Definition at line 238 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.JavaScene.classSpecs(), edu.mit.csail.sdg.squander.spec.Spec.fieldConstraint(), edu.mit.csail.sdg.squander.spec.Spec.forgeScene(), edu.mit.csail.sdg.squander.spec.Spec.javaScene(), and edu.mit.csail.sdg.squander.spec.ForgeScene.program.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.getPostSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getPostSpec(), and edu.mit.csail.sdg.squander.spec.Spec.toString().

ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.invariant

(

)

Semantic meaning of a specification. OR of old(pre) AND of old(pre) => post /\ frame All modifiable global variables across frames. Expression denoting the valid state semantics of invariants: For all relevant classes, for any instance in the class all invariants must hold. The only exception is for constructors to avoid invariant condition on the of "this" (the exact type, not super-types.)

Definition at line 150 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.JavaScene.classSpecs(), edu.mit.csail.sdg.squander.spec.Spec.forgeScene(), edu.mit.csail.sdg.squander.spec.Spec.javaScene(), edu.mit.csail.sdg.squander.spec.ForgeScene.program, and edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().

Referenced by edu.mit.csail.sdg.squander.spec.Spec.SpecCase.post().

boolean edu.mit.csail.sdg.squander.spec.Spec.isEmpty

(

)

Definition at line 97 of file Spec.java.

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

JavaScene edu.mit.csail.sdg.squander.spec.Spec.javaScene

(

)

Definition at line 94 of file Spec.java.

Referenced by edu.mit.csail.sdg.squander.spec.Spec.abstractConstraint(), edu.mit.csail.sdg.squander.spec.Spec.concreteConstraint(), edu.mit.csail.sdg.squander.spec.Spec.funcConstraint(), and edu.mit.csail.sdg.squander.spec.Spec.invariant().

String edu.mit.csail.sdg.squander.spec.Spec.toString

(

)

Definition at line 251 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.Spec.abstractConstraint(), edu.mit.csail.sdg.squander.spec.Spec.cases(), edu.mit.csail.sdg.squander.spec.Spec.concreteConstraint(), and edu.mit.csail.sdg.squander.spec.Spec.funcConstraint().

ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.wellformedPost

(

Set< GlobalVariable >

modifiable

)

Java language constraints for the post-state Language constraints for post-state

Parameters:

modifiable

Definition at line 193 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.Spec.concreteConstraint(), edu.mit.csail.sdg.squander.spec.Spec.forgeScene(), edu.mit.csail.sdg.squander.spec.ForgeScene.program, edu.mit.csail.sdg.squander.spec.ForgeScene.returnVar, and edu.mit.csail.sdg.squander.spec.ForgeScene.throwVar.

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

ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.wellformedPre

(

Set< GlobalVariable >

modifiable

)

Java language constraints for the pre-state

Parameters:

modifiable

Definition at line 172 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.ForgeScene.args, edu.mit.csail.sdg.squander.spec.Spec.concreteConstraint(), edu.mit.csail.sdg.squander.spec.Spec.forgeScene(), edu.mit.csail.sdg.squander.spec.ForgeScene.program, and edu.mit.csail.sdg.squander.spec.ForgeScene.thisVar.

---

Member Data Documentation

final List<SpecCase> edu.mit.csail.sdg.squander.spec.Spec.cases [private]

Definition at line 77 of file Spec.java.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.exeMethod().

int edu.mit.csail.sdg.squander.spec.Spec.fieldCounter = 0 [static, private]

Definition at line 73 of file Spec.java.

Referenced by edu.mit.csail.sdg.squander.spec.Spec.fieldConstraint().

final ForgeScene edu.mit.csail.sdg.squander.spec.Spec.forgeScene [private]

Definition at line 76 of file Spec.java.

final JavaScene edu.mit.csail.sdg.squander.spec.Spec.javaScene [private]

Definition at line 75 of file Spec.java.

---

The documentation for this class was generated from the following file:

• src/edu/mit/csail/sdg/squander/spec/Spec.java