Module dev.civl.mc

Package dev.civl.mc.model.IF

Interface AbstractFunction

All Superinterfaces:

CIVLFunction, Sourceable

public interface AbstractFunction
extends CIVLFunction

An abstract function is an uninterpreted mathematical function. It is used in assumptions and assertions to relate values in code to the actual mathematical functions they represent.

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static enum	AbstractFunction.SpecialRelationKind	The kind of a special relation represented by this abstract function

Method Summary

Modifier and Type	Method	Description
int	continuity()
AbstractFunction.SpecialRelationKind	getAttribute()

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

addLocation, addPossibleValidConsequence, addStatement, computePathconditionOfLocations, containingScope, dependsNoact, fid, functionContract, functionType, getAccessesAtomicFunction, getPossibleValidConsequences, isAbstractFunction, isAtomicFunction, isContracted, isFreeOfUnsafeloop, isLogic, isNondet, isNormalFunction, isPureFunction, isPurelyLocal, isRootFunction, isStateFunction, isSystemFunction, locations, model, name, outerScope, parameters, print, purelyLocalAnalysis, purelyLocalAnalysisForVariables, returnType, scopes, setAccessesAtomicFunction, setContainingScope, setFreeOfUnsafeloop, setFunctionContract, setLocations, setLogic, setModel, setName, setOuterScope, setParameters, setParameterTypes, setPureFunction, setReturnType, setScopes, setStartLocation, setStateFunction, setStatements, simplify, startLocation, statements, unreachedCode, variableAddressedOf, variableAddressedOf

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

getSource, setCIVLSource

Method Details

continuity

int continuity()

Returns:

The total number of partial derivatives that may be taken.

getAttribute

AbstractFunction.SpecialRelationKind getAttribute()

Returns:

AbstractFunction.SpecialRelationKind of a special relation (or NONE) represented by this abstract function