Module Analysis.Deterministic

Determinism analysis: checks whether functions are deterministic or nondeterministic, i.e., whether its evaluation on ground argument terms might cause different computation paths.

Author: Michael Hanus

Version: November 2024

Summary of exported operations:

overlapAnalysis :: Analysis Bool  Deterministic 
showOverlap :: AOutFormat -> Bool -> String  Deterministic 
functionalAnalysis :: Analysis Bool  Deterministic 
showFunctional :: AOutFormat -> Bool -> String  Deterministic 
isNondetDefined :: FuncDecl -> Bool  Deterministic 
showDet :: AOutFormat -> Deterministic -> String  Deterministic 
nondetAnalysis :: Analysis Deterministic  Deterministic 
showNonDetDeps :: AOutFormat -> [((String,String),[(String,String)])] -> String  Deterministic 
nondetDepAnalysis :: Analysis [((String,String),[(String,String)])]  Deterministic 
Non-deterministic dependency analysis.
nondetDepAllAnalysis :: Analysis [((String,String),[(String,String)])]  Deterministic 
Non-deterministic dependency analysis.

Exported datatypes:

Deterministic

Data type to represent determinism information.

Constructors:

  • NDet :: Deterministic
  • Det :: Deterministic

Exported operations:

overlapAnalysis :: Analysis Bool  Deterministic 

showOverlap :: AOutFormat -> Bool -> String  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

showFunctional :: AOutFormat -> Bool -> String  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

isNondetDefined :: FuncDecl -> Bool  Deterministic 

showDet :: AOutFormat -> Deterministic -> String  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

showNonDetDeps :: AOutFormat -> [((String,String),[(String,String)])] -> String  Deterministic 

nondetDepAnalysis :: Analysis [((String,String),[(String,String)])]  Deterministic 

Non-deterministic dependency analysis. The analysis computes for each operation the set of operations with a non-deterministic definition which might be called by this operation. Non-deterministic operations that are called by other non-deterministic operations are ignored so that only the first (w.r.t. the call sequence) non-deterministic operations are returned.

nondetDepAllAnalysis :: Analysis [((String,String),[(String,String)])]  Deterministic 

Non-deterministic dependency analysis. The analysis computes for each operation the set of all operations with a non-deterministic definition which might be called by this operation.