Overview of the ProgramAnalysis Subpackage of the CodeTools Package
DescriptionList of ProgramAnalysis Package CommandsReferencesCompatibility
<Text-field style="Heading 2" layout="Heading 2" bookmark="info">Description</Text-field>
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).
<Text-field style="Heading 2" layout="Heading 2" bookmark="bkmrk0">List of ProgramAnalysis Package Commands</Text-field>
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
IterationSpaceDependenceConeUnimodularTransformation
While loop related commands
IsLoopInvariantLoopInvariantTrajectoryPointsVerifyLoop
From a procedure generate a static call graph
StaticCallGraph
<Text-field style="Heading 2" layout="Heading 2" bookmark="bkmrk1">References</Text-field>
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.
<Text-field style="Heading 2" layout="Heading 2" bookmark="compatibility">Compatibility</Text-field>
The CodeTools:-ProgramAnalysis package was introduced in Maple 2016.
For more information on Maple 2016 changes, see Updates in Maple 2016.See AlsoRegularChainsCodeToolsmaplemint