

Aligators Tool


english only


Aligators is a Mathematica package for inferring quantified invariants of loops iterating over multdimensional arrays, such as matrices. When used on matrices, matrix shapes as type invariants (uppertriangular, diagonal, etc) can be derived from the invariant inferred by Aligators.
Aligators is a generalization of the Aligator package.
Inputs to Aligators are nested forloops iterating iterating linearly (rowbyrow or columnby column) over the matrix content by incrementing (or decrementing) the matrix row and column indices, and with assignments, sequencing, and nested conditionals over scalar and matrix variables in the innermost loop body.
We require that the innermost loop body fulfills the conditions below:
Aligators was implemented in Mathematica. It
Copyright © 2009 Laura Kovács — all rights reserved. Commercial use of the software is prohibited without prior written permission.
The package is encoded. It cannot be read or modified directly as plain text, but can be loaded into Mathematica just like any normal input file (i.e., with <<"file" or Get["file"]). There is no need (and also no way) to decode them by using additional software or a special key.
If loading an encoded file causes a syntax error, open it with a text editor and remove any blank lines at the beginning.
The package is contained in the Mathematica input file Aligators.m of
If you do not have Mathematica installed, you might study the demo file Demo.pdf.
Further information can be found here:
T. A. Henzinger, T. Hottelier and L. Kovács (2009), Type Invariants for Matrices Technical Report, EPFL, Switzerland. [pdf]
The tool was written and developed at at MTC, EPFL, Switzerland.
Right now you are using Version 0.3, last updated on January 29, 2009.
Please report any bugs and comments to Laura Kovács.