Overview of the ProgramAnalysis Subpackage of the CodeTools Package
Description
List of ProgramAnalysis Package Commands
References
Compatibility
The ProgramAnalysis package provides commands for working with for loops and while loops. For loops can be analyzed to investigate the data dependencies between array references and to apply transformations to the loop's index variables. These tools can be used to formally verify the correctness of a program. The properties of while loops can be analyzed to find invariants of the loop and to determine whether or not a given procedure satisfies its specifications (post-condition).
The following is a list of available package commands.
Creating "ForLoop" and "WhileLoop" data structures
CreateLoop
Generating procedures from the "ForLoop" and "WhileLoop" data structures
GenerateProcedure
For loop related commands
IterationSpace
DependenceCone
UnimodularTransformation
While loop related commands
IsLoopInvariant
LoopInvariant
TrajectoryPoints
VerifyLoop
From a procedure generate a static call graph
StaticCallGraph
Marc Moreno Maza and Rong Xiao. "Degree and dimension estimates for invariant ideals of P-solvable recurrence." Computer Mathematics. Springer Berlin Heidelberg. October 1, 2014. pp 349-373.
Marc Moreno Maza and Rong Xiao. "Generating Program Invariants via Interpolation." CoRR. 2012.
The CodeTools:-ProgramAnalysis package was introduced in Maple 2016.
For more information on Maple 2016 changes, see Updates in Maple 2016.
See Also
RegularChains
CodeTools
maplemint
Download Help Document
