FunctionContract.java

package dev.civl.mc.model.IF.contract;

import java.io.PrintStream;

import dev.civl.mc.model.IF.Scope;
import dev.civl.mc.model.IF.Sourceable;
import dev.civl.mc.model.IF.expression.Expression;

/**
 * This represents a block of ACSL contract for a function.
 * 
 * @author Manchun Zheng
 *
 */
public interface FunctionContract extends Sourceable {

	/**
	 * ContractKind: This kind is used to denotes all kinds of contracts. Currently,
	 * there are 5 kinds of contracts:
	 * <ul>
	 * <li>REQUIRES: denotes that the requirements of the contracts are used to
	 * infer some states.</li>
	 * <li>ENSURES:denotes that the ensurances of the contracts are guaranteed by
	 * some states.</li>
	 * <li>INFER: denotes that the ensurances of the contracts are used to infer
	 * some states.</li>
	 * <li>WAITSFOR: delivers an explicit synchronization knowledge.</li>
	 * </ul>
	 * 
	 * @author ziqingluo
	 *
	 */
	static public enum ContractKind {
		REQUIRES, ENSURES, INFER, WAITSFOR, LOOP
	}

	/**
	 * Returns the default behavior of the function.
	 * 
	 * @return
	 */
	FunctionBehavior defaultBehavior();

	/**
	 * Returns the named behaviors of the function.
	 * 
	 * @return
	 */
	Iterable<NamedFunctionBehavior> namedBehaviors();

	/**
	 * Returns the guard of the function.
	 * 
	 * @return
	 */
	Expression guard();

	/**
	 * Does the contract contains <code>pure</code> clause?
	 * 
	 * @return
	 */
	boolean isPure();

	/**
	 * Updates the contract to denote if it contains <code>pure</code> clause.
	 * 
	 * @param value
	 */
	void setPure(boolean value);

	/**
	 * Sets the guard of the function.
	 * 
	 * @param expression
	 */
	void setGuard(Expression expression);

	/**
	 * Sets the default behavior of the function.
	 * 
	 * @param behavior
	 */
	void setDefaultBehavior(FunctionBehavior behavior);

	/**
	 * Adds a named behavior to the function.
	 * 
	 * @param behavior
	 */
	void addNamedBehavior(NamedFunctionBehavior behavior);

	/**
	 * returns the behavior with the given name; null if no such behavior exists.
	 * 
	 * @param name
	 * @return
	 */
	NamedFunctionBehavior getBehavior(String name);

	/**
	 * prints this function contract
	 * 
	 * @param prefix
	 * @param out
	 * @param isDebug
	 */
	void print(String prefix, PrintStream out, boolean isDebug);

	/**
	 * is there reads clause in this contract?
	 * 
	 * @return
	 */
	boolean hasReadsClause();

	/**
	 * is there assigns clause in this contract?
	 * 
	 * @return
	 */
	boolean hasAssignsClause();

	/**
	 * is there depends clause in this contract?
	 * 
	 * @return
	 */
	boolean hasDependsClause();

	/**
	 * is there any requirements or ensurances ?
	 * 
	 * @return
	 */
	boolean hasRequirementsOrEnsurances();

	/**
	 * The static scope in which the function contract exists. Not necessarily the
	 * same as the function definition's parameter scope, because the contract may
	 * have been associated with a function prototype.
	 * 
	 * @return scope in which contract exists
	 */
	Scope scope();
}