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

Interface FunctionBehavior

All Superinterfaces:
Sourceable
All Known Subinterfaces:
NamedFunctionBehavior
public interface FunctionBehavior extends Sourceable
This represents a non-named behavior of the ACSL function contract. It contains the common components of the default behavior and any named behavior of a function contract.

  • Method Details

    • requirements

      Iterable<Expression> requirements()
      Returns the preconditions of this behavior.
      Returns:

    • ensurances

      Iterable<Expression> ensurances()
      Returns the postconditions of this behavior.
      Returns:

    • assignsMemoryUnits

      Iterable<Expression> assignsMemoryUnits()
      Returns the assigns clause of this behavior.
      Returns:

    • readsMemoryUnits

      Iterable<Expression> readsMemoryUnits()
      Returns the reads clause of this behavior.
      Returns:

    • dependsEvents

      Iterable<DependsEvent> dependsEvents()
      Returns the depends events of this behavior.
      Returns:

    • readsNothing

      boolean readsNothing()
      Does this function reads nothing? That is, is there a reads \nothing; clause in the contract.
      Returns:

    • assignsNothing

      boolean assignsNothing()
      Does this function assigns nothing? That is, is there a assigns \nothing; clause in the contract.
      Returns:

    • dependsNoact

      boolean dependsNoact()
      Is this function depending on nothing?
      Returns:

    • dependsAnyact

      boolean dependsAnyact()
      Is this function depending on anything?
      Returns:

    • setReadsNothing

      void setReadsNothing()
      When a reads \nothing; clause appears, sets the function behavior to be reading nothing.
      Precondition:
      invalid reference 
      #numReadsClauses()
      ==0;

    • setAssingsNothing

      void setAssingsNothing()
      When a assigns \nothing; clause appears, sets the function behavior to be assigning nothing.
      Precondition:
      invalid reference 
      #numAssignsClauses()
      ==0;

    • setDependsNoact

      void setDependsNoact()
      When a depends \noact; clause appears, sets the function behavior to be depending on nothing.
      Precondition: numDependsEvents()==0 invalid input: '&'invalid input: '&' ==false;

    • setDependsAnyact

      void setDependsAnyact()
      When a depends \anyact; clause appears, sets the function behavior to be depending on anything.
      Precondition:
      invalid @link 
      {@link #dependsNoact()==false
      };

    • addPrecondition

      void addPrecondition(Expression condition)
      Returns the precondition of this behavior.
      Parameters:
      condition -

    • addPostcondition

      void addPostcondition(Expression condition)
      Returns the post condition of this behavior.
      Parameters:
      condition -

    • addAssignsMemoryUnit

      void addAssignsMemoryUnit(Expression mu)
      Add an assigns clause to this behavior.
      Parameters:
      assigns -

    • addReadsMemoryUnit

      void addReadsMemoryUnit(Expression mu)
      Add a reads clause to this behavior.
      Parameters:
      reads -

    • addDependsEvent

      void addDependsEvent(DependsEvent dependsEvent)
      Add a depends event to this behavior.
      Precondition: dependsNoact()==false;
      Parameters:
      depends -

    • numRequirements

      int numRequirements()
      Returns the number of preconditions of this behavior.
      Returns:

    • numEnsurances

      int numEnsurances()
      Returns the number of postconditions of this behavior.
      Returns:

    • numAssignsMemoryUnits

      int numAssignsMemoryUnits()
      Returns the number of assigns clauses of this behavior.
      Returns:

    • numReadsMemoryUnits

      int numReadsMemoryUnits()
      Returns the number of reads clauses of this behavior.
      Returns:

    • numDependsEvents

      int numDependsEvents()
      Returns the number of depends events of this behavior.
      Returns:

    • print

      void print(String prefix, PrintStream out, boolean isDebug)
      Prints this behavior
      Parameters:
      out -
      isDebug -
      subPrefix -

    • clearDependsEvents

      void clearDependsEvents()
      clears the depends events of this behavior.

    • setWaitsforList

      void setWaitsforList(Iterable<Expression> waitsforArgs)
      Set an expression collection as the arguments set as the "waitsfor" clause.
      Parameters:
      waitsforArgs -

    • getWaitsforList

      Set<Expression> getWaitsforList()
      Get an iterable collection of expressions which contains arguments of a "waitsfor" clause. A "waitsfor" clause represents the synchronization relations of a function.

      waitsfor P, (where P is a set of process IDs) means the function will force the current process to wait for all processes p in P come in this function before the current process can proceed.

      Returns: