In this appendix, we describe the language that is used in the RISC ProgramExplorer for specifying programs. This language is based upon the logic language of the RISC ProofNavigator as explained in Section C.1. With this language whose formal syntax is described in Appendix H.2, theories can be constructed as described in Sections C.2 and C.3. With the help of theories, we may specify programs as described in Sections C.5, C.6, and C.7.