jack.plugin.source
Class ModifiesGenerator

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

All Implemented Interfaces:

org.eclipse.jface.operation.IRunnableWithProgress

public class ModifiesGenerator

extends JmlClauseGenerator

Generator of modifies clause.

Author:

L. Burdy

Constructor Summary

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

Methods inherited from class jack.plugin.source.JmlClauseGenerator

getUpdated, run, setMethods

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

ModifiesGenerator

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