jack.plugin.source
Class JmlClauseGenerator

java.lang.Object
  jack.plugin.RunnableWithError
      jack.plugin.source.JmlClauseGenerator

All Implemented Interfaces:

org.eclipse.jface.operation.IRunnableWithProgress

Direct Known Subclasses:

ModifiesGenerator, RequiresGenerator

public abstract class JmlClauseGenerator

extends RunnableWithError

implements org.eclipse.jface.operation.IRunnableWithProgress

Generator of JML clause.

Author:

L. Burdy

Constructor Summary

JmlClauseGenerator(IJml2bConfiguration configuration, org.eclipse.swt.widgets.Shell shell, JmlFile f)

Method Summary

boolean	getUpdated(int i)
void	run(org.eclipse.core.runtime.IProgressMonitor monitor)
void	setMethods(java.lang.Object[] objects)

Methods inherited from class jack.plugin.RunnableWithError

getErrorDescription, getErrorDetails, hasDetails, hasSucceeded

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

JmlClauseGenerator

public JmlClauseGenerator(IJml2bConfiguration configuration,
                          org.eclipse.swt.widgets.Shell shell,
                          JmlFile f)

Method Detail

run

public void run(org.eclipse.core.runtime.IProgressMonitor monitor)

Specified by:

run in interface org.eclipse.jface.operation.IRunnableWithProgress

setMethods

public void setMethods(java.lang.Object[] objects)

Parameters:

objects -

getUpdated

public boolean getUpdated(int i)

Returns: