Overview of the ProgramAnalysis Subpackage of the CodeTools Package
List of ProgramAnalysis Package Commands
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
Generating procedures from the "ForLoop" and "WhileLoop" data structures
For loop related commands
While loop related commands
From a procedure generate a static call graph
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.
Download Help Document