PAKCS
Exported names: Imported modules:

Module Analysis.Termination

Termination analysis: checks whether an operation is terminating, i.e., whether all evaluations on ground argument terms are finite. The method used here checks whether the arguments in all recursive calls of an operation are smaller than the arguments passed to the operation.

Author: Michael Hanus

Version: February 2017

Summary of exported operations:

terminationAnalysis :: Analysis Bool   
showTermination :: AOutFormat -> Bool -> String   
productivityAnalysis :: Analysis Productivity   
showProductivity :: AOutFormat -> Productivity -> String   

Exported datatypes:

Productivity

Data type to represent productivity status of an operation.

Constructors:

  • NoInfo :: Productivity
  • Terminating :: Productivity
  • DCalls :: [QName] -> Productivity
  • Looping :: Productivity

Exported operations:

showTermination :: AOutFormat -> Bool -> String   

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

showProductivity :: AOutFormat -> Productivity -> String