Overview of the ProgramAnalysis Subpackage of the CodeTools Package - Maple Programming Help

# Online Help

###### All Products    Maple    MapleSim

Home : Support : Online Help : Programming : CodeTools : Program Analysis : CodeTools/ProgramAnalysis

Overview of the ProgramAnalysis Subpackage of the CodeTools Package

Description

 • 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).

List of ProgramAnalysis Package Commands

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

References

 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.

Compatibility

 • The CodeTools[ProgramAnalysis] package was introduced in Maple 2016.
 • For more information on Maple 2016 changes, see Updates in Maple 2016.

 See Also