Welcome to Alt-Ergo’s tutorial !

This interactive tutorial is an introduction to Alt-Ergo and its native language.

For some of the sample code that will be presented, you’ll be able to run Alt-Ergo directly in your browser, to see what it does. You can edit the sample code, and rerun Alt-Ergo to see the effect of your modifications

Note that the in-browser version of Alt-Ergo is provided for convenience only, and isn’t especially powerful. While it should be enough to go through the tutorial and to make your own little experiments, you might want to install Alt-Ergo on your own machine to enjoy its full speed.

• Overview
  • What is it ?
  • How does it relate to other tools ?
• Get started with Alt-Ergo ! Logical foundations
  • Symbols, axioms and goals
  • Expanding our logical vocabulary
• Compute with functions
  • Uninterpreted functions
  • Explicit functions
  • Associative and commutative symbols
• Application: prove imperative programs
  • Check overflows
  • Loop invariants
  • Loop variants
• Model complex structures with types
  • Examples
  • Pattern matching
  • Modelisation exercises
• Application: prove functional programs
  • Recursive functions and induction
  • Higher-order functions and functional arrays
• Appendix: Experimental support for models and counter-examples generation
  • Options for model generation
  • Examples

Back to Try-Alt-Ergo