edu.mit.csail.sdg.squander.spec.Spec.SpecCase Class Reference

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

[legend]

List of all members.

Public Member Functions
ForgeExpression	preOnly ()
ForgeExpression	postOnly ()
ForgeExpression	pre ()
ForgeExpression	post ()
Frame	frame ()
Spec	spec ()
String	toString ()
Private Member Functions
	SpecCase (ForgeExpression requires, ForgeExpression ensures, Frame frame, boolean helper)
Private Attributes
final ForgeExpression	pre
final ForgeExpression	post
final Frame	frame
final boolean	helper

---

Detailed Description

Specification case. Remark that the pre-condition is not in the pre-state.

Author:

Kuat Yessenov (kuat@mit.edu)

Aleksandar Milicevic

Definition at line 41 of file Spec.java.

---

Constructor & Destructor Documentation

edu.mit.csail.sdg.squander.spec.Spec.SpecCase.SpecCase	(	ForgeExpression	requires,
		ForgeExpression	ensures,
		Frame	frame,
		boolean	helper
	)			[private]

Definition at line 47 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.Spec.SpecCase.post(), and edu.mit.csail.sdg.squander.spec.Spec.SpecCase.pre().

---

Member Function Documentation

Frame edu.mit.csail.sdg.squander.spec.Spec.SpecCase.frame

(

)

Definition at line 59 of file Spec.java.

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

ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.SpecCase.post

(

)

Definition at line 57 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.Spec.SpecCase.helper, and edu.mit.csail.sdg.squander.spec.Spec.invariant().

Referenced by edu.mit.csail.sdg.squander.spec.Spec.SpecCase.postOnly(), edu.mit.csail.sdg.squander.spec.Spec.SpecCase.SpecCase(), and edu.mit.csail.sdg.squander.spec.Spec.SpecCase.toString().

ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.SpecCase.postOnly

(

)

Definition at line 55 of file Spec.java.

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

ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.SpecCase.pre

(

)

Definition at line 56 of file Spec.java.

Referenced by edu.mit.csail.sdg.squander.spec.Spec.SpecCase.preOnly(), edu.mit.csail.sdg.squander.spec.Spec.SpecCase.SpecCase(), and edu.mit.csail.sdg.squander.spec.Spec.SpecCase.toString().

ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.SpecCase.preOnly

(

)

Definition at line 54 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.Spec.SpecCase.pre().

Spec edu.mit.csail.sdg.squander.spec.Spec.SpecCase.spec

(

)

Definition at line 60 of file Spec.java.

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(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getPreSpec().

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

(

)

Definition at line 63 of file Spec.java.

References edu.mit.csail.sdg.squander.spec.Spec.SpecCase.frame(), edu.mit.csail.sdg.squander.spec.Spec.SpecCase.helper, edu.mit.csail.sdg.squander.spec.Spec.SpecCase.post(), and edu.mit.csail.sdg.squander.spec.Spec.SpecCase.pre().

---

Member Data Documentation

final Frame edu.mit.csail.sdg.squander.spec.Spec.SpecCase.frame [private]

Definition at line 44 of file Spec.java.

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

final boolean edu.mit.csail.sdg.squander.spec.Spec.SpecCase.helper [private]

Definition at line 45 of file Spec.java.

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

final ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.SpecCase.post [private]

Definition at line 43 of file Spec.java.

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

final ForgeExpression edu.mit.csail.sdg.squander.spec.Spec.SpecCase.pre [private]

Definition at line 42 of file Spec.java.

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

---

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

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