Practicals
Practicals is a package for programming strategies in PVS with high level tacticals. Practicals enhances the PVS proof language (IF, REPEAT, THEN, TRY, ...) with tacticals for
- Looping (WHILE, FOR)
- Matching terms (MATCH)
- Matching proof contexts (SCREEN)
- Raising proof failures (THROW)
- Catching proof failures (CATCH), and more ...
Practicals was developed by Florent Kirchner while in residence in the Formal
Methods group at the National Institute of Aerospace
(NIA).
Publications
- Florent Kirchner and César Muñoz, The Proof Monad,
Journal of Logic and Algebraic Programming, Volume 79, Issues 3-5, pp. 264-277, April-July 2010. BibTeX Reference.
- Florent Kirchner and César Muñoz, PVS#: Streamlined Tacticals for PVS,
Electronic Notes in Theoretical Computer Science, Volume 174, Issue 11, July 2007. BibTeX Reference.
identifies links that are outside
the NASA domain
