ProofPower Documentation

This directory contains the documentation that is supplied with the six packages that make up the ProofPower specification and verification tool suite:

• PPDev - The ProofPower developer toolkit including the SLRP Parser Generator
• PPTex - The ProofPower interface to TeX and LaTeX.
• PPXpp - The X Windows front-end for ProofPower
• PPHol - The HOL specification and proof development system
• PPZed - The Z specification and proof development system
• PPDaz - The Compliance Tool for specifying and verifying

The papers are supplied as PDF files.

PPDev

• ProofPower - SLRP User Guide - how to use the SLRP Parser Generator

PPTex

• ProofPower - Document Preparation - how to typeset ProofPower documents using the LaTeX interface

• Xpp - User Guide - an overview of Xpp

• ProofPower - Description - descriptions of the HOL and Z concrete syntax and some background information on how to control PPHol and PPZed
• ProofPower - Tutorial Manual - a tutorial on working with HOL in ProofPower (based on Cambdige HOL documentation)
• ProofPower - HOL Tutorial Transparencies - a short course on specification and proof with PPHol
• ProofPower - HOL Tutorial Notes - notes on the short course on specification and proof with PPHol
• ProofPower - HOL Reference Manual - the comprehensive reference manual on PPHol, includes a keyword-in-context index

Examples and Demos

• Modal Logic in HOL
• Ramsey's Theorem in ProofPower
• Theorems on Finiteness
• Library Theorems
• Creating Example ProofPower Databases

Formal Specification

• HOL Formalised: Language and Overview
• HOL Formalised: Semantics
• HOL Formalised: Deductive System
• HOL Formalised: Proof Development System
• HOL Formalised: Formal Design of the Logical Kernel

• ProofPower - Description - descriptions of the HOL and Z concrete syntax and some background information on PPHol and PPZed
• ProofPower - Z Tutorial Transparencies - a short course on specification and proof with PPZed
• ProofPower - Z Tutorial Manual - notes from t short course on specification and proof with PPZed
• ProofPower - Z Reference Manual - the comprehensive reference manual on PPZed, includes a keyword-in-context index

Examples and Demos

• Methods and Tools for the Verification of Critical Properties
• Creating Example ProofPower Databases

• Compliance Tool - User Guide - how to get started with the Compliance Tool with some reference information
• Compliance Tool - Installation and Operation - installation instructions for the Compliance Tool
• Compliance Tool - Proving VCs - a refresher course on proof in Z customised to proving the verification conditions that the Compliance Tool generates
• Compliance Tool - Language Description - describes the syntax and semantics of the Compliance Notation

Examples and Demos

• First 1000 Primes Example
• Example of Literate Script Development
• Calculator Example
• Calculator Example VCs Proof Scripts

Copyright © Lemma 1 Ltd. Created by  Rob Arthan Last updated: $Date: 2004/06/28 13:13:54 $