edu.mit.csail.sdg.squander.engine.SquanderImpl Class Reference
[Engine]

Inherits edu::mit::csail::sdg::squander::engine::ISquander.

Inherited by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.

Collaboration diagram for edu.mit.csail.sdg.squander.engine.SquanderImpl:

Public Member Functions
	SquanderImpl ()
ISquanderResult	getLastResult ()
Protected Member Functions
JMethod	convToJMethod (Object caller, String clsName, String methodName, Class<?>[] methodParams)
Iterator<?extends ISquanderResult >	exeMethod (SquanderReporter reporter, Object caller, JMethod m, Object[] methodArgs)
final IEvaluator	checkPre (SpecCase cs, ForgeConverter fconv)
final Iterator<?extends ISquanderResult >	ensurePost (SpecCase cs, ForgeConverter fconv)
Set< GlobalVariable >	getModsForPostState (ForgeConverter fconv, SpecCase sc)
ForgeExpression	getPreSpec (SpecCase cs)
ForgeExpression	getPostSpec (SpecCase cs, ForgeConverter fconv)
Spec	getSpec (ForgeConverter fconv)
IEvaluator	exeSpec (ForgeExpression spec, Set< GlobalVariable > modifies, ForgeConverter fconv)
Protected Attributes
SquanderReporter	reporter
Package Functions
public< R > R	magic (Object caller, String clsName, String methodName, Class<?>[] methodParams, Object[] methodArgs)
public< R > R	magic (Object caller, Method method, Object[] methodArgs)
public< R > R	magic (Object caller, JMethod method, Object[] methodArgs)
Private Attributes
ISquanderResult	lastResult
Spec	spec

Detailed Description

An implementation of the ISquander interface that uses Forge as the back-end.

Author:: Aleksandar Milicevic (aleks@csail.mit.edu)

Definition at line 33 of file SquanderImpl.java.

Constructor & Destructor Documentation

edu.mit.csail.sdg.squander.engine.SquanderImpl.SquanderImpl ( )

Definition at line 40 of file SquanderImpl.java.

Member Function Documentation

final IEvaluator edu.mit.csail.sdg.squander.engine.SquanderImpl.checkPre	(	SpecCase	cs,
		ForgeConverter	fconv
	)			`[protected]`

Check pre-conditions in the specification case.

all values of concrete fields are in bounds all values of spec fields are in bounds

Parameters:

	cs
	options

Returns:: non-null if the pre-condition is satisfied

Definition at line 192 of file SquanderImpl.java.

References edu.mit.csail.sdg.squander.engine.SquanderImpl.exeSpec(), edu.mit.csail.sdg.squander.engine.SquanderImpl.getPreSpec(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.printBounds().

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

JMethod edu.mit.csail.sdg.squander.engine.SquanderImpl.convToJMethod	(	Object	caller,
		String	clsName,
		String	methodName,
		Class<?>[]	methodParams
	)			`[protected]`

Definition at line 126 of file SquanderImpl.java.

References edu.mit.csail.sdg.squander.spec.JMethod.forJavaMethod().

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

final Iterator<? extends ISquanderResult> edu.mit.csail.sdg.squander.engine.SquanderImpl.ensurePost	(	SpecCase	cs,
		ForgeConverter	fconv
	)			`[protected]`

Modifies the heap to ensure the post-condition of the specification case.

that only relations in modifies clause can be changed that new instances should have their relations mentioned in frame that specification fields are bounded to literals according to their abstraction function

Parameters:

	cs
	options

Returns:

Definition at line 219 of file SquanderImpl.java.

References edu.mit.csail.sdg.squander.engine.SquanderImpl.exeSpec(), edu.mit.csail.sdg.squander.spec.Spec.SpecCase.frame, edu.mit.csail.sdg.squander.engine.SquanderImpl.getModsForPostState(), edu.mit.csail.sdg.squander.engine.SquanderImpl.getPostSpec(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.printBounds().

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

Iterator<? extends ISquanderResult> edu.mit.csail.sdg.squander.engine.SquanderImpl.exeMethod	(	SquanderReporter	reporter,
		Object	caller,
		JMethod	m,
		Object[]	methodArgs
	)			`[protected]`

reporter != null; classPath != null; className != null; methodName != null;

Definition at line 148 of file SquanderImpl.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.boundSpecFields(), edu.mit.csail.sdg.squander.spec.Spec.cases, edu.mit.csail.sdg.squander.engine.SquanderImpl.checkPre(), edu.mit.csail.sdg.squander.engine.SquanderImpl.ensurePost(), edu.mit.csail.sdg.squander.engine.SquanderImpl.getSpec(), edu.mit.csail.sdg.squander.engine.SquanderReporter.restoringSpecFields(), edu.mit.csail.sdg.squander.engine.ForgeConverter.setCallContext(), and edu.mit.csail.sdg.squander.engine.SquanderImpl.spec.

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

IEvaluator edu.mit.csail.sdg.squander.engine.SquanderImpl.exeSpec	(	ForgeExpression	spec,
		Set< GlobalVariable >	modifies,
		ForgeConverter	fconv
	)			`[protected]`

Executes the given forge expression.

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.

Definition at line 274 of file SquanderImpl.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeOptions(), edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene, edu.mit.csail.sdg.squander.spec.JavaScene.methodSpec(), edu.mit.csail.sdg.squander.spec.MethodSpec.options, and edu.mit.csail.sdg.squander.engine.ForgeConverter.proc().

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.checkPre(), and edu.mit.csail.sdg.squander.engine.SquanderImpl.ensurePost().

ISquanderResult edu.mit.csail.sdg.squander.engine.SquanderImpl.getLastResult ( )

Returns the result of the last execution.

Implements edu.mit.csail.sdg.squander.engine.ISquander.

Definition at line 118 of file SquanderImpl.java.

References edu.mit.csail.sdg.squander.engine.SquanderImpl.lastResult.

Set<GlobalVariable> edu.mit.csail.sdg.squander.engine.SquanderImpl.getModsForPostState	(	ForgeConverter	fconv,
		SpecCase	sc
	)			`[protected]`

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.

Definition at line 241 of file SquanderImpl.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene, and edu.mit.csail.sdg.squander.spec.ForgeScene.program.

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

ForgeExpression edu.mit.csail.sdg.squander.engine.SquanderImpl.getPostSpec	(	SpecCase	cs,
		ForgeConverter	fconv
	)			`[protected]`

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.

Definition at line 253 of file SquanderImpl.java.

References edu.mit.csail.sdg.squander.spec.Spec.abstractConstraint(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene, edu.mit.csail.sdg.squander.spec.Spec.SpecCase.frame, edu.mit.csail.sdg.squander.spec.Spec.funcConstraint(), edu.mit.csail.sdg.squander.spec.Spec.SpecCase.post, edu.mit.csail.sdg.squander.spec.ForgeScene.program, edu.mit.csail.sdg.squander.spec.Spec.SpecCase.spec(), and edu.mit.csail.sdg.squander.spec.Spec.wellformedPost().

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

ForgeExpression edu.mit.csail.sdg.squander.engine.SquanderImpl.getPreSpec ( SpecCase cs ) [protected]

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.

Definition at line 249 of file SquanderImpl.java.

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

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

Spec edu.mit.csail.sdg.squander.engine.SquanderImpl.getSpec ( ForgeConverter fconv ) [protected]

Definition at line 264 of file SquanderImpl.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.getSpec(), and edu.mit.csail.sdg.squander.engine.SquanderImpl.spec.

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

public<R> R edu.mit.csail.sdg.squander.engine.SquanderImpl.magic	(	Object	caller,
		JMethod	method,
		Object[]	methodArgs
	)			`[package]`

Executes the specification of the given JMethod

Parameters:

	<R>	- the return type
	caller	- the caller instance (`null` if the method is static)
	method	- Squander's internal representation of a method (which includes method's spec). This can be used to execute specs that are not necessarily given as annotations on a Java method
	methodArgs	- actual method arguments

Returns:: - the result of the method's execution (or nothing if the type is void)

Implements edu.mit.csail.sdg.squander.engine.ISquander.

Definition at line 78 of file SquanderImpl.java.

public<R> R edu.mit.csail.sdg.squander.engine.SquanderImpl.magic	(	Object	caller,
		Method	method,
		Object[]	methodArgs
	)			`[package]`

Executes the specification of the given Java method

Parameters:

	<R>	- the return type
	caller	- the caller instance (`null` if the method is static)
	method	- Java method
	methodArgs	- actual method arguments

Returns:: - the result of the method's execution (or nothing if the type is void)

Implements edu.mit.csail.sdg.squander.engine.ISquander.

Definition at line 72 of file SquanderImpl.java.

References edu.mit.csail.sdg.squander.engine.SquanderImpl.magic().

public<R> R edu.mit.csail.sdg.squander.engine.SquanderImpl.magic	(	Object	caller,
		String	clsName,
		String	methodName,
		Class<?>[]	methodParams,
		Object[]	methodArgs
	)			`[package]`

Most general form

Parameters:

	<R>	return type
	caller	the object the method is being invoked on; null if the method is static
	clsName	name of the class of the method (explicitly needed if `caller` is null, otherwise must be equal to caller.getClass().getName())
	methodName	name of the method
	methodParams	types of method parameters
	methodArgs	actual method arguments