edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree Class Reference
Public Member Functions | |
| BinarySearchTree () | |
| void | runMin () |
Static Public Member Functions | |
| static void | main (String[] args) |
Private Member Functions | |
| ForgeCFG | cfgMin () |
| ForgeBounds | bounds () |
Static Private Member Functions | |
| static SolveOptions | options () |
Private Attributes | |
| ForgeProgram | program |
| InstanceDomain | node |
| InstanceDomain | bst |
| InstanceLiteral | nodeInsts [] |
| InstanceLiteral | bstInst |
| GlobalVariable | root |
| GlobalVariable | key |
| GlobalVariable | left |
| GlobalVariable | right |
| GlobalVariable | parent |
| LocalVariable | minRet |
| ForgeProcedure | minProc |
Detailed Description
An example of a Forge program that implements and Binary Search Tree data structure and a couple of operations on it.
Definition at line 31 of file BinarySearchTree.java.
Constructor & Destructor Documentation
| edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.BinarySearchTree | ( | ) |
Creates Forge programs, instance domains, global variables, literal instances, procedures and such
Definition at line 54 of file BinarySearchTree.java.
References edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bst, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bstInst, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.key, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.left, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.minProc, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.minRet, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.node, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.nodeInsts, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.parent, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.program, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.right, and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.root.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.main().
Member Function Documentation
| ForgeBounds edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bounds | ( | ) | [private] |
Returns Forge bounds that bound initial state space, i.e. encode a binary search tree into Forge bounds using boundInitial method.
Definition at line 120 of file BinarySearchTree.java.
References edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bst, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bstInst, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.key, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.left, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.node, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.nodeInsts, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.parent, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.program, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.right, and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.root.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.runMin().
| ForgeCFG edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.cfgMin | ( | ) | [private] |
Returns the specs for the min operation
Definition at line 108 of file BinarySearchTree.java.
References edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.key, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.minProc, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.minRet, edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.node, and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.program.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.runMin().
| static void edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.main | ( | String[] | args | ) | [static] |
Definition at line 160 of file BinarySearchTree.java.
References edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.BinarySearchTree(), and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.runMin().
| static SolveOptions edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.options | ( | ) | [static, private] |
Returns Forge options for this purpose
Definition at line 99 of file BinarySearchTree.java.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.runMin().
| void edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.runMin | ( | ) |
Runs the min operation on a binary search tree purely based on specs for that operation (no method implementation)
Definition at line 82 of file BinarySearchTree.java.
References edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bounds(), edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.cfgMin(), edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.minRet, and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.options().
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.main().
Member Data Documentation
InstanceDomain edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bst [private] |
Definition at line 35 of file BinarySearchTree.java.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.BinarySearchTree(), and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bounds().
InstanceLiteral edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bstInst [private] |
Definition at line 38 of file BinarySearchTree.java.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.BinarySearchTree(), and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bounds().
GlobalVariable edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.key [private] |
GlobalVariable edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.left [private] |
Definition at line 42 of file BinarySearchTree.java.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.BinarySearchTree(), and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bounds().
ForgeProcedure edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.minProc [private] |
Definition at line 48 of file BinarySearchTree.java.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.BinarySearchTree(), and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.cfgMin().
LocalVariable edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.minRet [private] |
InstanceDomain edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.node [private] |
InstanceLiteral edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.nodeInsts[] [private] |
Definition at line 37 of file BinarySearchTree.java.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.BinarySearchTree(), and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bounds().
GlobalVariable edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.parent [private] |
Definition at line 44 of file BinarySearchTree.java.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.BinarySearchTree(), and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bounds().
ForgeProgram edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.program [private] |
GlobalVariable edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.right [private] |
Definition at line 43 of file BinarySearchTree.java.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.BinarySearchTree(), and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bounds().
GlobalVariable edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.root [private] |
Definition at line 40 of file BinarySearchTree.java.
Referenced by edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.BinarySearchTree(), and edu.mit.csail.sdg.squander.forge_examples.BinarySearchTree.bounds().
The documentation for this class was generated from the following file:
- src/edu/mit/csail/sdg/squander/forge_examples/BinarySearchTree.java
