Module dev.civl.mc

Package dev.civl.mc.model.IF.contract

Interface NamedFunctionBehavior

All Superinterfaces:

FunctionBehavior, Sourceable

public interface NamedFunctionBehavior
extends FunctionBehavior

A named behavior contains a name and assumptions in addition to those components contained by FunctionBehavior. It is corresponding to the named behavior block of an ACSL function contract.

Method Summary

Modifier and Type	Method	Description
Expression	assumptions()	Returns the conjunction of all assumptions of this behavior.
String	name()	Returns the name of this behavior.
void	print(String prefix, PrintStream out, boolean isDebug)	prints this behavior
void	setAssumption(Expression assumption)	Set the conjunction of all assumptions to this behavior.

Methods inherited from interface dev.civl.mc.model.IF.contract.FunctionBehavior

addAssignsMemoryUnit, addDependsEvent, addPostcondition, addPrecondition, addReadsMemoryUnit, assignsMemoryUnits, assignsNothing, clearDependsEvents, dependsAnyact, dependsEvents, dependsNoact, ensurances, getWaitsforList, numAssignsMemoryUnits, numDependsEvents, numEnsurances, numReadsMemoryUnits, numRequirements, readsMemoryUnits, readsNothing, requirements, setAssingsNothing, setDependsAnyact, setDependsNoact, setReadsNothing, setWaitsforList

Methods inherited from interface dev.civl.mc.model.IF.Sourceable

getSource, setCIVLSource

Method Details

name

String name()

Returns the name of this behavior.

Returns:

print

void print(String prefix,
 PrintStream out,
 boolean isDebug)

prints this behavior

Specified by:

print in interface FunctionBehavior

Parameters:

prefix -

out -

isDebug -

assumptions

Expression assumptions()

Returns the conjunction of all assumptions of this behavior.

Returns:

setAssumption

void setAssumption(Expression assumption)

Set the conjunction of all assumptions to this behavior.

Parameters:

assumption -