The Pandora part is for logic only, and uses the boxproof method for natural deduction, as described in the book Reasoned Programming. The tool will allow you to construct correct proofs that a conclusion follows from some given sentences, all expressed in logic.

The Raptor part is a tool for reasoning about (imperative) programs and it includes Pandora Rules as a sub-system. This tool extends the boxproof method for natural deduction to allow you to construct proofs of programs using the statement kinds of assignment, while and if. It incorporates reasoning with booleans and single dimensional arrays as well as integer types, and allows methods to be defined and called within a program. As with Pandora, you write a program together with its precondition and postcondition, and then try to show that if the precondition holds and the program executes, then the postcondition will hold.

Since Raptor uses Pandora for reasoning about logic, we advise that you play with Pandora first to gain familiarity with the interface. Various help files are included, as well as a manual. We hope you will enjoy using it.